Kenji Maillard (Jul 19 2022 at 12:16): 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";
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.
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.
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!
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.
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.
Notification Bot (Sep 19 2022 at 09:29):Kenji Maillard has marked this topic as resolved.
Last updated: Oct 12 2024 at 13:01 UTC