Pierre Castéran (Feb 13 2023 at 17:37): Pierre Castéran (Feb 13 2023 at 17:37):@Karl Palmskog @Théo Zimmermann The CI compilation of goedel (on branch Experimental) failed on all Coq versions.
Could it be because goedel now imports a module theories/ordinals/Prelude/MoreLibHyps, which depends on LibHyps?
On my local machine, the compilation (by makeis OK).
I used LibHyps in order to lower the amount of automatically named intros patterns in many destructor decomposetactics.
Karl Palmskog (Feb 13 2023 at 17:39):something may have changed in some .dev package to cause this, for example libhyps. But I'd need to look at CI logs carefully, which I might be able to do tomorrow night.
Pierre Castéran (Feb 16 2023 at 07:36):@Karl Palmskog Indeed, looks to work now (except on dev, but I think the issue comes from Equations)
#=== ERROR while compiling coq-equations.dev ==================================#
# context 2.1.3 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.13.1+options | https://coq.inria.fr/opam/extra-dev#2023-02-16 08:00
# path ~/.opam/4.13.1+flambda/.opam-switch/build/coq-equations.dev
# command /usr/bin/make -j2
# exit-code 2
# env-file ~/.opam/log/coq-equations-540-5a2abb.env
# output-file ~/.opam/log/coq-equations-540-5a2abb.out
### output ###
# [...]
# CAMLOPT -c src/syntax.ml
# CAMLOPT -c src/eqdec.ml
# File "src/syntax.ml", line 343, characters 2-94:
# 343 | (CHole (Some (ImplicitArg (GlobRef.ConstRef cst, (0,None), false)), Namegen.IntroAnonymous)), None
# ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
# Error: The constructor CHole expects 3 argument(s),
# but is applied here to 2 argument(s)
# make[2]: *** [Makefile.coq:743: src/syntax.cmx] Error 2
```
I think this is the same problem I addressed in this commit
Last updated: Apr 20 2024 at 10:02 UTC