Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

regression: coq-serapi.8.13.0+0.13.1 #7748

Closed
emillon opened this issue May 17, 2023 · 4 comments
Closed

regression: coq-serapi.8.13.0+0.13.1 #7748

emillon opened this issue May 17, 2023 · 4 comments
Assignees
Milestone

Comments

@emillon
Copy link
Collaborator

emillon commented May 17, 2023

Hi,
coq-serapi.8.13.0+0.13.1 does not build with dune.3.8.0~alpha3, but it does with dune.3.7.1.
See this build:

#=== ERROR while compiling coq-serapi.8.13.0+0.13.1 ===========================#
# context              2.2.0~alpha~dev | linux/x86_64 | ocaml-base-compiler.4.14.1 | file:///home/opam/opam-repository
# path                 ~/.opam/4.14/.opam-switch/build/coq-serapi.8.13.0+0.13.1
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-serapi -j 255
# exit-code            1
# env-file             ~/.opam/log/coq-serapi-7-872efe.env
# output-file          ~/.opam/log/coq-serapi-7-872efe.out
### output ###
# Error: exception Dune_rules__coq_config.Vars.E(_)
# Raised at Dune_rules__coq_config.Vars.fail in file
#   "src/dune_rules/coq/coq_config.ml", line 35, characters 21-49
# Called from Dune_rules__coq_config.Vars.get_path in file
#   "src/dune_rules/coq/coq_config.ml" (inlined), line 44, characters 23-32
# Called from Dune_rules__coq_config.make_res in file
#   "src/dune_rules/coq/coq_config.ml", line 186, characters 25-56
# Called from Fiber__core.O.(>>|).(fun) in file "otherlibs/fiber/src/core.ml",
#   line 250, characters 36-41
# Called from Fiber__scheduler.exec in file "otherlibs/fiber/src/scheduler.ml",
#   line 73, characters 8-11
# -> required by ("<unnamed>", ())
# -> required by ("<unnamed>", ())
# -> required by ("<unnamed>", ())
# -> required by ("Super_context.all", ())
# -> required by ("toplevel", ())
# 
# I must not crash.  Uncertainty is the mind-killer. Exceptions are the
# little-death that brings total obliteration.  I will fully express my cases. 
# Execution will pass over me and through me.  And when it has gone past, I
# will unwind the stack along its path.  Where the cases are handled there will
# be nothing.  Only I will remain.

Looks like this exception is never caught, in particular.

@emillon emillon added the bug label May 17, 2023
@emillon emillon added this to the 3.8.0 milestone May 17, 2023
@Alizter Alizter self-assigned this May 17, 2023
@emillon
Copy link
Collaborator Author

emillon commented May 17, 2023

I bisected that to 98de950 (#7047) as well.

@Alizter
Copy link
Collaborator

Alizter commented May 17, 2023

This is likely due to requesting a config option that doesn't exist in 8.13.

@ejgallego
Copy link
Collaborator

Mmm, I was under the impression we should never query coqc for OCaml projects, how is this happening?

@emillon
Copy link
Collaborator Author

emillon commented May 23, 2023

main now builds correctly

@emillon emillon closed this as completed May 23, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

4 participants