Stream: MetaCoq

Topic: error from opam


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Yannick Forster (Jan 09 2021 at 17:32):

Mh, that's looks good to me. What's the output of which sed and which gsed?

view this post on Zulip Jonathan Leivent (Jan 09 2021 at 17:35):

$ which sed
/usr/bin/sed

gsed is not installed

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Théo Winterhalter (Jan 09 2021 at 18:38):

Ah right what's your ocaml version?

view this post on Zulip 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.)

view this post on Zulip Jonathan Leivent (Jan 09 2021 at 18:40):

$ ocaml --version
The OCaml toplevel, version 4.10.0

view this post on Zulip Li-yao (Jan 09 2021 at 18:47):

Can you share the build output? Opam cut out the interesting part.

view this post on Zulip Jonathan Leivent (Jan 09 2021 at 18:49):

output file attached coq-metacoq-template-23548-0325cb.out

view this post on Zulip 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

view this post on Zulip Yannick Forster (Jan 09 2021 at 18:49):

We fix this manually using patch

view this post on Zulip Yannick Forster (Jan 09 2021 at 18:49):

Ahh

view this post on Zulip Yannick Forster (Jan 09 2021 at 18:50):

What about which patch?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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: Aug 11 2022 at 02:03 UTC