From fbcfe6596eed8bd9ca91b6b6b9cefe4918247cbb Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Wed, 13 Dec 2023 12:45:30 -0500
Subject: [PATCH] fix: lake: leave `run` options for script (#3064)

Options passed to `lake script run <name>` / `lake run <name>` after the
`<name>` will now be properly passed on through to the script rather
than being consumed by Lake.

The issue was reported [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lake.20script.20flag.20.22passthrough.22.3F/near/407734447).
---
 src/lake/Lake/CLI/Main.lean            | 2 +-
 src/lake/examples/scripts/expected.out | 1 +
 src/lake/examples/scripts/test.sh      | 1 +
 3 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean
index 7e402d0066..370e8f7d4a 100644
--- a/src/lake/Lake/CLI/Main.lean
+++ b/src/lake/Lake/CLI/Main.lean
@@ -226,7 +226,7 @@ protected def list : CliM PUnit := do
         IO.println script.name
 
 protected nonrec def run : CliM PUnit := do
-  processOptions lakeOption
+  processLeadingOptions lakeOption  -- between `lake [script] run` and `<name>`
   let config ← mkLoadConfig (← getThe LakeOptions)
   let ws ← loadWorkspace config
   if let some spec ← takeArg? then
diff --git a/src/lake/examples/scripts/expected.out b/src/lake/examples/scripts/expected.out
index 47508d273a..ac7cdad5a4 100644
--- a/src/lake/examples/scripts/expected.out
+++ b/src/lake/examples/scripts/expected.out
@@ -3,6 +3,7 @@ scripts/dismiss
 scripts/greet
 Hello, world!
 Hello, me!
+Hello, --me!
 Display a greeting
 
 USAGE:
diff --git a/src/lake/examples/scripts/test.sh b/src/lake/examples/scripts/test.sh
index b032172cc3..0d90532679 100755
--- a/src/lake/examples/scripts/test.sh
+++ b/src/lake/examples/scripts/test.sh
@@ -11,6 +11,7 @@ $LAKE update
 $LAKE script list | tee produced.out
 $LAKE run /greet | tee -a produced.out
 $LAKE script run greet me | tee -a produced.out
+$LAKE script run greet --me | tee -a produced.out
 $LAKE script doc greet | tee -a produced.out
 $LAKE script run hello | tee -a produced.out
 $LAKE script run dep/hello | tee -a produced.out