aboutsummaryrefslogtreecommitdiffstats
path: root/README.md
diff options
context:
space:
mode:
authorLibravatar Rutger Broekhoff2024-06-27 02:03:05 +0200
committerLibravatar Rutger Broekhoff2024-06-27 02:03:05 +0200
commitba973b2fa09e0ff203eec9770908a88e0ccfde70 (patch)
tree0ca3da4b8fc74202084a89581dd3f72ed30bb787 /README.md
parent4598e77a9406d8040357c943a05dd1ab939932db (diff)
downloadmininix-formalization-ba973b2fa09e0ff203eec9770908a88e0ccfde70.tar.gz
mininix-formalization-ba973b2fa09e0ff203eec9770908a88e0ccfde70.zip
Update README
Diffstat (limited to 'README.md')
-rw-r--r--README.md24
1 files changed, 15 insertions, 9 deletions
diff --git a/README.md b/README.md
index 125ea10..861b848 100644
--- a/README.md
+++ b/README.md
@@ -16,6 +16,12 @@ During my thesis, I used Nix to manage the Coq installation for this thesis.
16If you use Nix, it should be easy to build/check the codebase. If not, this 16If you use Nix, it should be easy to build/check the codebase. If not, this
17might be a bit more tricky. 17might be a bit more tricky.
18 18
19There are two things that you need to have installed. The current `flake.lock`
20ensures 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
21I have attached a `flake.nix` and `flake.lock` file, which should make my setup 27I 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
23Nix command enabled, simply running `nix develop` followed by `make` should run 29Nix 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/)
25installation, simply running `direnv allow` (after inspecting the `.envrc` 31installation, simply running `direnv allow` (after inspecting the `.envrc`
26file) should make the right version of Coq available. 32file) should make the right version of Coq and Coq-std++ available.
27 33
28### Without Nix 34### Without Nix
29 35
30There are two things you need to have available. The current `flake.lock` 36If you are on some Unix-based system, there is a good chance that your package
31ensures that we have the following software: 37manager provides a Coq package. [The Repology
38page](https://repology.org/project/coq/versions) should give you the
39information that you need.
32 40
33- Coq, version 8.19.2. 41You 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. 42Coq-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 43provide a package. Consider taking a look at [the Repology
36 Coq-std++. However, your operating system's package repositories may also 44page](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).