Stream: Coq devs & plugin devs

Topic: coq_makefile failure for extra-dev


view this post on Zulip Karl Palmskog (Feb 03 2022 at 16:17):

Was there some big coq_makefile change in the last few days? Looks like both coq-paramcoq.dev and coq-equations.dev extra-dev opam packages are now failing with the following error messages:

#=== ERROR while compiling coq-equations.dev ==================================#
  # context              2.0.9 | linux/x86_64 | ocaml-variants.4.07.1+flambda | https://coq.inria.fr/opam/extra-dev#2022-02-01 16:40
  # path                 ~/.opam/4.07.1+flambda/.opam-switch/build/coq-equations.dev
  # command              ~/.opam/4.07.1+flambda/.opam-switch/build/coq-equations.dev/./configure.sh
  # exit-code            1
  # env-file             ~/.opam/log/coq-equations-175-6aa130.env
  # output-file          ~/.opam/log/coq-equations-175-6aa130.out
  ### output ###
  # [...]
  # [-Q physicalpath logicalpath]: look for Coq dependencies starting from
  #   "physicalpath". The logical path associated to the physical path
  #   is "logicalpath".
  # [VARIABLE = value]: Add the variable definition "VARIABLE=value"
  # [-arg opt]: send option "opt" to coqc
  # [-docroot path]: Install the documentation in this folder, relative to
  #   "user-contrib".
  # [-f file]: take the contents of file as arguments
  # [-o file]: output should go in file file (recommended)
  #     Output file outside the current directory is forbidden.
  # [-h]: print this usage summary
  # [--help]: equivalent to [-h]

view this post on Zulip Karl Palmskog (Feb 03 2022 at 16:17):

example failing build: https://github.com/coq-community/hydra-battles/runs/5052931877?check_suite_focus=true

view this post on Zulip Gaëtan Gilbert (Feb 03 2022 at 16:17):

findlib merge today

view this post on Zulip Karl Palmskog (Feb 03 2022 at 16:18):

ah OK, that will indeed make things fail until the next coq.dev refresh...

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 16:18):

expect a few turbulences, the fallout hasn't completely dried off

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 16:30):

Things should be much better once we merge the coq_dune PR, now that the findlib patch is in, I can finish it


Last updated: Feb 01 2023 at 16:03 UTC