search

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes
MIT License
96 stars 21 forks source link

Difficulty packaging hierarchy-builder for Guix #320

Closed chipsf closed 1 year ago

chipsf commented 1 year ago

I'm packaging coq-mathcomp-analysis for Guix; the progress so far is here: https://issues.guix.gnu.org/58310.

When I try to build coq-mathcomp-hierarchy-builder (as a dependency for analysis), I get the following error (the "..." signifies a hash, just like in Nix, omitted for readability):

make[2]: Entering directory '/tmp/guix-build-coq-mathcomp-hierarchy-builder-1.4.0.drv-0/source'
COQDEP VFILES
COQC structures.v
File "./structures.v", line 18, characters 0-30:
Error:
Findlib error: coq-elpi.elpi not found in:
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/funind
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/btauto
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/micromega
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/ltac
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/nsatz
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/derive
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/cc
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/tauto
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/zify
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/ssrmatching
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/ssreflect
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/tutorial
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/tutorial/p0
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/tutorial/p3
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/tutorial/p1
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/tutorial/p2
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/extraction
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/firstorder
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/rtauto
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/ltac2
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/number_string_notation
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/plugins/ring
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib/coq-core/..
/gnu/store/...-coq-stdlib-8.16.0/lib/ocaml/site-lib/coq/user-contrib/Ltac2
/gnu/store/...-coq-stdlib-8.16.0/lib/ocaml/site-lib/coq/user-contrib/Ltac2
/gnu/store/...-coq-elpi-1.16.0/lib/coq/user-contrib/elpi
/gnu/store/...-coq-elpi-1.16.0/lib/coq/user-contrib/elpi/apps
/gnu/store/...-coq-elpi-1.16.0/lib/coq/user-contrib/elpi/apps/derive
/gnu/store/...-coq-elpi-1.16.0/lib/coq/user-contrib/elpi/apps/eltac
/gnu/store/...-coq-elpi-1.16.0/lib/coq/user-contrib/gnu
/gnu/store/...-coq-elpi-1.16.0/lib/coq/user-contrib/gnu/store
/gnu/store/...-coq-mathcomp-1.15.0/lib/coq/user-contrib/mathcomp
/gnu/store/...-coq-mathcomp-1.15.0/lib/coq/user-contrib/mathcomp/character
/gnu/store/...-coq-mathcomp-1.15.0/lib/coq/user-contrib/mathcomp/fingroup
/gnu/store/...-coq-mathcomp-1.15.0/lib/coq/user-contrib/mathcomp/solvable
/gnu/store/...-coq-mathcomp-1.15.0/lib/coq/user-contrib/mathcomp/algebra
/gnu/store/...-coq-mathcomp-1.15.0/lib/coq/user-contrib/mathcomp/ssreflect
/gnu/store/...-coq-mathcomp-1.15.0/lib/coq/user-contrib/mathcomp/all
/gnu/store/...-coq-mathcomp-1.15.0/lib/coq/user-contrib/mathcomp/field
/gnu/store/...-ocaml-4.14.0/lib/ocaml
/gnu/store/...-ocaml-findlib-1.9.3/lib/ocaml
/gnu/store/...-ocaml-findlib-1.9.3/lib/ocaml/site-lib
/gnu/store/...-coq-core-8.16.0/lib/ocaml
/gnu/store/...-coq-core-8.16.0/lib/ocaml/site-lib
/gnu/store/...-ocaml-elpi-1.16.7/lib/ocaml
/gnu/store/...-ocaml-elpi-1.16.7/lib/ocaml/site-lib
/gnu/store/...-coq-stdlib-8.16.0/lib/ocaml
/gnu/store/...-coq-stdlib-8.16.0/lib/ocaml/site-lib
/gnu/store/...-ocaml-zarith-1.12/lib/ocaml
/gnu/store/...-ocaml-zarith-1.12/lib/ocaml/site-lib
/gnu/store/...-ocaml-yojson-2.0.2/lib/ocaml
/gnu/store/...-ocaml-yojson-2.0.2/lib/ocaml/site-lib
/gnu/store/...-ocaml-biniou-1.2.2/lib/ocaml
/gnu/store/...-ocaml-biniou-1.2.2/lib/ocaml/site-lib
/gnu/store/...-ocaml-camlp-streams-5.0.1/lib/ocaml
/gnu/store/...-ocaml-camlp-streams-5.0.1/lib/ocaml/site-lib
/gnu/store/...-ocaml-atd-2.10.0/lib/ocaml
/gnu/store/...-ocaml-atd-2.10.0/lib/ocaml/site-lib
/gnu/store/...-ocaml-ppx-deriving-5.2.1/lib/ocaml
/gnu/store/...-ocaml-ppx-deriving-5.2.1/lib/ocaml/site-lib
/gnu/store/...-ocaml-re-1.10.4/lib/ocaml
/gnu/store/...-ocaml-re-1.10.4/lib/ocaml/site-lib
/gnu/store/...-ocaml-menhir-20220210/lib/ocaml
/gnu/store/...-ocaml-menhir-20220210/lib/ocaml/site-lib
/gnu/store/...-ocaml-ppxlib-0.25.0/lib/ocaml
/gnu/store/...-ocaml-ppxlib-0.25.0/lib/ocaml/site-lib
/gnu/store/...-ocaml-stdlib-shims-0.3.0/lib/ocaml
/gnu/store/...-ocaml-stdlib-shims-0.3.0/lib/ocaml/site-lib
/gnu/store/...-ocaml-seq-0.1/lib/ocaml
/gnu/store/...-ocaml-seq-0.1/lib/ocaml/site-lib
/gnu/store/...-ocaml-cmdliner-1.1.1/lib/ocaml
/gnu/store/...-ocaml-cmdliner-1.1.1/lib/ocaml/site-lib
/gnu/store/...-ocaml-odoc-2.2.0-alpha/lib/ocaml
/gnu/store/...-ocaml-odoc-2.2.0-alpha/lib/ocaml/site-lib
/gnu/store/...-ocaml-easy-format-1.3.4/lib/ocaml
/gnu/store/...-ocaml-easy-format-1.3.4/lib/ocaml/site-lib
/gnu/store/...-ocaml-result-1.5/lib/ocaml
/gnu/store/...-ocaml-result-1.5/lib/ocaml/site-lib
/gnu/store/...-ocaml-ppx-derivers-1.2.1/lib/ocaml
/gnu/store/...-ocaml-ppx-derivers-1.2.1/lib/ocaml/site-lib
/gnu/store/...-ocaml-sexplib0-0.15.1/lib/ocaml
/gnu/store/...-ocaml-sexplib0-0.15.1/lib/ocaml/site-lib
/gnu/store/...-ocaml-stdio-0.15.0/lib/ocaml
/gnu/store/...-ocaml-stdio-0.15.0/lib/ocaml/site-lib
/gnu/store/...-ocaml-migrate-parsetree-2.4.0/lib/ocaml
/gnu/store/...-ocaml-migrate-parsetree-2.4.0/lib/ocaml/site-lib
/gnu/store/...-ocaml-compiler-libs-0.12.4/lib/ocaml
/gnu/store/...-ocaml-compiler-libs-0.12.4/lib/ocaml/site-lib
/gnu/store/...-ocaml-base-0.15.0/lib/ocaml
/gnu/store/...-ocaml-base-0.15.0/lib/ocaml/site-lib
/gnu/store/...-ocamlbuild-0.14.2/lib/ocaml
/gnu/store/...-ocamlbuild-0.14.2/lib/ocaml/site-lib
/gnu/store/...-o-caml-findlib-1.9.3/lib/ocaml/site-lib

When using all the dependencies of coq-elpi, launching Proof General for Coq in Emacs, and inputting the following text,

From elpi Require Import elpi.

Findlib throws the same error.

It's true that coq-elpi.elpi does not exist, however that file seems to never be installed by the Makefile in coq-elpi. Digging into the installation dir of coq-elpi, it seems that coq-elpi.elpi has been replaced by coq-lib.elpi.

I'm using Coq 8.16, ocaml-elpi 1.16.7, and coq-elpi v1.16.0. I'm also running Guix 49e1a3a, but I'm not so sure the version of Guix is relevant.

Is there a way that I can tell hierarchy-builder that elpi should be imported from coq-lib.elpi? Ideally I'd want to do this in hierarchy-builder's Makefile, before building.

Let me know if you need any more info on this from me, or if I'm way off track :)

Thanks!

SnarkBoojum commented 1 year ago

Here you'll see what versions Debian and coq-platform use ; perhaps that will guide you: Coq platform vs Debian ; perhaps that will help?

gares commented 1 year ago

coq-elpi.elpi is a name defined in coq-elpi/META, wherever it is installed. The makefile installs it.

chipsf commented 1 year ago

It looks like it's simpler than I thought. After "installing" coq-elpi, ocamlfind can't find it. The problem seems to be more related to how Guix is building the package. I'll close the issue for now.

chipsf commented 1 year ago

In other words, META isn't getting installed, so that's a Guix problem. Thanks for your help!