regression on missing Coq #9818
Description
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)