Using nix - math-comp/math-comp GitHub Wiki

Nix installation (pre-requisite for the rest)
Use mathcomp or extras with nix
Make your own package
Troubleshooting
More on this nix-shell

Nix installation

(pre-requisite for the rest)

To install it on a single-user unix system where you have admin rights, just type:
```
curl -L https://nixos.org/nix/install | sh
```
or
```
sh <(curl -L https://nixos.org/nix/install) --no-daemon
```
The --no-daemon option is for a single-user installation. (See the nix install manual for alternatives.)

You should run this under your usual user account, not as root. The script will invoke sudo as needed. See Troubleshooting in case of error.

For other configurations (in particular if multiple users share the machine) or for nix uninstallation, go to the appropriate section of the nix manual.
At the end of the installation, a message explains that several environment variables have to be set before you get a working environment. The simplest way to do so is to log out from your X session and log in again. See Troubleshooting if you prefer not to terminate your session.
This step (Nix installation) only need to be done once on a same machine.

To get most coq and mathcomp some packages faster, Setup nix once and for all:

nix-env -iA nixpkgs.cachix
cachix use coq
cachix use coq-community
cachix use math-comp

These steps only need to be done once on a same machine.

Use mathcomp or extras with nix

In any context, anywhere, now.

This provides a context with mathcomp and extra packages bigenough, finmap, multinomials, analysis and coqeal (if possible).

nix-shell https://github.com/math-comp/math-comp-nix/archive/v2.tar.gz

If you provided no more arguments the cached binaries and vo should be downloaded and you should be set quickly!

See more on this nix-shell.

In a directory containing a `default.nix` or `shell.nix` file.

nix-shell

This will download and build the required packages, wait until you get a shell.
You need to type this command every time you open a new terminal.

If a appropriate configuration files are present at the root of the directory, you should now be a in context where you can develop on the current library.

You are now in the correct work environment. You can run make and do whatever you are accustomed to do with Coq.

See Troubleshooting in case of error.

Here is an example:

Nix Example: Instantaneously work on a branch---Example of use of the nix toolchain in mathcomp

Install nix and setup cachix has explained above
Work!

TMP=$(mktemp -d) # or wherever you like
git clone -o upstream -b master https://github.com/math-comp/math-comp $TMP && cd $TMP
nix-shell --run cachedMake # Wait about one minute
nix-shell --run "emacs mathcomp/field/galois.v" # add "--arg withEmacs true" if you do not have emacs & PG installed

That's it!

In shell commands

Once inside a shell, to see your work environment (available packages):

command nixEnv or ppNixEnv
or call nix-shell with the option --arg print-env true

File edition with `emacs` or `coqide`

If you were already using emacs with proof general, make sure you empty your coq-prog-name variables and any other proof general options that used to be tied to a previous local installation of Coq.
Proof general will rely on the file _CoqProject, so you want to make sure that your .emacs configuration has not overwritten the coq-project-filename either.
If you do not have emacs installed, but want to use it, you can go back call nix-shell with the following option

nix-shell --arg withEmacs true in order to get a temporary installation of emacs and proof-general. Make sure you add (require 'proof-site) to your $HOME/.emacs.

Troubleshooting

Error when installing nix

You may experience errors when installing nix. If the installation stops with an error message similar to the following one

... installing 'nix-2.2.2' error: cloning builder process: Operation not permitted error: unable to start build process ...

it may be fixed by the following command (tested with Debian 9.9):

sudo sysctl kernel.unprivileged_userns_clone=1

Error when executing make

If the environment variable COQBIN is set, it is likely to point to the wrong binaries. If set, do:

export COQBIN=$(which coqtop | xargs dirname)/

Source without Logging out

Nix needs the user to set several environment variables and the nix installer appends a command for this purpose to the user's .profile. The Nix environment variables can actually be set from within any shell by sourcing the appropriate file:

. ${HOME}/.nix-profile/etc/profile.d/nix.sh

Make your own package

Locally

Download the latest default.nix

$ nix-shell https://github.com/math-comp/math-comp-nix/archive/v2.tar.gz --run generateNixDefault

Initialize a .nix/config.nix

$ nix-shell https://github.com/math-comp/math-comp-nix/archive/v2.tar.gz --run "initNixConfig YOURPACKAGENAME"

Edit .nix/config.nix following the recommendations inside

Sharing a package on nixpkgs

The design pattern changed, wait for this section to be updated or ask on zulip.

More on this nix-shell

Options

This nix-shell https://github.com/math-comp/math-comp-nix/archive/v2.tar.gz command could optionally take additional arguments:

--arg config   '{ attribute = your-package-name; }' # to specify your own package
--arg override '{ coq = "x.y"; mathcomp = "x.y.z"; }' # to change the versions of coq and mathcomp

if your arguments fall into the pre-cached configurations, the cached binaries and vo should be downloaded and you should be set within a minute!
if your-package-name is in pkgs.coqPackages in the currently used repository (cf https://github.com/math-comp/math-comp-nix/blob/master/default.nix#L2), it will use the derivation from there (including the currently known dependencies).
For mathcomp, instead of "x.y.z", you may use any branch name (e.g. "master") or a local path (e.g. ./. or ~/git/math-comp/your-local-branch or a pull request "#207")
You can also add to override the version, revision or path of other coq packages you would like to use. e.g. coqeal = "master"; or mathcomp-finmap = ~/git/finmap/your-local-branch; etc
You can also call nix-build instead of nix-shell to build a package instead of getting a context for it.

Examples

Get a shell for your local package my-package against the master version of finmap, with coq 8.10 and mathcomp 1.11.0.

nix-shell https://github.com/math-comp/math-comp-nix/archive/v2.tar.gz \
  --arg override  '{
      coq = "8.10"; 
      mathcomp = "1.11.0";
      mathcomp-finmap = "master";
    }' \
  --arg config '{ attribute = "my-package"; }'