Jonathan Leivent (Jan 09 2021 at 17:07): Jonathan Leivent (Jan 09 2021 at 17:07):I'm trying to install metacoq from opam on Debian 10.7, and am getting:
# Error: The implementation gen-src/cRelationClasses.ml
# [...]
# val eq_equivalence : ('a1, __) coq_Equivalence
# File "gen-src/cRelationClasses.mli", line 107, characters 0-46:
# Expected declaration
# File "gen-src/cRelationClasses.ml", line 204, characters 4-18:
# Actual declaration
# make[3]: *** [Makefile.plugin:664: gen-src/cRelationClasses.cmx]
Error 2 # make[2]: *** [Makefile.plugin:339: all] Error 2
I have nothing pinned in opam, hence all versions are set to whatever metacoq is requesting.
Yannick Forster (Jan 09 2021 at 17:27):Hi again :) opam tells you which version it tries to install. Can you give us the printout of versions opam computed for all packages?
Jonathan Leivent (Jan 09 2021 at 17:30):The following actions will be performed:
∗ install coq-metacoq-template 1.0~beta1+8.12 [required by coq-metacoq]
∗ install coq-metacoq-checker 1.0~beta1+8.12 [required by coq-metacoq]
∗ install coq-metacoq-translations 1.0~beta1+8.12 [required by coq-metacoq]
∗ install coq-metacoq-pcuic 1.0~beta1+8.12 [required by coq-metacoq]
∗ install coq-metacoq-safechecker 1.0~beta1+8.12 [required by coq-metacoq]
∗ install coq-metacoq-erasure 1.0~beta1+8.12 [required by coq-metacoq]
∗ install coq-metacoq 1.0~beta1+8.12
Mh, that's looks good to me. What's the output of which sed and which gsed?
Jonathan Leivent (Jan 09 2021 at 17:35):$ which sed
/usr/bin/sed
gsed is not installed
Théo Winterhalter (Jan 09 2021 at 18:34):Unless on macOS, I don't think you need gsed. The error message doesn't look like the usual gsed problem to me.
Did opam manage to install at least some of the packages or did it already fail on coq-metacoq-template?
Jonathan Leivent (Jan 09 2021 at 18:38):It failed on coq-metacoq-template. Do you want me to attach the full build output file? There are some warnings in it about Stlib.Pervasives, such as:
File "gen-src/binPos.ml", line 18, characters 17-32:
18 | let rec succ = Pervasives.succ
^^^^^^^^^^^^^^^
Alert deprecated: module Stdlib.Pervasives
Use Stdlib instead.
If you need to stay compatible with OCaml < 4.07, you can use the
stdlib-shims library: https://github.com/ocaml/stdlib-shims
Ah right what's your ocaml version?
Théo Winterhalter (Jan 09 2021 at 18:39):(I have no clue what the problem so I'm trying to get more information to compare.)
Jonathan Leivent (Jan 09 2021 at 18:40):$ ocaml --version
The OCaml toplevel, version 4.10.0
Can you share the build output? Opam cut out the interesting part.
Jonathan Leivent (Jan 09 2021 at 18:49):output file attached coq-metacoq-template-23548-0325cb.out
Yannick Forster (Jan 09 2021 at 18:49):The error is on the line of extracted code where Coq extraction has a bug and creates a non-Typable OCaml file
Yannick Forster (Jan 09 2021 at 18:49):We fix this manually using patch
Yannick Forster (Jan 09 2021 at 18:49):Ahh
Yannick Forster (Jan 09 2021 at 18:50):What about which patch?
Yannick Forster (Jan 09 2021 at 18:51):This error occurred under windows because there the automatic patch failed, and the wrong extracted code was compiled. That's why my first idea was that it's this problem again, just in Debían-clothes
Jonathan Leivent (Jan 09 2021 at 19:18):Ohhh... patch... OK - that might be it. I have patch wrapped by a custom firejail profile, as I don't expect it to be used non-interactively. Let me try temporarily unwrapping it, and re-installing metacoq.
Jonathan Leivent (Jan 09 2021 at 19:33):It is building past that point now. Just a suggestion: perhaps the usage of patch should check to see if it has an error and stop the build there?
Jonathan Leivent (Jan 09 2021 at 20:02):The install completed! Thanks!
IMHO, patch is generally not a good tool to use non-interactively (such as in installs), as its heuristics will occasionally silently make mistakes, some of which won't get caught later.
Yannick Forster (Jan 09 2021 at 20:17):Both are probably a good idea. We also currently don't mention anywhere that patch is being used, which might already have helped you
Jonathan Leivent (Jan 09 2021 at 23:46):I'm now having trouble with the demo: I get this in ProofGeneral:
Sys_error("/home/jil/.opam/default/.opam-switch/sources/coq-metacoq-template.1.0~beta1+8.12/template-coq/build: No such file or directory")
Did I miss a step in the install?
Jonathan Leivent (Jan 10 2021 at 01:30):It must have been some left-over cruft from the install problems. After uninstalling, cleaning, and re-installing, all is well.
Abhishek Anand (Feb 16 2021 at 19:10):Ohhh... patch... OK - that might be it. I have patch wrapped by a custom firejail profile, as I don't expect it to be used non-interactively. Let me try temporarily unwrapping it, and re-installing metacoq.
I was also getting the same error. I did not even write any custom firejail profile (just using the defaults on the latest Manjaro). I don't get any error after unjailing patch (commenting it out in /usr/lib/firejail/firecfg.config and then doing sudo firecfg --clean; sudo firecfg )
Last updated: Jun 01 2023 at 12:01 UTC