regression on missing Coq

[vzaliva]

Expected Behavior

Consider the following toy demo repository:

https://github.com/vzaliva/coq-dune-examlpe

In an opam switch without Coq installed, with dune 3.12.2 it builds without errors using following command:

dune build -p example-ocaml

(this is expected)

Actual Behavior

However, with dune 3.13.0 it gives build error:

$ dune build -p example-ocaml
Error: Couldn't find Coq standard library, and theory is not using (stdlib
no)

(this is a regression)

It is related to the following bug #8099
See the discussion there.

Specifications

$ dune --version
3.13.0
$ ocaml --version
The OCaml toplevel, version 4.13.1
$ lsb_release -a
No LSB modules are available.
Distributor ID:	Ubuntu
Description:	Ubuntu 23.04
Release:	23.04
Codename:	lunar

Additional information

dune build -p example-ocaml --verbose
Shared cache: disabled
Shared cache location: /home/lord/.cache/dune/db
Workspace root: /home/lord/src/coq-dune-examlpe
Auto-detected concurrency: 12
Dune context:
 { name = "default"
 ; kind = "default"
 ; profile = Release
 ; merlin = true
 ; fdo_target_exe = None
 ; build_dir = In_build_dir "default"
 ; installed_env =
     map
       { "INSIDE_DUNE" : "/home/lord/src/coq-dune-examlpe/_build/default"
       ; "OCAML_COLOR" : "always"
       ; "OPAMCOLOR" : "always"
       }
 ; instrument_with = []
 }
Actual targets:
- recursive alias @install
Error: Couldn't find Coq standard library, and theory is not using (stdlib
no)

[ejgallego]

Thanks for the careful report @vzaliva , I think we should bisect to see what commit produces this error, but actually this may be an unintended result of a bug fix, that makes some important checks on rule creation.

We need to understand how the check is triggered, but in principle it should be possible and reasonably easy to make this check a bit more lazy so things work again.

[ejgallego]

Indeed, the error is trigged by Bootstrap.make. I'm am not sure how to make this check more lazy, as indeed it is needed to setup the Coq rules.

@rgrinberg , is it expected that the Coq rules are setup in this case?

[emillon]

b6cf48c is the first bad commit (#9347)

[ejgallego]

uld bisect to see what commit produces this error, but actually this may be an unintended result of a bug fix, that makes s

Thanks @emillon , this is indeed the bug fix I was talking about. Before the bugfix, we did setup the rules, but we didn't error in this wrong configuration.

I'm not sure how to delay this check. One option is to remove the check, but that would introduce another kind of problems due to actual invalid configurations.

[rgrinberg]

I was going to explain how to do avoid this issue in detail, but realized half way that prototype would be easier to understand. Basically, the issue is that doing User_error.raise or Resolve.Memo.read_memo are going to prevent rule loading for the entire directory. Depending on how fatal the error is, that's not what you want. The trick is to delay such errors until the rules are executed by plumbing them down to Action_builder.t using Resolve.Memo.t.

See #9845 for an example.

I'm not actually sure if it fixes the concrete error in this PR, but it should give you a sketch on how to go about this. Feel free to take over and adjust it to your tastes.