Karl Palmskog (Feb 03 2022 at 16:17): 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]
example failing build: https://github.com/coq-community/hydra-battles/runs/5052931877?check_suite_focus=true
Gaëtan Gilbert (Feb 03 2022 at 16:17):findlib merge today
Karl Palmskog (Feb 03 2022 at 16:18):ah OK, that will indeed make things fail until the next coq.dev refresh...
Pierre-Marie Pédrot (Feb 03 2022 at 16:18):expect a few turbulences, the fallout hasn't completely dried off
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: Apr 19 2024 at 18:01 UTC