Building UniMath with Nix

Introduction

These are instructions to install UniMath on a Unix-like system using the Nix Package Manager.

This method has some advantages:

Should work both on Mac and on any major Linux distribution without any difference.
Does not require to install OCaml or Git or other dependencies separately (only Nix itself).
Does not interfere with or modify other software already present on the same system (other versions of OCaml, camlp5, etc).
It makes possible to uninstall cleanly all the software.

The main disadvantage of this method is that it is not the most used (see INSTALL.md) and it is not very well tested at the moment.

If you already have the Nix Package Manager installed, skip this step. Otherwise, type the following command to install Nix (as a user other than root):
```
$ curl https://nixos.org/nix/install | sh
```
Follow the instructions output by the script. The installation script requires that you have sudo access to root. (Go to the NixOS website to get more detailed instructions.)
Start a "nix-shell" with the following command:
```
$ nix-shell -p ocaml ocamlPackages.findlib ocamlPackages.camlp5 ocamlPackages.num gnumake git
```
(This may require some time to download and deploy the ocaml environment into the Nix storage.)
Clone UniMath, move to the top directory and launch the build:
```
$ git clone https://github.com/UniMath/UniMath.git
$ cd UniMath
$ make
```
Once the building is finished, you can quit the nix-shell (type exit).
You may also want to install emacs using Nix:
```
$ nix-env -i emacs
```
(Or skip this step if you have emacs already installed.)
Finally, you need to install Proof-General following the instructions on the website.

If you want to uninstall UniMath and OCaml to reclaim disk space:

If you want to uninstall the Nix Package Manager directly, consult the Nix Manual.