[Coq] Dune crashes on version 3.8

[LasseBlaauwbroek]

Reproduction

1. Make sure you are on Dune 3.8.
2. git clone git@github.com:coq-tactician/coq-tactician.git
3. opam install . --deps-only
4. dune build

Crashes with:

Error: exception Dune_rules__coq_config.Vars.E(_)
Raised at file "src/dune_rules/coq/coq_config.ml", line 37, characters 21-49
Called from file "src/dune_rules/coq/coq_config.ml", line 194, characters
  10-53
Called from file "otherlibs/fiber/src/core.ml", line 250, characters 36-41
Called from file "otherlibs/fiber/src/scheduler.ml", line 73, characters 8-11
-> required by ("<unnamed>", ())
-> required by ("<unnamed>", ())
-> required by ("<unnamed>", ())
-> required by ("<unnamed>", ())
-> required by ("gen-rules", In_build_dir "default/tests")
-> required by ("load-dir", In_build_dir "default/tests")
-> required by ("<unnamed>", ())
-> required by
   ("build-alias", { dir = In_build_dir "default"; name = "default" })
-> required by ("top-level", ())

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.

CC @ejgallego @Alizter

Specifications

• Version of dune (output of dune --version): 3.8.0
• Version of ocaml (output of ocamlc --version): 4.09.1
• Operating system (distribution and version): Arch linux

[Alizter]

Do you only have coq-core installed by chance? This should go away if you install the stdlib. The issue is that coqc --config fails without the stdlib.

[LasseBlaauwbroek]

No. This is running on coq 8.11.

[Alizter]

@LasseBlaauwbroek OK in that case this is new, will have a look ASAP.

[Alizter]

OK so the issue is that Dune is looking for COQ_NATIVE_COMPILER_DEFAULT however this is only available since 8.13. I'm not exactly sure how it should be treated when it isn't present, so I will assume "no" for the time being.

[LasseBlaauwbroek]

Thanks. Since 3.8.0 is already released, can we add a conflicts clause for Coq < 8.13 to the package?

[Alizter]

Sure that will be up to @emillon to do. I will definitely fix this for a 3.8.1 point release however.

[Alizter]

I've submitted #7847. If you could opam pin that PR branch and test it that would be appreciated. It worked (didn't crash) for me locally.

[emillon]

Thanks. Since 3.8.0 is already released, can we add a conflicts clause for Coq < 8.13 to the package?

coq 8.13.0 builds fine with dune 3.8.0, so it looks like it's a more precise combination that should be rejected.

Agree to cut a point release with a fix.

[emillon]

coq 8.13.0 builds fine with dune 3.8.0, so it looks like it's a more precise combination that should be rejected.

To clarify: if the coq package as built with 3.8.0 is useless, it can conflict, but it seems like we're restricting valid combinations.

[LasseBlaauwbroek]

• I think the problem is only for Coq 8.12 and below.
• Even for Coq 8.12, it is probably indeed still possible to build Coq itself with Dune 3.8.0. But it is impossible to build any packages that depend on Coq.

if the coq package as built with 3.8.0 is useless, it can conflict, but it seems like we're restricting valid combinations.

I guess we are indeed restricting valid combinations. But is this really a big problem? Dune 3.7 can still be used for all current packages, and Dune 3.8.1 will presumably be released soon. It would be inconvenient to have a Dune version in the Opam manager that crashes on a bunch of packages.

The only other solution is to manually mark all current and future packages that depend on Coq <= 8.12 to be conflicting with Dune 3.8.0... Not something I'd like to be in charge of.

[emillon]

I guess it's up to the coq and opam maintainers. You can open a PR to ocaml/opam-repository to add the conflicts clause.

[erikmd]

I guess we are indeed restricting valid combinations

At first sight, I don't think so. I mean, all Coq versions upto 8.12.x certainly will trigger the crash regarding COQ_NATIVE_COMPILER_DEFAULT.

So I vote +1 for adding a conflicts: [ "coq" {< "8.13"} ] clause in dune.3.8.0

[ejgallego]

Indeed the conflict sounds reasonable. As we approach (lang coq 1.0) it could be worth to add Coq 8.11 to Dune's CI.

[Alizter]

I was imagining setting up a custom workflow for older coq versions that can be manually triggered. That would help us with a lot of these issues stemming from the coq world.

[ejgallego]

Actually if we do cache the Coq installl that should not be too heavy IMVHO as a regular job.

[ejgallego]

I was imagining setting up a custom workflow for older coq versions that can be manually triggered. That would help us with a lot of these issues stemming from the coq world.

I think we also need to be very mindful and define (maybe we write it down in the DuneCoq paper) our methodology for ensuring compatibility with older Coq versions. Testing is very important but also we need to be very defensive when interacting with the Coq API.

[LasseBlaauwbroek]

See ocaml/opam-repository#23882