From 9badaf470d8f724346d33738bd273efacd78df76 Mon Sep 17 00:00:00 2001 From: Matteo Cipollina Date: Thu, 30 Jul 2026 15:15:47 +0200 Subject: [PATCH] Insert '--' terminator before the sandboxed command in buildLandrunArgs landrun's CLI parser continues flag-scanning past positionals and consumes the first bare '--' in the command tail. safeExport passes exactly such a '--' to lean4export as the module/declaration separator, so lean4export receives the declaration names as module names and fails with 'unknown module prefix'. Adding the explicit flag terminator before the command protects every sandboxed invocation's arguments. --- Main.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Main.lean b/Main.lean index 284f7a3..60e6837 100644 --- a/Main.lean +++ b/Main.lean @@ -84,7 +84,7 @@ def buildLandrunArgs (spawnArgs : LandrunArgs) : Array String := let args := spawnArgs.readablePaths.foldl (init := args) (fun acc path => acc ++ #["--ro", path.toString]) let args := spawnArgs.writablePaths.foldl (init := args) (fun acc path => acc ++ #["--rwx", path.toString]) let args := spawnArgs.executablePaths.foldl (init := args) (fun acc path => acc ++ #["--rox", path.toString]) - args ++ #[spawnArgs.cmd] ++ spawnArgs.args + args ++ #["--", spawnArgs.cmd] ++ spawnArgs.args def runSandBoxedWithStdout (spawnArgs : LandrunArgs) : M String := do let args := buildLandrunArgs spawnArgs