[coq] make expand "coq.version" and co not depend on coq-stdlib (#10631)

* [coq] fix `%{coq.version} expansion to work without coq-stdlib Signed-off-by: Enrico Tassi <Enrico.Tassi@Inria.fr>
ocaml · Jun 30, 2024 · 24dab51 · 24dab51
1 parent ab3b66c
commit 24dab51
Show file tree

Hide file tree

Showing 4 changed files with 92 additions and 93 deletions.
diff --git a/doc/changes/10631.md b/doc/changes/10631.md
@@ -0,0 +1,2 @@
+- Don't depend on coq-stdlib being installed when expanding variables
+  of the `coq.version` family (#10631, fixes #10629, @gares)
diff --git a/src/dune_rules/coq/coq_config.ml b/src/dune_rules/coq/coq_config.ml
@@ -154,7 +154,7 @@ module Version = struct
          Return
          bin
          (* we pass -boot since this means it will work with just coq-core *)
-         [ "--print-version"; "-boot" ]
+         [ "--print-version"; "-boot"; "-noinit" ]
   ;;
 
   let version_memo = Memo.create "coq-and-ocaml-version" ~input:(module Path) impl_version
@@ -183,24 +183,20 @@ module Version = struct
     { version_num; version_string; ocaml_version_string }
   ;;
 
-  let by_name t name =
-    match t with
-    | Error msg -> User_error.raise Pp.[ textf "Could not parse coqc version: "; msg ]
-    | Ok { version_num; version_string; ocaml_version_string } ->
-      (match name with
-       | "version.major" -> Num.by_name version_num "major"
-       | "version.minor" -> Num.by_name version_num "minor"
-       | "version.revision" -> Num.by_name version_num "revision"
-       | "version.suffix" -> Num.by_name version_num "suffix"
-       | "version" -> Some (Value.string version_string)
-       | "ocaml-version" -> Some (Value.string ocaml_version_string)
-       | _ -> None)
+  let by_name { version_num; version_string; ocaml_version_string } name =
+    match name with
+    | "version.major" -> Num.by_name version_num "major"
+    | "version.minor" -> Num.by_name version_num "minor"
+    | "version.revision" -> Num.by_name version_num "revision"
+    | "version.suffix" -> Num.by_name version_num "suffix"
+    | "version" -> Some (Value.string version_string)
+    | "ocaml-version" -> Some (Value.string ocaml_version_string)
+    | _ -> None
   ;;
 end
 
 type t =
-  { version_info : (Version.t, User_message.Style.t Pp.t) Result.t
-  ; coqlib : Path.t
+  { coqlib : Path.t
   ; coqcorelib : Path.t option (* this is not available in Coq < 8.14 *)
   ; coq_native_compiler_default : string option (* this is not available in Coq < 8.13 *)
   }
@@ -221,19 +217,11 @@ let impl_config bin =
 
 let config_memo = Memo.create "coq-config" ~input:(module Path) impl_config
 
-let version ~coqc =
-  let open Memo.O in
-  let+ t = Version.make ~coqc in
-  let open Result.O in
-  let+ t = t in
-  t.version_string
-;;
-
 let make ~(coqc : Action.Prog.t) =
   let open Memo.O in
   let+ config_output =
     get_output_from_config_or_version ~coqc ~what:"--config" config_memo
-  and+ version_info = Version.make ~coqc in
+  in
   let open Result.O in
   let* config_output = config_output in
   match Vars.of_lines config_output with
@@ -243,19 +231,13 @@ let make ~(coqc : Action.Prog.t) =
     let coqcorelib = Vars.get_path_opt vars "COQCORELIB" in
     (* this is not available in Coq < 8.13 *)
     let coq_native_compiler_default = Vars.get_opt vars "COQ_NATIVE_COMPILER_DEFAULT" in
-    Ok { version_info; coqlib; coqcorelib; coq_native_compiler_default }
+    Ok { coqlib; coqcorelib; coq_native_compiler_default }
   | Error msg ->
     User_error.raise Pp.[ textf "Cannot parse output of coqc --config:"; msg ]
 ;;
 
-let by_name { version_info; coqlib; coqcorelib; coq_native_compiler_default } name =
+let by_name { coqlib; coqcorelib; coq_native_compiler_default } name =
   match name with
-  | "version.major"
-  | "version.minor"
-  | "version.revision"
-  | "version.suffix"
-  | "version"
-  | "ocaml-version" -> Version.by_name version_info name
   | "coqlib" -> Some (Value.path coqlib)
   | "coqcorelib" -> Option.map ~f:Value.path coqcorelib
   | "coq_native_compiler_default" ->
@@ -270,25 +252,34 @@ let expand source macro artifacts_host =
   let s = Pform.Macro_invocation.Args.whole macro in
   let open Memo.O in
   let* coqc = Artifacts.binary artifacts_host ~where:Original_path ~loc:None "coqc" in
-  let+ t = make ~coqc in
-  match t with
-  | Error msg ->
-    User_error.raise
-      ~loc:(Dune_lang.Template.Pform.loc source)
-      [ Pp.textf "Could not expand %%{coq:%s} as running coqc --config failed." s; msg ]
-      ~hints:
-        [ Pp.textf
-            "coqc --config requires the coq-stdlib package in order to function properly."
-        ]
-  | Ok t ->
-    (match by_name t s with
-     | None ->
-       User_error.raise
-         ~loc:(Dune_lang.Template.Pform.loc source)
-         [ Pp.textf "Unknown Coq configuration variable %S" s ]
-     | Some v ->
-       (match v with
-        | Int x -> [ Dune_lang.Value.String (string_of_int x) ]
-        | String x -> [ String x ]
-        | Path x -> Dune_lang.Value.L.paths [ x ]))
+  let expand m k s =
+    let+ t = m ~coqc in
+    match t with
+    | Error msg ->
+      User_error.raise
+        ~loc:(Dune_lang.Template.Pform.loc source)
+        [ Pp.textf "Could not expand %%{coq:%s} as running coqc failed." s; msg ]
+    | Ok t ->
+      (match k t s with
+       | None ->
+         User_error.raise
+           ~loc:(Dune_lang.Template.Pform.loc source)
+           [ Pp.textf "Unknown Coq configuration variable %S" s ]
+       | Some v ->
+         let open Value in
+         (match v with
+          | Int x -> [ Dune_lang.Value.String (string_of_int x) ]
+          | String x -> [ Dune_lang.Value.String x ]
+          | Path x -> Dune_lang.Value.L.paths [ x ]))
+  in
+  match s with
+  | "version.major"
+  | "version.minor"
+  | "version.revision"
+  | "version.suffix"
+  | "version"
+  | "ocaml-version" -> expand Version.make Version.by_name s
+  | "coqlib" | "coqcorelib" | "coq_native_compiler_default" -> expand make by_name s
+  | _ ->
+    Code_error.raise "Unknown name was requested from coq_config" [ "name", Dyn.string s ]
 ;;
diff --git a/src/dune_rules/coq/coq_config.mli b/src/dune_rules/coq/coq_config.mli
@@ -1,24 +1,5 @@
 open Import
 
-(** Data of a Coq configuration. *)
-type t
-
-(** [version ~coqc] runs coqc --print-version and returns the version of Coq as a string
-    without having to run coqc --config. Exceptionally, one of the following will happen:
-
-    - Return [Error message] if coqc --print-version exits with a non-zero code.
-    - Throw a user error if coqc --print-version is not parsable.
-    - Throw an [Action.Prog.Not_found] exception if the coqc binary is not found. *)
-val version : coqc:Action.Prog.t -> (string, User_message.Style.t Pp.t) result Memo.t
-
-(** [make ~coqc] runs coqc --config and returns the configuration data. Exceptionally, one
-    of the following will happen:
-
-    - Return [Error message] if coqc --config exits with a non-zero code.
-    - Throw a user error if coqc --config is not parsable.
-    - Throw an [Action.Prog.Not_found] exception if the coqc binary is not found. *)
-val make : coqc:Action.Prog.t -> (t, User_message.Style.t Pp.t) result Memo.t
-
 module Value : sig
   type t = private
     | Int of int
@@ -31,18 +12,51 @@ module Value : sig
   val to_dyn : t -> Dyn.t
 end
 
+module Version : sig
+  (** Data of a Coq version. *)
+  type t
+
+  (** [make ~coqc] runs coqc --print-version and returns the version of Coq
+      and the version of OCaml used to build Coq.
+      Exceptionally, one of the following will happen:
+
+      - Return [Error message] if coqc --print-version exits with a non-zero code.
+      - Throw a user error if coqc --print-version is not parsable.
+      - Throw an [Action.Prog.Not_found] exception if the coqc binary is not found. *)
+  val make : coqc:Action.Prog.t -> (t, User_message.Style.t Pp.t) result Memo.t
+
+  (** [by_name t name] returns the value of the field [name] in the Coq
+      version [t]. If the value is not available then [None] is returned.
+      Throws a code error if an invalid [name] is requested.
+
+      Currently supported names are:
+
+      - version.major
+      - version.minor
+      - version.revision
+      - version.suffix
+      - version
+      - ocaml-version *)
+  val by_name : t -> string -> Value.t Option.t
+end
+
+(** Data of a Coq configuration. *)
+type t
+
+(** [make ~coqc] runs coqc --config and returns the configuration data. Exceptionally, one
+    of the following will happen:
+
+    - Return [Error message] if coqc --config exits with a non-zero code.
+    - Throw a user error if coqc --config is not parsable.
+    - Throw an [Action.Prog.Not_found] exception if the coqc binary is not found. *)
+val make : coqc:Action.Prog.t -> (t, User_message.Style.t Pp.t) result Memo.t
+
 (** [by_name t name] returns the value of the option [name] in the Coq
     configuration [t]. If the value is not available then [None] is returned.
     Throws a code error if an invalid [name] is requested.
 
     Currently supported names are:
 
-    - version.major
-    - version.minor
-    - version.revision
-    - version.suffix
-    - version
-    - ocaml-version
     - coqlib
     - coqcorelib
     - coq_native_compiler_default *)

diff --git a/test/blackbox-tests/test-cases/coq/failed-config.t/run.t b/test/blackbox-tests/test-cases/coq/failed-config.t/run.t
@@ -101,25 +101,19 @@ Here we query the version of Coq. Due to the expansion of %{coq:_} macros we nee
   >   (echo %{coq:version})))
   > EOF
 
-Fails for now, but could be improved in the future.
+Succeeds after PR #10631
   $ FAIL_CONFIG=1 \
   > dune build @version
-  File "dune", line 4, characters 8-22:
-  4 |   (echo %{coq:version})))
-              ^^^^^^^^^^^^^^
-  Error: Could not expand %{coq:version} as running coqc --config failed.
-  $TESTCASE_ROOT/bin/coqc --config failed with exit code 1.
-  Hint: coqc --config requires the coq-stdlib package in order to function
-  properly.
-  [1]
+  8.16.1
 
 Should fail.
   $ FAIL_VERSION=1 \
   > dune build @version
-  Error: Could not parse coqc version: 
+  File "dune", line 4, characters 8-22:
+  4 |   (echo %{coq:version})))
+              ^^^^^^^^^^^^^^
+  Error: Could not expand %{coq:version} as running coqc failed.
   $TESTCASE_ROOT/bin/coqc --print-version failed with exit code 1.
-  -> required by %{coq:version} at dune:4
-  -> required by alias version in dune:1
   [1]
 
 Here we query the config. A failing --config will block this value from being realised
@@ -139,10 +133,8 @@ Should fail.
   File "dune", line 4, characters 8-21:
   4 |   (echo %{coq:coqlib})))
               ^^^^^^^^^^^^^
-  Error: Could not expand %{coq:coqlib} as running coqc --config failed.
+  Error: Could not expand %{coq:coqlib} as running coqc failed.
   $TESTCASE_ROOT/bin/coqc --config failed with exit code 1.
-  Hint: coqc --config requires the coq-stdlib package in order to function
-  properly.
   [1]
 
 Should succeed.
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		- Don't depend on coq-stdlib being installed when expanding variables
		of the `coq.version` family (#10631, fixes #10629, @gares)