feat: add supportInterpreter config setting

also don't use `--export-all` on Windows anymore

Lake/Package.lean

@@ -286,6 +286,18 @@ structure PackageConfig extends WorkspaceConfig where
   -/
   moreLibTargets : Array FileTarget := #[]
 
+  /--
+    Whether to expose symbols within the executable to the Lean interpreter.
+    This allows the executable to interpret Lean files (e.g.,  via
+    `Lean.Elab.runFrontend`).
+
+    Implementation-wise, this passes `-rdynamic` to the linker when building
+    on non-Windows systems.
+
+    Defaults to `false`.
+  -/
+  supportInterpreter : Bool := false
+
   /--
     Additional arguments to pass to `leanc`
       while compiling the package's binary executable.
@@ -476,9 +488,16 @@ def binFile (self : Package) : FilePath :=
 def moreLibTargets (self : Package) : Array FileTarget :=
   self.config.moreLibTargets
 
-/-- The package's `moreLinkArgs` configuration. -/
+/-- The package's `supportInterpreter` configuration. -/
+def supportInterpreter (self : Package) : Bool :=
+  self.config.supportInterpreter
+
+/-- `-rdynamic` (if non-Windows and `supportInterpreter`) plus `moreLinkArgs` -/
 def moreLinkArgs (self : Package) : Array String :=
-  self.config.moreLinkArgs
+  if self.supportInterpreter && !Platform.isWindows then
+    #["-rdynamic"] ++ self.config.moreLinkArgs
+  else
+    self.config.moreLinkArgs
 
 /-- Whether the given module is in the package. -/
 def hasModule (mod : Name) (self : Package) : Bool :=

README.md

@@ -116,6 +116,7 @@ Workspace options are shared across a package and its dependencies.
 * `binDir`: The build subdirectory to which Lake should output the package's binary executable. Defaults to `bin`.
 * `binRoot`: The root module of the package's binary executable. Defaults to `Main`. The root is built by recursively building its local imports (i.e., fellow modules of the package). This setting is most useful for packages that are distributing both a library and a binary (like Lake itself). In such cases, it is common for there to be code (e.g., `main`) that is needed for the binary but should not be included in the library proper.
 * `moreLibTargets`: An `Array` of additional library `FileTarget`s (beyond the package's and its dependencies' libraries) to build and link to the package's binary executable (and/or to dependent package's executables).
+* `supportInterpreter`: Whether to expose symbols within the executable to the Lean interpreter. This allows the executable to interpret Lean files (e.g., via `Lean.Elab.runFrontend`). Implementation-wise, this passes `-rdynamic` to the linker when building on a non-Windows systems. Defaults to `false`.
 * `moreLinkArgs`: An `Array` of additional arguments to pass to `leanc` while compiling the package's binary executable. These will come *after* the paths of libraries built with `moreLibTargets`.
 
 ## Scripts

build.sh

@@ -1,6 +1,6 @@
 #!/usr/bin/env sh
 if [ "$OS" = "Windows_NT" ]; then
-  LINK_OPTS=-Wl,--export-all
+  LINK_OPTS=
 else
   LINK_OPTS=-rdynamic
 fi

examples/bootstrap/lakefile.lean

@@ -4,8 +4,4 @@ open System Lake DSL
 package lake where
   srcDir := FilePath.mk ".." / ".."
   binRoot := `Lake.Main
-  moreLinkArgs :=
-    if Platform.isWindows then
-      #["-Wl,--export-all"]
-    else
-      #["-rdynamic"]
+  supportInterpreter := true

lakefile.lean

@@ -3,8 +3,4 @@ open System Lake DSL
 
 package lake where
   binRoot := `Lake.Main
-  moreLinkArgs :=
-    if Platform.isWindows then
-      #["-Wl,--export-all"]
-    else
-      #["-rdynamic"]
+  moreLinkArgs := if Platform.isWindows then #[] else #["-rdynamic"]