diff options
| author |  Rutger Broekhoff | 2024-06-27 12:22:08 +0200 |
|---|---|---|
| committer | Rutger Broekhoff | 2024-06-27 12:22:08 +0200 |
| commit | 493678b8df4183e59884bf2069eb3b1bf8ebb07f (patch) | |
| tree | 82dfd515cab72b2d6e5fc21ae72e03f967bcafd8 | |
| parent | ff82f7c63616e96bdf8a4268212f8094fa69748d (diff) | |
| download | mininix-formalization-493678b8df4183e59884bf2069eb3b1bf8ebb07f.tar.gz mininix-formalization-493678b8df4183e59884bf2069eb3b1bf8ebb07f.zip | |
Update README
| -rw-r--r-- | README.md | 21 |
1 files changed, 14 insertions, 7 deletions
| @@ -12,9 +12,9 @@ the [thesis archive](https://www.cs.ru.nl/bachelors-theses/) page of | |||
| 12 | 12 | ||
| 13 | ## Development | 13 | ## Development |
| 14 | 14 | ||
| 15 | During my thesis, I used Nix to manage the Coq installation for this thesis. | 15 | During my thesis, I used Nix to manage my Coq installation. If you use Nix, it |
| 16 | If you use Nix, it should be easy to build/check the codebase. If not, this | 16 | should be easy to build/check the codebase. If not, this might be a bit more |
| 17 | might be a bit more tricky. | 17 | tricky. |
| 18 | 18 | ||
| 19 | There are two things that you need to have installed. The current `flake.lock` | 19 | There are two things that you need to have installed. The current `flake.lock` |
| 20 | ensures that we have the following software: | 20 | ensures that we have the following software: |
| @@ -26,10 +26,12 @@ ensures that we have the following software: | |||
| 26 | 26 | ||
| 27 | 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 |
| 28 | reproducible. Assuming a working Nix installation with flake support and the | 28 | reproducible. Assuming a working Nix installation with flake support and the |
| 29 | Nix command enabled, simply running `nix develop` followed by `make` should run | 29 | Nix command enabled, simply running `nix develop` should give you a shell where |
| 30 | `coqc` on all files. If you have a working [direnv](https://direnv.net/) | 30 | the right Coq and Coq-std++ versions available. |
| 31 | installation, simply running `direnv allow` (after inspecting the `.envrc` | 31 | |
| 32 | file) should make the right version of Coq and Coq-std++ available. | 32 | If you have a working [direnv](https://direnv.net/) installation, simply |
| 33 | running `direnv allow` (after inspecting the `.envrc` file) should make the | ||
| 34 | right version of Coq and Coq-std++ available. | ||
| 33 | 35 | ||
| 34 | ### Without Nix | 36 | ### Without Nix |
| 35 | 37 | ||
| @@ -43,3 +45,8 @@ Coq-std++. However, your operating system's package repositories may also | |||
| 43 | provide a package. Consider taking a look at the Repology pages: | 45 | provide a package. Consider taking a look at the Repology pages: |
| 44 | [coq-stdpp](https://repology.org/project/coq-stdpp/versions), | 46 | [coq-stdpp](https://repology.org/project/coq-stdpp/versions), |
| 45 | [coq:stdpp](https://repology.org/project/coq:stdpp/versions). | 47 | [coq:stdpp](https://repology.org/project/coq:stdpp/versions). |
| 48 | |||
| 49 | ## Building/checking | ||
| 50 | |||
| 51 | Running `make` should run `coqc` on all files; assuming that you are using a | ||
| 52 | compatible Coq version, this should successfully check all proofs. | ||