This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
These are instructions to install UniMath on a Unix-like system using the Nix Package Manager.
This method has some advantages:
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.
$ 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.)
$ 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.)
$ git clone https://github.com/UniMath/UniMath.git
$ cd UniMath
$ make
Once the building is finished, you can quit the nix-shell (type exit
).
$ nix-env -i emacs
(Or skip this step if you have emacs already installed.)
If you want to uninstall UniMath and OCaml to reclaim disk space:
$ rm -rf UniMath
$ nix-collect-garbage
If you want to uninstall the Nix Package Manager directly, consult the Nix Manual.