--release for pure Coq code affects flags and triggers rebuild

[Blaisorblade]

Expected Behavior

Since Coq code cannot be optimized, passing --release should not trigger a rebuild of .v files.

Actual Behavior

-w -native-compiler-disabled -native-compiler ondemand is passed for normal builds but not --release builds, triggering a rebuild.

Reproduction

• PR with a reproducing test:

1. dune build --cache=disabled --display=verbose theories/lang/prelude/notations.vo &> build-normal
2. dune build --cache=disabled --display=verbose theories/lang/prelude/notations.vo -p coq-cpp2v &> build-release
3. confirm that the options are different (which will trigger a rebuild); I've observed the actual rebuild with cache enabled

The code was a version of https://github.com/bedrocksystems/cpp2v but I can minimize.

Specifications

• Version of dune (output of dune --version): 2.8.5
• Version of ocaml (output of ocamlc --version): 4.07.1
• Operating system (distribution and version): MacOS 10.15

Additional information

• Link to gist with verbose output (run dune with the --verbose flag):
  https://gist.github.com/Blaisorblade/ef78b996624c42702d13886101342b41

[ejgallego]

Thanks, this is indeed a bug, and fortunately quite easy to solve I think if you look at coq_rules

[Blaisorblade]

Ah, I should have mentioned my dune-project has

(lang dune 2.7)
(using coq 0.2)

Bumping to 2.8 and 0.3 works around the problem, which is consistent with the code I see.

It seems the bug is in this code, which for 0.2 should use Legacy instead of VoOnly in non-release mode (is_dev):

let select_native_mode ~sctx ~(buildable : Buildable.t) =
  let profile = (SC.context sctx).profile in
  if Profile.is_dev profile then
    Coq_mode.VoOnly
  else
    snd buildable.mode

(but I wouldn't immediately know how to get to the config, so don't wait for me for a fix).

EDIT: so this might come from #4224.

[ejgallego]

Yup, thanks a lot for the analysis, it is correct.

[Blaisorblade]

From my latest testing this is not a problem today, even if I'm not sure when this was fixed.

[ejgallego]

It was fixed on some flags rework, I think when I fixed the (env (coq ...)) bug. Thanks for checking it is fixed!

By the way, I'd be nice to have a test suite entry for this.