max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: LSP setup using Nix

Browse source
This commit is contained in:
Sebastian Ullrich 2020-12-23 19:36:27 +01:00
parent f42bd8f693
commit d2b82bf563
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/make/nix.md
View file

@ -70,6 +70,8 @@ Starting a known-good (pinned) version of Emacs from the Lean shell with `lean4-
```bash
nix run .#emacs-dev
```
After adding `src/` as an LSP workspace using `lsp-workspace-folder-add`, it should automatically fall back to using stage 0 in there.
If you've already installed lean4-mode manually, you might need to first deactivate that. `elan` can be left as is on the other hand.
Arguments can be passed as well: