#lang scheme/base (require scheme/sandbox "../language/acl2-module-v.scm") (provide the-evaluator evaluator) (define (evaluator . definitions) (parameterize ([sandbox-path-permissions '([read #rx#""] [write #rx#"LINKAGE$"])] [sandbox-output 'string] [sandbox-error-output 'string] [sandbox-eval-limits (list #f #f)]) (apply make-evaluator acl2-module-v definitions))) (define the-evaluator (evaluator))