Using nix build with metacoq

Work In Progress

Setup

Step 1: Install nix

See https://nixos.org/download.html.

For MetaCoq development purpose, a single user installation is enough. On MacOS, you don't have a choice and must setup a multi-user installation.

Step 2: Setup cachix

$ nix-env -iA nixpkgs.cachix && cachix use coq && cachix use coq-community && cachix use metacoq

Step 3: Build your branch

Pull a MetaCoq branch with nix set up (the top directory should contain a default.nix file and a .nix subdirectory.

From the top directory of metacoq, enter a nix-environment (this will either download the CIed artifacts if they exists or build everything):

$ nix-shell

Then to retrieve the .vo artifacts built by the CI, run the following script (still from the top directory):

$ ./.nix/cachedMake.sh

Otherwise you can build locally with

$ nix-build

Step 4: Using an editor

Editors need to set up their environment variables correctly.

VSCode

From a nix-shell, running code .vscode/metacoq.code-workspace from the top directory seem to work well for a globally installed vscode/vscodium (not necessarily with nix).

Emacs

coq-nix-toolbox also comes with a --arg withEmacs true parameter that can be passed to nix-shell to bring in emacs (but paths might still need to be setup).

Configuration

The configuration is located in .nix/config.nix (in particular default coq and equations version for the current branch). See the documentation of coq-nix-toolbox.