Skip to content

Commit 6d1b1fb

Browse files
committed
Add README section
1 parent 0ed7cfc commit 6d1b1fb

File tree

1 file changed

+18
-0
lines changed

1 file changed

+18
-0
lines changed

README.md

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -118,6 +118,24 @@ Pickling is quite efficient:
118118
* file sizes are generally small, but see https://github.com/digama0/leangz if compression is
119119
desirable
120120

121+
## Using the REPL from another project
122+
123+
Set up your project as usual using `lake new` or `lake init`
124+
(or the interactive setup GUI available via the VSCode extension under the `` menu).
125+
126+
In that project, add `require` statements in the `lakefile.lean` for any dependencies you need
127+
(e.g. Mathlib). (You probably should verify that `lake build` works as expected in that project.)
128+
129+
Now you can run the REPL as:
130+
```shell
131+
lake env ../path/to/repl/.lake/build/bin/repl < commands.in
132+
```
133+
(Here `../path/to/repl/` represents the path to your checkout of this repository,
134+
in which you've already run `lake build`.)
135+
136+
The `lake env` prefix sets up the environment associated to your local project, so that the REPL
137+
can find needed imports.
138+
121139
## Future work
122140

123141
* Replay tactic scripts from tactic mode back into the original `sorry`.

0 commit comments

Comments
 (0)