coqc: ondemand: no such file or directory

[Armael]

With Coq 8.9.1, after upgrading to dune 2.8.1, compiling coq files does not seem to work anymore (due to unsupported command-line arguments it seems).

Expected Behavior

It works.

Actual Behavior

It does not work.

       coqc .t.aux,t.{glob,vo} (exit 1)
(cd _build/default && /home/armael/.opam/latest/bin/coqc -q -w -native-compiler-disabled -native-compiler ondemand -R . foo t.v)
coqc: ondemand: no such file or directory

Reproduction

dune file:

(coq.theory (name foo))

with an empty file t.v on the side.

Specifications

• Version of dune: 2.8.1
• Version of ocaml (output of ocamlc --version): 4.08.1
• Version of coq: 8.9.1

[LasseBlaauwbroek]

This issue is also happening in Coq bench. For example, see here: https://coq-bench.github.io/clean/Linux-x86_64-4.07.1-2.0.6/released/8.9.1/tactician-dummy/1.0~beta1.html. It appears that this bug was introduced in #3210, in particular here:

dune/src/dune_rules/coq_rules.ml

Line 162 in 0453da3

[ "-w"; "-native-compiler-disabled"; "-native-compiler"; "ondemand" ]

Presumably, some kind of special case for older versions of Coq needs to be introduced?

[gares]

It seems this commit broke old versions of Coq: 0337d3e

[rgrinberg]

I assume this was intentional and @ejgallego does not intend to support old versions of coq.

[Armael]

Well I mean, both the retro-compatibility and the user experience are a bit terrible. I just upgraded dune and my stuff stopped compiling. Note that even using a dune-project that specifies an older version of dune/the coq support doesn't help, the error is still there.

[ejgallego]

I didn't do this on purpose, I only test in fact with 8.10 , and didn't recall this option was introduced so recently. So this is a bug.

Determining the version of Coq is unfortunately quite tricky, but if someone manages to write something that would work on the composed build I'd be happy to add it. For now I think indeed the best choice is document that coq-lang >= 0.3 is not compatible with Coq < 8.10 , document it, and actually don't add this flag unless the coq version is bumped.

WDYT @Armael ? Is dropping support for Coq < 8.10 in coq-lang >= 0.3 a huge problem? Note that we may be able to have to improve on this for example in Coq 8.14 if Coq moves to the split compilation scheme [which would mean that coq-lang >= 0.4 would support back Coq 8.9]

[Armael]

Having things work again with coq-lang < 0.3 definitely sounds like an improvement; I'm ok with coq-lang 0.3 requiring a more recent version of Coq if that's documented.

I was initially wondering if that could be a problem in a fresh setup (where dune automatically generates a dune-project with the most recent dune version), but since the coq-lang directive has to be inserted manually then there should be no problem.

[ejgallego]

Coq lang is actually automatically inserted by dune-project auto-generation [if dune sees some coq.theory around] , however that feature is deprecated [due to it being too surprising] so as long as it is properly documented IMHO not a big deal.

Will prepare a fix ASAP, pity 2.8.2 just got released so this will have to wait until 2.8.3 :/

[ejgallego]

The best would be of course to be able to expose to dune the proper Coq version, otherwise the workaround is still not very usable as if you use (coq 0.3) and Coq 8.9 you will get a weird error. But I'm afraid the whole native stuff is quite experimental :S

Dropping the explicit option is pretty inconvenient but could be another possibility, tho it would incur in a large cost for nothing when people set Coq to produce native objects by default [which is a large mistake by itself]

[ejgallego]

Fix incoming, sorry I missed Dune 2.8.2 , I'm unsure if there will be a 2.8.3 :S

[ghost]

If the bugfix is important for users, we should release a 2.8.3.

[ejgallego]

If the bugfix is important for users, we should release a 2.8.3.

The set of users is quite small [I thought it was empty] , so not entirely sure about doing the 2.8.3 effort if that's the only fix we'd add there, as opposed to a 2.9.0 later on.