[coq] Fix computation of profile flags. (ocaml#4749)

* Add test case for coq + env

Signed-off-by: Rudi Grinberg <[email protected]>

* [coq] Fix computation of profile flags.

This is very subtle and I am not sure I do understand all the
subtleties here, but moving the expansion to the inheritance function
seems like the right thing to do.

Added almost exhaustive test cases.

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

Co-authored-by: Rudi Grinberg <[email protected]>

CHANGES.md

@@ -27,6 +27,9 @@ unreleased - 2.9 branch
 
 - Handle renaming of `coq.kernel` library to `coq-core.kernel` in Coq 8.14 (#4713, @proux01)
 
+- Fix issue where Dune would ignore `(env ... (coq (flags ...)))`
+  declarations appearing in `dune` files (#4749, fixes #4566, @ejgallego @rgrinberg)
+
 2.8.5 (28/03/2021)
 ------------------
 

src/dune_rules/coq_rules.ml

@@ -119,7 +119,7 @@ module Context = struct
     ; scope : Scope.t
     ; boot_type : Bootstrap.t
     ; build_dir : Path.Build.t
-    ; profile_flags : Ordered_set_lang.Unexpanded.t
+    ; profile_flags : string list Action_builder.t
     ; mode : Coq_mode.t
     ; native_includes : Path.Set.t Or_exn.t
     ; native_theory_includes : Path.Build.Set.t Or_exn.t
@@ -129,13 +129,8 @@ module Context = struct
     let dir = Path.build (snd t.coqc) in
     Command.run ~dir ?stdout_to (fst t.coqc) args
 
-  let standard_coq_flags = Build.return [ "-q" ]
-
   let coq_flags t =
-    let standard = standard_coq_flags in
-    let standard =
-      Expander.expand_and_eval_set t.expander t.profile_flags ~standard
-    in
+    let standard = t.profile_flags in
     Expander.expand_and_eval_set t.expander t.buildable.flags ~standard
 
   let theories_flags =

src/dune_rules/env_node.ml

@@ -10,7 +10,7 @@ module Odoc = struct
 end
 
 module Coq = struct
-  type t = Ordered_set_lang.Unexpanded.t
+  type t = string list
 end
 
 type t =
@@ -23,7 +23,7 @@ type t =
   ; inline_tests : Dune_env.Stanza.Inline_tests.t Memo.Lazy.t
   ; menhir_flags : string list Build.t Memo.Lazy.t
   ; odoc : Odoc.t Memo.Lazy.t
-  ; coq : Coq.t Memo.Lazy.t
+  ; coq : Coq.t Action_builder.t Memo.Lazy.t
   ; format_config : Format_config.t Memo.Lazy.t
   }
 
@@ -144,7 +144,14 @@ let make ~dir ~inherit_from ~scope ~config_stanza ~profile ~expander
     inherited ~field:odoc ~root (fun { warnings } ->
         { warnings = Option.value config.odoc.warnings ~default:warnings })
   in
-  let coq = inherited ~field:coq ~root:config.coq (fun x -> x) in
+  let default_coq_flags = Action_builder.return [ "-q" ] in
+  let coq : Coq.t Action_builder.t Memo.Lazy.t =
+    inherited ~field:coq ~root:default_coq_flags (fun flags ->
+        let+ expander = Memo.Lazy.force expander in
+        let expander = Expander.set_dir expander ~dir in
+        let standard = flags in
+        Expander.expand_and_eval_set expander config.coq ~standard)
+  in
   let format_config =
     inherited_if_absent ~field:format_config ~root:config.format_config
       (function

src/dune_rules/env_node.mli

@@ -12,7 +12,7 @@ module Odoc : sig
 end
 
 module Coq : sig
-  type t = Ordered_set_lang.Unexpanded.t
+  type t = string list
 end
 
 type t
@@ -46,7 +46,7 @@ val bin_artifacts : t -> Artifacts.Bin.t
 
 val odoc : t -> Odoc.t
 
-val coq : t -> Coq.t
+val coq : t -> Coq.t Build.t
 
 val menhir_flags : t -> string list Build.t
 

src/dune_rules/super_context.mli

@@ -85,7 +85,7 @@ val local_binaries : t -> dir:Path.Build.t -> File_binding.Expanded.t list
 val odoc : t -> dir:Path.Build.t -> Env_node.Odoc.t
 
 (** coq config in the corresponding [(env)] stanza. *)
-val coq : t -> dir:Path.Build.t -> Env_node.Coq.t
+val coq : t -> dir:Path.Build.t -> Env_node.Coq.t Build.t
 
 (** Formatting settings in the corresponding [(env)] stanza. *)
 val format_config : t -> dir:Path.Build.t -> Format_config.t