added ability to loadDynlib through command line flag

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

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

test/dynlib/.gitignore

@@ -0,0 +1 @@
+/.lake

test/dynlib/CMakeLists.txt

@@ -0,0 +1,30 @@
+cmake_minimum_required(VERSION 3.15)
+project(mylib C)
+
+# 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"
+)

test/dynlib/Dynlib.lean

@@ -0,0 +1,2 @@
+@[extern "l_add"]
+opaque add : UInt32 → UInt32 → UInt32

test/dynlib/Main.lean

@@ -0,0 +1,4 @@
+import Dynlib
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"

test/dynlib/README.md

@@ -0,0 +1 @@
+# dynlib

test/dynlib/fail.in

@@ -0,0 +1,3 @@
+{ "cmd": "@[extern \"add\"]\nopaque add' (a b : UInt32) : UInt32" }
+
+{ "cmd": "#eval add' 2 2", "env": 0 }

test/dynlib/lake-manifest.json

@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "dynlib",
+ "lakeDir": ".lake"}

test/dynlib/lakefile.lean

@@ -0,0 +1,21 @@
+import Lake
+open Lake DSL
+
+package dynlib where
+  name := "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
+  precompileModules := true
+  moreLinkLibs := #[mylib]
+
+lean_exe dynlib where
+  root := `Main
+  moreLinkLibs := #[mylib]

test/dynlib/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.21.0

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;
+}
+

test/dynlib/success.in

@@ -0,0 +1,5 @@
+{ "cmd": "import Dynlib" }
+
+{"env": 0}
+
+{ "cmd": "#eval add 2 2", "env": 0 }

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"