0

I am using Coq (versions 8.5-6), installed w/ Nix. I want to install ssreflect, preferably also w/ Nix. The only information I found about this is here. However, this is not about installing ssreflect, merely trying it out. Nevertheless, I tried to try it out, but ended up w/ hundreds of warnings (about the contents of various .v and .ml4 files) and couldn't wait for the process to end. A fairly typical warning looked like this:

File "./algebra/ssralg.v", line 856, characters 0-39: Warning: Implicit Arguments is deprecated; use Arguments instead

So the question: How on earth do I install ssreflect w/ Nix?

EDIT: After reading ejgallego's comments, it seems it may be impossible to install ssreflect w/ Nix -- esp. if one wants install only ssreflect w/out the other modules (fingroup, algebra, etc.). So I've also the following question:

Would the standard Opam or make install installation of ssreflect work w/ a Nix-installed Coq?

jaam
  • 900
  • 4
  • 23
  • 2
    These warnings are sadly normal as the developers have not fixed them. ssreflect takes a looong time to build, in particular if you want to build the whole package and its many libraries. You can either edit ssreflect's Make to remove some libraries, or just split the package up. It depends on your needs, for instance, OPAM distributes math-comp as 5 separate packages due to its size. – ejgallego Jun 09 '17 at 21:44
  • 1
    If you plan to use only the tactics plugin, it is included in Coq 8.7, however note that the tactics are really not very useful without at least its main library. – ejgallego Jun 09 '17 at 21:44

1 Answers1

2

There are a few things that you need to be aware of:

  • Nix is a source-based package manager with a binary cache. A lot of packages are pre-built and available in the binary cache, thus their installation doesn't take long; some packages (in particular development libraries) are not pre-built and Nix, when installing them will take the time it needs to compile them. Please be patient: you will only need to wait for the full compilation the first time (and yes, math-comp emits lots of warning upon compilation); next times, the package will be already available in your local Nix store.

  • Since OPAM is also source-based, using OPAM instead of Nix won't make you save time. You can't mixup Nix-installed Coq with OPAM installed SSReflect because the latter will want the former as an OPAM dependency.

  • The Nix way to use libraries is not to install them but to load them with nix-shell instead. nix-shell will "install" the libraries and set some environment variables for you (e.g. $COQPATH in this case).

  • You can also compile the package from source yourself using a Nix-installed Coq but you cannot run make install because this would try to install SSReflect at the same place where Coq is installed but the Nix store is non-mutable. Instead you could skip this step, and set up $COQPATH manually.

  • Indeed, the compilation of the full math-comp takes very long. There is a Coq ssreflect package which is lighter. You can get it using: 

    nix-shell -p coqPackages_8_6.ssreflect
Zimm i48
  • 2,901
  • 17
  • 26
  • "The Nix way to use libraries is not to install them but to load them with nix-shell instead." Thanks, this explains a lot – jaam Jun 11 '17 at 15:52
  • It took me a long time to understand this. In the case of Coq in particular because I'm not used thinking about it as a programming language. – Zimm i48 Jun 11 '17 at 15:54
  • I have a [new question](https://stackoverflow.com/questions/44553350/nix-querying-packages-packages) related to this – jaam Jun 14 '17 at 20:37