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

chore: Nix: simplify package instructions

Browse source
This commit is contained in:
Sebastian Ullrich 2021-12-04 12:14:47 +01:00
parent 171624d7a7
commit 45917f2f90
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
doc/setup.md
View file

@ -75,11 +75,9 @@ Note: Your system Nix might print warnings about not knowing some of the setting
From a Lean shell, run
```bash
$ nix flake new mypkg -t github:leanprover/lean4
$ cd mypkg && git init && git add flake.nix
```
to create a new Lean package in directory `mypkg` using the latest commit of Lean 4.
Note that Nix Flakes will not recognize your `flake.nix` file unless it is visible to Git.
Such packages follow the same directory layout as described in the basic setup above, except for a `leanpkg.toml` replaced by a `flake.nix` file set up so you can run Nix commands on it, for example:
Such packages follow the same directory layout as described in the basic setup above, except for a `leanpkg.toml`/`lakefile.lean` replaced by a `flake.nix` file set up so you can run Nix commands on it, for example:
```bash
$ nix build # build package and all dependencies
$ nix build .#executable # compile `main` definition into executable (after you've added one)
@ -88,6 +86,7 @@ $ nix run .#emacs-dev MyPackage.lean # arguments can be passed as well, e.g. th
$ nix run .#vscode-dev MyPackage.lean # ditto, using VS Code
```
Note that if you rename `MyPackage.lean`, you also have to adjust the `name` attribute in `flake.nix` accordingly.
Also note that if you turn the package into a Git repository, only tracked files will be visible to Nix.
As in the basic setup, changes need to be saved to be visible in other files, which have then to be invalidated via an editor command.