diff options
author | Rutger Broekhoff | 2024-06-27 02:03:05 +0200 |
---|---|---|
committer | Rutger Broekhoff | 2024-06-27 02:03:05 +0200 |
commit | ba973b2fa09e0ff203eec9770908a88e0ccfde70 (patch) | |
tree | 0ca3da4b8fc74202084a89581dd3f72ed30bb787 /README.md | |
parent | 4598e77a9406d8040357c943a05dd1ab939932db (diff) | |
download | mininix-formalization-ba973b2fa09e0ff203eec9770908a88e0ccfde70.tar.gz mininix-formalization-ba973b2fa09e0ff203eec9770908a88e0ccfde70.zip |
Update README
Diffstat (limited to 'README.md')
-rw-r--r-- | README.md | 24 |
1 files changed, 15 insertions, 9 deletions
@@ -16,6 +16,12 @@ During my thesis, I used Nix to manage the Coq installation for this thesis. | |||
16 | If you use Nix, it should be easy to build/check the codebase. If not, this | 16 | If you use Nix, it should be easy to build/check the codebase. If not, this |
17 | might be a bit more tricky. | 17 | might be a bit more tricky. |
18 | 18 | ||
19 | There are two things that you need to have installed. The current `flake.lock` | ||
20 | ensures that we have the following software: | ||
21 | |||
22 | - Coq, version 8.19.2. | ||
23 | - [Coq-std++](https://gitlab.mpi-sws.org/iris/stdpp), version 1.10.0. | ||
24 | |||
19 | ### Using Nix | 25 | ### Using Nix |
20 | 26 | ||
21 | I have attached a `flake.nix` and `flake.lock` file, which should make my setup | 27 | I have attached a `flake.nix` and `flake.lock` file, which should make my setup |
@@ -23,16 +29,16 @@ reproducible. Assuming a working Nix installation with flake support and the | |||
23 | Nix command enabled, simply running `nix develop` followed by `make` should run | 29 | Nix command enabled, simply running `nix develop` followed by `make` should run |
24 | `coqc` on all files. If you have a working [direnv](https://direnv.net/) | 30 | `coqc` on all files. If you have a working [direnv](https://direnv.net/) |
25 | installation, simply running `direnv allow` (after inspecting the `.envrc` | 31 | installation, simply running `direnv allow` (after inspecting the `.envrc` |
26 | file) should make the right version of Coq available. | 32 | file) should make the right version of Coq and Coq-std++ available. |
27 | 33 | ||
28 | ### Without Nix | 34 | ### Without Nix |
29 | 35 | ||
30 | There are two things you need to have available. The current `flake.lock` | 36 | If you are on some Unix-based system, there is a good chance that your package |
31 | ensures that we have the following software: | 37 | manager provides a Coq package. [The Repology |
38 | page](https://repology.org/project/coq/versions) should give you the | ||
39 | information that you need. | ||
32 | 40 | ||
33 | - Coq, version 8.19.2. | 41 | You may be able to install Coq-std++ via opam, as described in the README of |
34 | - [Coq-std++](https://gitlab.mpi-sws.org/iris/stdpp), version 1.10.0. | 42 | Coq-std++. However, your operating system's package repositories may also |
35 | You may be able to install Coq-std++ via opam, as described in the README of | 43 | provide a package. Consider taking a look at [the Repology |
36 | Coq-std++. However, your operating system's package repositories may also | 44 | page](https://repology.org/project/coq-stdpp/versions). |
37 | provide a package. Consider taking a look at [the Repology | ||
38 | page](https://repology.org/project/coq-stdpp/packages). | ||