Coq package questions

[Zimmi48]

Hello @vbgl and others,

I have a couple of remarks on the Coq packages in the repositories.

Why is the default, coq-8.4pl6 ? Shouldn't the default be the last stable version coq-8.5pl1 ?

Is there any sense to keep a package pointing to the development version if this package needs to be updated by hand for each new commit? It hasn't been updated since 2014 by the way so nixpkgs.coq_8_5 is more advanced than nixpkgs.coq_HEAD.

Cheers,
Théo

[yacinehmito]

Has this been answered?

[Zimmi48]

No it hasn't.
I closed it because this is not a real problem and it only resulted in a higher number of unsolved issues on the issue tracker.
I still think that the default coq derivation should be the latest stable version.
However, for the way coq_HEAD is managed, this seems to be quite standard and a more pervasive issue of the general Nix package management model.

[Zimmi48]

@jwiegley @roconnor @thoughtpolice Now that Coq version 8.6 has been released and included in nixpkgs (commit 838a3b4), I'm asking these questions again:

• Isn't it time to switch to a more recent stable version as the default? I would now be in favor of switching directly to Coq 8.6.
• Isn't it time to remove the more than out-of-date coq_HEAD? It made sense at the time to have it but since then, Coq has switched to a faster release cycle so it doesn't make sense to keep it now.

[jwiegley]

Hi @Zimmi48, most libraries (especially mathcomp and ssreflect) do not have 8.6 compatible versions yet, so switching the default would mean a newer Coq with no libraries. I think we should wait until at least the most commonly used libraries catch up, and then we can switch.

Removing coq_HEAD is fine with me. I can always build that as a local expression anyway, so I'm fine if it's not part of what we offer.

[Zimmi48]

OK waiting a bit longer seems like a good plan then.

[Zimmi48]

Hi @jwiegley, MathComp/SSReflect 8.6 compatible versions have now been released but you probably know other widely used libraries which have not been ported yet. Do you have a list in mind which we could track to know when to switch?

[jwiegley]

Those are really the main ones. I'm sad that QuickChick is slow to update, and tlc and unimath probably have a lot of users too, but 8.5 didn't wait for those etiher. As long as there's a clear way to stay on 8.5, I guess it's OK then to make 8.6 the default.

[jwiegley]

@Zimmi48 I'm working on the 8.6 transition now, stay tuned.

[jwiegley]

8.6 is now the default, although mathcomp still doesn't build with it. I've contacted Enrico Tassi for assistance, and will get it fixed ASAP.

[Zimmi48]

Any progress on making mathcomp compile with Coq 8.6?

[jwiegley]

No, for the time being I just backed out the dependency on it.

[Zimmi48]

Sorry, which dependency did you backed out?

[jwiegley]

That coq implies coq_8_6. I switched it back to where it had been before.

[jwiegley]

Note also that my discussions with Enrico revealed that it might be a Nix issue. Here's my dialog with him:

I'm trying to package this release for Nix, but I'm getting an error quite error in the build process when using Coq 8.6:

> CAMLC -pp -c ssreflect.ml4
> findlib: [WARNING] cannot read directory /dev/null: Not a directory
> Redundant [TYPED AS] clause in [ARGUMENT EXTEND ssrindex].
> File "ssreflect.ml4", line 670, characters 21-26:
> Error: Unbound module Gramext
> Did you mean Gram?

He writes:

Hard to say.  Could be no .cmi file from Coq compilation installed, or
camlp5 missing/not in path.  Try calling
  make H=
or 
  make -f Makefile.coq VERBOSE=1
so that the commands are printed verbosely

I confirm that camlp5 is on the path: Camlp5 version 6.17 (ocaml 4.01.0)

Here I've used OPAM to intall Coq 8.6 and its deps:

gares@gargamel:~$ find opam-coq.8.6.0/ -name gramext\*
opam-coq.8.6.0/system/lib/camlp5/gramext.cmi
opam-coq.8.6.0/system/lib/camlp5/gramext.mli
opam-coq.8.6.0/system/lib/camlp5/gramext.cmx

where opam-coq.8.6.0/ is the opam root.

Interesting, I have these two files, but not the .mli:

/nix/store/8640hpgpfqsw2xzn5w2qsipiz7211f38-camlp5_transitional-6.17/lib/ocaml/4.01.0/site-lib/camlp5/gramext.cmi
/nix/store/8640hpgpfqsw2xzn5w2qsipiz7211f38-camlp5_transitional-6.17/lib/ocaml/4.01.0/site-lib/camlp5/gramext.cmx

Is it the missing .mli that's the problem, or the location of these files, do you think?

compilation must find the cm* via -I flags.

[vbgl]

Thanks for your investigation, John! The fix seems rather simple: just add findlib to the build inputs. Let me merge #21879 and I’ll do it.

[vbgl]

Done in 42bf99e: mathcomp is now available in Nixpkgs for 8.4, 8.5 and 8.6.

[Zimmi48]

Thanks a lot @jwiegley and @vbgl! If math-comp now builds fine with Coq 8.6, it could make sense to finally make it the default version (what coq attribute name links to).
Besides, I think that math-comp 1.6.1 is supposed to work fine with Coq 8.4, 8.5 and 8.6 so it could also make sense to use the same version in all cases.

[Zimmi48]

@vbgl Loading Coq 8.6 with mathcomp, with nix-shell -p coqPackages_8_6.mathcomp --run coqide I can evaluate Require Import mathcomp.ssreflect.ssrbool. without a problem but Require Import mathcomp.algebra.ssrnum. gives me the error:

Error:
Compiled library mathcomp.algebra.ssrnum (in file /nix/store/x79bd0bkcx017da93vbhrvamcp878w7k-coq8.6-mathcomp-1.6.1/lib/coq/8.6/user-contrib/mathcomp/algebra/ssrnum.vo) makes inconsistent assumptions over library mathcomp.ssreflect.ssreflect

Do you observe the same problem?

[vbgl]

Yes. Apologies for the overstatement: I’ve only fixed the build.

[Zimmi48]

No problem. I don't even know if this error is new or ancient.

[jwiegley]

I don't have any real preference over what the default Coq version is. I know that fiat doesn't build with it yet, but since the user can always choose an explicit version, we can make the default 8.6.

[Zimmi48]

I have a preference for encouraging people to use the latest version.
But I suppose we first need to fix this issue I just found.

[vbgl]

A tentative fix of mathcomp is to be found in PR #22223. Testers welcome :-)

[Zimmi48]

Hi again! I'm not really aware of NixOS development practices but I suppose that the feature freeze for 17.03 will happen soon (I suppose that it hasn't yet since there is no 17.03 branch). If I'm right, now might be the time to update the default Coq version in nixpkgs. Otherwise we will have one more release with a default version of Coq (8.4) that starts to be quite old...

[Zimmi48]

The default is now 8.6.