Add README section

README.md

@@ -118,6 +118,24 @@ Pickling is quite efficient:
 * file sizes are generally small, but see https://github.com/digama0/leangz if compression is
   desirable
 
+## Using the REPL from another project
+
+Set up your project as usual using `lake new` or `lake init`
+(or the interactive setup GUI available via the VSCode extension under the `∀` menu).
+
+In that project, add `require` statements in the `lakefile.lean` for any dependencies you need
+(e.g. Mathlib). (You probably should verify that `lake build` works as expected in that project.)
+
+Now you can run the REPL as:
+```shell
+lake env ../path/to/repl/.lake/build/bin/repl < commands.in
+```
+(Here `../path/to/repl/` represents the path to your checkout of this repository,
+in which you've already run `lake build`.)
+
+The `lake env` prefix sets up the environment associated to your local project, so that the REPL
+can find needed imports.
+
 ## Future work
 
 * Replay tactic scripts from tactic mode back into the original `sorry`.

lakefile.lean

@@ -12,4 +12,4 @@ lean_lib REPL {
 @[default_target]
 lean_exe repl where
   root := `REPL.Main
-  supportInterpreter := true
+  supportInterpreter := true

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.4.0-rc1
+leanprover/lean4-pr-releases:pr-release-3071

test/Mathlib/lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "baf6defee1fe881ae535519c0776f37f6ef08603",
+   "rev": "16d8352f7ed0d38cbc58ace03b3429d693cf50c6",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,10 +49,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "561ab0981d6df710afb3d34423378152195e3440",
+   "rev": "0540b2bc8a2a85e314e1e9329722a549b31496d7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "nightly-testing-2023-12-14",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "«repl-mathlib-tests»",

test/Mathlib/lakefile.lean

@@ -3,7 +3,7 @@ open Lake DSL
 
 package «repl-mathlib-tests» where
   -- add package configuration options here
-  require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "master"
+  require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "nightly-testing-2023-12-14"
 
 lean_lib «ReplMathlibTests» where
   -- add library configuration options here

test/Mathlib/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.4.0-rc1
+leanprover/lean4-pr-releases:pr-release-3071