From ac98cf428cae0c9cf580ede31d1e6812daa3e8fe Mon Sep 17 00:00:00 2001
From: FrederickPu <119814259+FrederickPu@users.noreply.github.com>
Date: Thu, 24 Jul 2025 15:11:14 +0000
Subject: [PATCH 1/4] added ability to loadDynlib through command line args

---
 REPL/Main.lean | 47 ++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 46 insertions(+), 1 deletion(-)

diff --git a/REPL/Main.lean b/REPL/Main.lean
index d181080f..062f4896 100644
--- a/REPL/Main.lean
+++ b/REPL/Main.lean
@@ -418,6 +418,44 @@ def printFlush [ToString α] (s : α) : IO Unit := do
   out.putStr (toString s)
   out.flush -- Flush the output
 
+/-- Parses command-line arguments of the form:
+    --flag-name value1 value2 ... --other-flag val ...
+    into a map from flag name to list of values.
+
+    example usage:
+    #eval parseFlagArgs ["--dog", "adjak", "a;lskda;l"] -- Std.HashMap.ofList [("dog", ["adjak", "a;lskda;l"])]
+    #eval parseFlagArgs ["--dog", "adjak", "a;lskda;l", "--cat", "ads"] -- Std.HashMap.ofList [("dog", ["adjak", "a;lskda;l"]), ("cat", ["ads"])]
+    #eval parseFlagArgs ["--dog", "adjak", "a;lskda;l",  "--cat", "ads", "--dog", "womp"] -- Std.HashMap.ofList [("dog", ["adjak", "a;lskda;l", "womp"]), ("cat", ["ads"])]
+    #eval parseFlagArgs ["--dog", "as"] -- Std.HashMap.ofList [("dog", ["as"])]
+    #eval parseFlagArgs ["--dog"] -- Std.HashMap.ofList [("dog", [])]
+    #eval parseFlagArgs ["asd"] -- Std.HashMap.ofList []
+-/
+def parseFlagArgs (args : List String) : Std.HashMap String (List String) :=
+  let rec go (args : List String) (cur : Option String) (acc : Std.HashMap String (List String)) :=
+    match args with
+    | [] =>
+      match cur with
+      | some flag => acc.insert flag (acc.getD flag [])  -- ensure it's inserted even if no values
+      | none => acc
+    | arg :: rest =>
+      if arg.startsWith "--" then
+        let acc :=
+          match cur with
+          | some flag => acc.insert flag (acc.getD flag [])  -- close previous flag if it had no values
+          | none => acc
+        let newFlag := arg.drop 2
+        go rest (some newFlag) acc
+      else
+        match cur with
+        | some flag =>
+          let updated := acc.insert flag (arg :: acc.getD flag [])
+          go rest (some flag) updated
+        | none =>
+          -- positional value with no preceding flag (ignored)
+          go rest none acc
+  let raw := go args none {}
+  raw.map (fun _ x => List.reverse x)
+
 /-- Read-eval-print loop for Lean. -/
 unsafe def repl : IO Unit :=
   StateT.run' loop {}
@@ -438,6 +476,13 @@ where loop : M IO Unit := do
   loop
 
 /-- Main executable function, run as `lake exe repl`. -/
-unsafe def main (_ : List String) : IO Unit := do
+unsafe def main (args : List String) : IO Unit := do
+  let flagMap := parseFlagArgs args
+  
+  let dynlibs := flagMap.getD "dynlib" []
+  for lib in dynlibs do
+    IO.println s!"Loading dynlib: {lib}"
+    Lean.loadDynlib lib
+
   initSearchPath (← Lean.findSysroot)
   repl

From d8636d2d38ecd8bef279450faec13ba944722b95 Mon Sep 17 00:00:00 2001
From: FrederickPu <119814259+FrederickPu@users.noreply.github.com>
Date: Fri, 25 Jul 2025 14:22:41 +0000
Subject: [PATCH 2/4] added test example

---
 test/dynlib/CMakeLists.txt | 9 +++++++++
 test/dynlib/mylib.c        | 6 ++++++
 2 files changed, 15 insertions(+)
 create mode 100644 test/dynlib/CMakeLists.txt
 create mode 100644 test/dynlib/mylib.c

diff --git a/test/dynlib/CMakeLists.txt b/test/dynlib/CMakeLists.txt
new file mode 100644
index 00000000..73f0a441
--- /dev/null
+++ b/test/dynlib/CMakeLists.txt
@@ -0,0 +1,9 @@
+cmake_minimum_required(VERSION 3.15)
+project(mylib C)
+
+# Put your actual path here from step 1
+set(LEAN_INCLUDE_DIR "/home/codespace/.elan/toolchains/leanprover--lean4---v4.22.0-rc4/include")
+
+include_directories(${LEAN_INCLUDE_DIR})
+
+add_library(mylib SHARED mylib.c)
diff --git a/test/dynlib/mylib.c b/test/dynlib/mylib.c
new file mode 100644
index 00000000..754087ce
--- /dev/null
+++ b/test/dynlib/mylib.c
@@ -0,0 +1,6 @@
+#include <lean/lean.h>
+
+LEAN_EXPORT uint32_t l_add(uint32_t a, uint32_t b) {
+    return a + b;
+}
+

From 60c569135e443e3c666ff903d603e2a203a23fe7 Mon Sep 17 00:00:00 2001
From: FrederickPu <119814259+FrederickPu@users.noreply.github.com>
Date: Fri, 25 Jul 2025 19:53:31 +0000
Subject: [PATCH 3/4] added test changes

---
 .../.github/workflows/lean_action_ci.yml      | 14 +++++++++++++
 test/dynlib/.gitignore                        |  1 +
 test/dynlib/Main.lean                         |  4 ++++
 test/dynlib/README.md                         |  1 +
 test/dynlib/fail.in                           |  3 +++
 test/dynlib/lake-manifest.json                |  5 +++++
 test/dynlib/lakefile.lean                     | 13 ++++++++++++
 test/dynlib/lean-toolchain                    |  1 +
 test/dynlib/success.in                        |  5 +++++
 test/dynlib/test.sh                           | 20 +++++++++++++++++++
 10 files changed, 67 insertions(+)
 create mode 100644 test/dynlib/.github/workflows/lean_action_ci.yml
 create mode 100644 test/dynlib/.gitignore
 create mode 100644 test/dynlib/Main.lean
 create mode 100644 test/dynlib/README.md
 create mode 100644 test/dynlib/fail.in
 create mode 100644 test/dynlib/lake-manifest.json
 create mode 100644 test/dynlib/lakefile.lean
 create mode 100644 test/dynlib/lean-toolchain
 create mode 100644 test/dynlib/success.in
 create mode 100644 test/dynlib/test.sh

diff --git a/test/dynlib/.github/workflows/lean_action_ci.yml b/test/dynlib/.github/workflows/lean_action_ci.yml
new file mode 100644
index 00000000..09cd4ca6
--- /dev/null
+++ b/test/dynlib/.github/workflows/lean_action_ci.yml
@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1
diff --git a/test/dynlib/.gitignore b/test/dynlib/.gitignore
new file mode 100644
index 00000000..bfb30ec8
--- /dev/null
+++ b/test/dynlib/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/test/dynlib/Main.lean b/test/dynlib/Main.lean
new file mode 100644
index 00000000..7c591c91
--- /dev/null
+++ b/test/dynlib/Main.lean
@@ -0,0 +1,4 @@
+import Dynlib
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"
diff --git a/test/dynlib/README.md b/test/dynlib/README.md
new file mode 100644
index 00000000..055e48b7
--- /dev/null
+++ b/test/dynlib/README.md
@@ -0,0 +1 @@
+# dynlib
\ No newline at end of file
diff --git a/test/dynlib/fail.in b/test/dynlib/fail.in
new file mode 100644
index 00000000..39ae4514
--- /dev/null
+++ b/test/dynlib/fail.in
@@ -0,0 +1,3 @@
+{ "cmd": "@[extern \"add\"]\nopaque add' (a b : UInt32) : UInt32" }
+
+{ "cmd": "#eval add' 2 2", "env": 0 }
diff --git a/test/dynlib/lake-manifest.json b/test/dynlib/lake-manifest.json
new file mode 100644
index 00000000..e9f31ca4
--- /dev/null
+++ b/test/dynlib/lake-manifest.json
@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "dynlib",
+ "lakeDir": ".lake"}
diff --git a/test/dynlib/lakefile.lean b/test/dynlib/lakefile.lean
new file mode 100644
index 00000000..9723e286
--- /dev/null
+++ b/test/dynlib/lakefile.lean
@@ -0,0 +1,13 @@
+import Lake
+open Lake DSL
+
+package dynlib where
+  name := "dynlib"
+  defaultTargets := #[`dynlib]
+
+lean_lib Dynlib where
+  -- no special settings needed
+
+lean_exe dynlib where
+  root := `Main
+  moreLinkArgs := #["-Llib", "-lmylib"]
diff --git a/test/dynlib/lean-toolchain b/test/dynlib/lean-toolchain
new file mode 100644
index 00000000..2c6e1c4b
--- /dev/null
+++ b/test/dynlib/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.22.0-rc4
diff --git a/test/dynlib/success.in b/test/dynlib/success.in
new file mode 100644
index 00000000..a1a080c9
--- /dev/null
+++ b/test/dynlib/success.in
@@ -0,0 +1,5 @@
+{ "cmd": "import Dynlib" }
+
+{"env": 0}
+
+{ "cmd": "#eval add 2 2", "env": 0 }
diff --git a/test/dynlib/test.sh b/test/dynlib/test.sh
new file mode 100644
index 00000000..93772da4
--- /dev/null
+++ b/test/dynlib/test.sh
@@ -0,0 +1,20 @@
+#!/bin/bash
+
+set -e
+
+REPL_BIN="../../.lake/build/bin/repl"
+DYNLIB_PATH="lib/libmylib.so"
+INPUT_FILE="success.in"
+
+echo "Running test with dynamic library: $DYNLIB_PATH"
+
+# Create a temp file for output
+tmpfile=./dynlib.out
+
+# Run REPL with dynlib and input, dump output to temp file
+lake env "$REPL_BIN" --dynlib "$DYNLIB_PATH" < "$INPUT_FILE" > "$tmpfile" 2>&1
+
+cat "$tmpfile"
+
+# Optionally remove temp file (comment out if you want to keep)
+# rm "$tmpfile"

From 3a04d004d088cec73c7a59064bab8dc721b827a3 Mon Sep 17 00:00:00 2001
From: FrederickPu <pufrederick51@gmail.com>
Date: Fri, 25 Jul 2025 19:50:02 -0400
Subject: [PATCH 4/4] improved dynlib test setup

---
 test/dynlib/CMakeLists.txt | 25 +++++++++++++++++++++++--
 test/dynlib/Dynlib.lean    |  2 ++
 test/dynlib/lakefile.lean  | 14 +++++++++++---
 test/dynlib/lean-toolchain |  2 +-
 4 files changed, 37 insertions(+), 6 deletions(-)
 create mode 100644 test/dynlib/Dynlib.lean

diff --git a/test/dynlib/CMakeLists.txt b/test/dynlib/CMakeLists.txt
index 73f0a441..11efc973 100644
--- a/test/dynlib/CMakeLists.txt
+++ b/test/dynlib/CMakeLists.txt
@@ -1,9 +1,30 @@
 cmake_minimum_required(VERSION 3.15)
 project(mylib C)
 
-# Put your actual path here from step 1
-set(LEAN_INCLUDE_DIR "/home/codespace/.elan/toolchains/leanprover--lean4---v4.22.0-rc4/include")
+# Default elan base directory (adjust if your elan is elsewhere)
+set(ELAN_BASE_DIR "$ENV{HOME}/.elan/toolchains")
+
+# Try to read lean-toolchain file (simple read first line)
+file(READ "${CMAKE_SOURCE_DIR}/lean-toolchain" LEAN_TOOLCHAIN_CONTENT)
+string(STRIP "${LEAN_TOOLCHAIN_CONTENT}" LEAN_TOOLCHAIN_CONTENT)
+
+# Extract version after colon, e.g. leanprover/lean4:v4.21.0  --> v4.21.0
+string(REGEX MATCH "v[0-9]+\\.[0-9]+\\.[0-9]+" LEAN_VERSION "${LEAN_TOOLCHAIN_CONTENT}")
+
+message("${LEAN_VERSION}")
+
+
+set(LEAN_TOOLCHAIN_DIR "${ELAN_BASE_DIR}/leanprover--lean4---${LEAN_VERSION}")
+message(STATUS "Using Lean toolchain: ${LEAN_TOOLCHAIN_DIR}")
+
+set(LEAN_INCLUDE_DIR "${LEAN_TOOLCHAIN_DIR}/include")
+set(LEAN_LIBRARY_DIR "${LEAN_TOOLCHAIN_DIR}/lib")
 
 include_directories(${LEAN_INCLUDE_DIR})
+link_directories(${LEAN_LIBRARY_DIR})
 
 add_library(mylib SHARED mylib.c)
+
+set_target_properties(mylib PROPERTIES
+    LIBRARY_OUTPUT_DIRECTORY "${CMAKE_SOURCE_DIR}/.lake/build/lib"
+)
\ No newline at end of file
diff --git a/test/dynlib/Dynlib.lean b/test/dynlib/Dynlib.lean
new file mode 100644
index 00000000..415c31e1
--- /dev/null
+++ b/test/dynlib/Dynlib.lean
@@ -0,0 +1,2 @@
+@[extern "l_add"]
+opaque add : UInt32 → UInt32 → UInt32
diff --git a/test/dynlib/lakefile.lean b/test/dynlib/lakefile.lean
index 9723e286..4cc63acc 100644
--- a/test/dynlib/lakefile.lean
+++ b/test/dynlib/lakefile.lean
@@ -3,11 +3,19 @@ open Lake DSL
 
 package dynlib where
   name := "dynlib"
-  defaultTargets := #[`dynlib]
+  preferReleaseBuild := true
 
+-- Define a target representing the prebuilt shared library
+target mylib pkg : Dynlib := do pure $ Job.pure {
+  path := pkg.sharedLibDir / nameToSharedLib "mylib"
+  name := "mylib"
+}
+
+@[default_target]
 lean_lib Dynlib where
-  -- no special settings needed
+  precompileModules := true
+  moreLinkLibs := #[mylib]
 
 lean_exe dynlib where
   root := `Main
-  moreLinkArgs := #["-Llib", "-lmylib"]
+  moreLinkLibs := #[mylib]
diff --git a/test/dynlib/lean-toolchain b/test/dynlib/lean-toolchain
index 2c6e1c4b..980709bb 100644
--- a/test/dynlib/lean-toolchain
+++ b/test/dynlib/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.22.0-rc4
+leanprover/lean4:v4.21.0