Stream: Nix toolbox devs & users

Topic: ✔ nix pkg for equations 1.3 and coq8.16


view this post on Zulip Kenji Maillard (Jul 19 2022 at 12:16):

I tried to add the latest release of equations for coq 8.16 to the nixpkgs (see diff below), but it seem to fail on my computer:

 ~/W/G/nixpkgs > nix-build -K -A coqPackages_8_16.equations
this derivation will be built:
  /nix/store/wwq8xl4m0d7a4a7cp96fqzdnxgqpwbrv-coq8.16-equations-1.3+8.16.drv
building '/nix/store/wwq8xl4m0d7a4a7cp96fqzdnxgqpwbrv-coq8.16-equations-1.3+8.16.drv'...
unpacking sources
unpacking source archive /nix/store/m1xz2h9pq26hmh5k9g78g3aa75hr0r8k-source
source root is source
patching sources
configuring
no configure script, doing nothing
building
build flags: -j8 -l8 SHELL=/nix/store/3j18grljsyy4nxc078g00sy4cx6cf16g-bash-5.1-p16/bin/bash
COQDEP VFILES
COQPP src/g_equations.mlg
CAMLDEP src/extra_tactics.mli
CAMLDEP src/noconf.mli
CAMLDEP src/noconf_hom.mli
CAMLDEP src/equations.mli
CAMLDEP src/principles.mli
CAMLDEP src/principles_proofs.mli
CAMLDEP src/covering.mli
CAMLDEP src/splitting.mli
CAMLDEP src/simplify.mli
CAMLDEP src/syntax.mli
CAMLDEP src/context_map.mli
CAMLDEP src/depelim.mli
CAMLDEP src/eqdec.mli
CAMLDEP src/subterm.mli
CAMLDEP src/sigma_types.mli
CAMLDEP src/ederive.mli
CAMLDEP src/equations_common.mli
OCAMLLIBDEP src/equations_plugin.mllib
CAMLDEP src/extra_tactics.ml
CAMLDEP src/noconf.ml
CAMLDEP src/noconf_hom.ml
CAMLDEP src/equations.ml
CAMLDEP src/principles.ml
CAMLDEP src/principles_proofs.ml
CAMLDEP src/covering.ml
CAMLDEP src/splitting.ml
CAMLDEP src/simplify.ml
CAMLDEP src/context_map.ml
CAMLDEP src/syntax.ml
CAMLDEP src/depelim.ml
CAMLDEP src/eqdec.ml
CAMLDEP src/subterm.ml
CAMLDEP src/sigma_types.ml
CAMLDEP src/ederive.ml
CAMLDEP src/equations_common.ml
CAMLDEP src/g_equations.ml
*** Warning: in file theories/Init.v, declared ML module ./plugins/ltac/ltac_plugin has not been found!
cd test-suite && coq_makefile -f _CoqProject -o Makefile
cd examples && coq_makefile -f _CoqProject -o Makefile
Warning: No common logical root.
Warning: In this case the -docroot option should be given.
Warning: Otherwise the install-doc target is going to install files
Warning: in orphan_TestSuite_Equations
Warning: No common logical root.
Warning: In this case the -docroot option should be given.
Warning: Otherwise the install-doc target is going to install files
Warning: in orphan_Examples_Equations
CAMLC -c src/equations_common.mli
CAMLC -c src/ederive.mli
CAMLC -c src/subterm.mli
CAMLC -c src/noconf_hom.mli
CAMLC -c src/noconf.mli
CAMLC -c src/extra_tactics.mli
CAMLOPT -c  src/ederive.ml
CAMLOPT -c  src/equations_common.ml
CAMLC -c src/syntax.mli
CAMLC -c src/eqdec.mli
CAMLC -c src/context_map.mli
CAMLC -c src/depelim.mli
CAMLC -c src/sigma_types.mli
CAMLC -c src/simplify.mli
CAMLC -c src/splitting.mli
CAMLC -c src/covering.mli
CAMLC -c src/principles_proofs.mli
CAMLC -c src/equations.mli
CAMLC -c src/principles.mli
CAMLOPT -c  src/syntax.ml
CAMLOPT -c  src/eqdec.ml
CAMLOPT -c  src/extra_tactics.ml
CAMLOPT -c  src/context_map.ml
CAMLOPT -c  src/sigma_types.ml
File "src/sigma_types.ml", line 271, characters 2-43:
271 |   Extraction_plugin.Table.extraction_inline true
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module Extraction_plugin
make[1]: *** [Makefile:741: src/sigma_types.cmx] Error 2
make: *** [Makefile:409: all] Error 2
note: keeping build directory '/tmp/nix-build-coq8.16-equations-1.3+8.16.drv-1'
error: builder for '/nix/store/wwq8xl4m0d7a4a7cp96fqzdnxgqpwbrv-coq8.16-equations-1.3+8.16.drv' failed with exit code 2

Looks like a problem with ocaml paths/ocamlfind but I couldn't figure out what is actually wrong.
Does anyone encounter a similar issue ? Maybe @Matthieu Sozeau or @John Wiegley have an idea what could be happening.

Here's my local change to the nixpkgs:

diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/coq-modules/equations/default.nix
index 16b358b7377..a1fac90069c 100644
--- a/pkgs/development/coq-modules/equations/default.nix
+++ b/pkgs/development/coq-modules/equations/default.nix
@@ -6,6 +6,7 @@ with lib; mkCoqDerivation {
   repo = "Coq-Equations";
   inherit version;
   defaultVersion = switch coq.coq-version [
+    { case = "8.16"; out = "1.3+8.16"; }
     { case = "8.15"; out = "1.3+8.15"; }
     { case = "8.14"; out = "1.3+8.14"; }
     { case = "8.13"; out = "1.3+8.13"; }
@@ -51,6 +52,9 @@ with lib; mkCoqDerivation {
     release."1.3+8.14".sha256         = "19bj9nncd1r9g4273h5qx35gs3i4bw5z9bhjni24b413hyj55hkv";
     release."1.3+8.15".rev            = "v1.3-8.15";
     release."1.3+8.15".sha256         = "1vfcfpsp9zyj0sw0cwibk76nj6n0r6gwh8m1aa3lbvc0b1kbm32k";
+    release."1.3+8.16".rev            = "v1.3-8.16";
+    release."1.3+8.16".sha256         = "sha256-zyMGeRObtSGWh7n3WCqesBZL5EgLvKwmnTy09rYpxyE=";
+

   mlPlugin = true;
   preBuild = "coq_makefile -f _CoqProject -o Makefile";

view this post on Zulip John Wiegley (Jul 19 2022 at 15:44):

I have been using 8.16 yet under Nix, but I was able to get it working at some point. I didn't try with equations, however.

view this post on Zulip Théo Zimmermann (Jul 19 2022 at 15:59):

When such errors happen, this usually means that something is wrong in one of the dependencies (here I'm assuming Coq). If that's the case, I would expect SerAPI to also break, but I realize we haven't yet packaged the new SerAPI version for 8.16.

view this post on Zulip Vincent Laporte (Jul 24 2022 at 20:50):

That warning looks serious:

*** Warning: in file theories/Init.v, declared ML module ./plugins/ltac/ltac_plugin has not been found!

view this post on Zulip Théo Zimmermann (Jul 25 2022 at 07:16):

Indeed, and since this is Coq 8.16, that would be explained again by an issue with findlib not having registered the Coq libraries. But it's more surprising in this case that anything using Coq 8.16 works.

view this post on Zulip Vincent Laporte (Jul 25 2022 at 07:19):

I’ve managed to build equations for Coq 8.16. I’ll open a PR in nixpkgs.

view this post on Zulip Notification Bot (Sep 19 2022 at 09:29):

Kenji Maillard has marked this topic as resolved.


Last updated: May 19 2024 at 18:02 UTC