Mininix is a smaller version of the Nix expression language. This codebase provides the mechanization of the semantics and reference interpreter for this language in the Coq proof assistant. For more details, I refer to my bachelor's thesis. It should be linked to from the related work section of the Zenodo record after it has been made available on the thesis archive page of iCIS.
During my thesis, I used Nix to manage my Coq installation. If you use Nix, it should be easy to build/check the codebase. If not, this might be a bit more tricky.
There are two things that you need to have installed. The current flake.lock
ensures that we have the following software:
- Coq, version 8.19.2.
- Coq-std++, version 1.10.0.
I have attached a flake.nix and flake.lock file, which should make my setup
reproducible. Assuming a working Nix installation with flake support and the
Nix command enabled, simply running nix develop should give you a shell where
the right Coq and Coq-std++ versions available.
If you have a working direnv installation, simply
running direnv allow (after inspecting the .envrc file) should make the
right version of Coq and Coq-std++ available.
If you are on some Unix-based system, there is a good chance that your package manager provides a Coq package. The Repology page should give you the information that you need.
You may be able to install Coq-std++ via opam, as described in the README of Coq-std++. However, your operating system's package repositories may also provide a package. Consider taking a look at the Repology pages: coq-stdpp, coq:stdpp.
Running make should run coqc on all files; assuming that you are using a
compatible Coq version, this should successfully check all proofs.