[coq] Composition with (boot) theories is not working in Dune 3.8

[ejgallego]

Steps to reproduce:

$ git clone https://github.com/coq/coq.git
$ cd coq && cp theories/dune.disabled theories/dune
$ dune build @default

result is that -boot flag is missing from the first coqdep call:

File "theories/dune", line 2, characters 0-588:
 2 | (coq.theory
 3 |  (name Coq)
 4 |  (package coq-stdlib)
....
28 | 
29 |    coq-core.plugins.ssreflect
30 |    coq-core.plugins.derive))
cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used.

This can only be tested up to (lang coq 0.6), as newer lang versions are blocked #7908

[ejgallego]

Will have a look into this next.

[Alizter]

I had a look. Our boot flags seem to be messed up. Before we had:

dune/src/dune_rules/coq/coq_rules.ml

Lines 75 to 82 in e2b2d6a

	match t with
	(* Coq's stdlib is installed globally *)
	| `No_boot -> Command.Args.empty
	(* Coq's stdlib is in scope of the composed build *)
	| `Bootstrap _ -> A "-boot"
	(* We are compiling the prelude itself
	[should be replaced with (per_file ...) flags] *)
	| `Bootstrap_prelude -> As [ "-boot"; "-noinit" ]

Now we have:

dune/src/dune_rules/coq/coq_rules.ml

Lines 135 to 142 in 23617a8

	let boot_flags ~coq_lang_version t : _ Command.Args.t =
	let boot_flag = if coq_lang_version >= (0, 8) then [ "-boot" ] else [] in
	match t with
	(* We are compiling the prelude itself
	[should be replaced with (per_file ...) flags] *)
	| `Bootstrap_prelude -> As ("-noinit" :: boot_flag)
	(* No special case *)
	| `No_boot | `Bootstrap _ -> As boot_flag

which seems wrong.

[ejgallego]

Well spotted! I think this got messed up when we backtracked on some cleanup that always put -boot unconditionally, but we decided against it as to better preserve the < 0.8 behavior (no boot flag)

So your patch should solve this problem.