Stream: Hydras & Co. universe

Topic: CI failure on goedel

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

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

view this post on Zulip 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 ==================================#
  # context              2.1.3 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.13.1+options | 08:00
  # path                 ~/.opam/4.13.1+flambda/.opam-switch/build/
  # 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/
  # CAMLOPT -c  src/
  # File "src/", 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

view this post on Zulip Karl Palmskog (Feb 26 2023 at 09:54):

I think this is the same problem I addressed in this commit

Last updated: May 18 2024 at 10:02 UTC