feature(coq): coq_version variable

src/dune_lang/pform.ml

@@ -46,6 +46,7 @@ module Var = struct
     | Corrected_suffix
     | Inline_tests
     | Toolchain
+    | Coq_version
 
   let compare : t -> t -> Ordering.t = Poly.compare
 
@@ -97,6 +98,7 @@ module Var = struct
         | Corrected_suffix -> "Corrected_suffix"
         | Inline_tests -> "Inline_tests"
         | Toolchain -> "Toolchain"
+        | Coq_version -> "Coq_version"
       in
       Dyn.Variant (cstr, [])
 end
@@ -299,6 +301,7 @@ let encode_to_latest_dune_lang_version t =
       | Corrected_suffix -> Some "corrected-suffix"
       | Inline_tests -> Some "inline_tests"
       | Toolchain -> Some "toolchain"
+      | Coq_version -> Some "coq_version"
     with
     | None -> Pform_was_deleted
     | Some name -> Success { name; payload = None })
@@ -482,6 +485,7 @@ module Env = struct
         ; ("corrected-suffix", No_info Corrected_suffix)
         ; ("inline_tests", No_info Inline_tests)
         ; ("toolchains", since ~version:(3, 0) Var.Toolchain)
+        ; ("coq_version", since ~version:(3, 4) Var.Coq_version)
         ]
       in
       String.Map.of_list_exn (List.concat [ lowercased; uppercased; other ])

src/dune_lang/pform.mli

@@ -46,6 +46,7 @@ module Var : sig
     | Corrected_suffix
     | Inline_tests
     | Toolchain
+    | Coq_version
 
   val compare : t -> t -> Ordering.t
 

src/dune_rules/coq_config.ml

@@ -0,0 +1,16 @@
+open Import
+open Memo.O
+
+let impl bin =
+  let* _ = Build_system.build_file bin in
+  let+ line =
+    Memo.of_non_reproducible_fiber
+    @@ Process.run_capture_line Process.Strict bin [ "--print-version" ]
+  in
+  match String.lsplit2 ~on:' ' line with
+  | Some (coq, _ocaml) -> Some coq
+  | None -> None
+
+let memo = Memo.create "coq-version" ~input:(module Path) impl
+
+let version ~bin = Memo.exec memo bin

src/dune_rules/coq_config.mli

@@ -0,0 +1,3 @@
+open Import
+
+val version : bin:Path.t -> string option Memo.t

src/dune_rules/expander.ml

@@ -368,6 +368,21 @@ let expand_pform_gen ~(context : Context.t) ~bindings ~dir ~source
             With
               (let* cc = Action_builder.of_memo (cc t) in
                cc.c))
+      | Coq_version ->
+        Need_full_expander
+          (fun t ->
+            Without
+              (let open Memo.O in
+              let* bin =
+                Artifacts.Bin.binary t.bin_artifacts_host ~loc:None "coqc"
+              in
+              match bin with
+              | Error _ -> failwith "TODO"
+              | Ok bin -> (
+                let+ res = Coq_config.version ~bin in
+                match res with
+                | None -> failwith "bad version"
+                | Some s -> [ Value.String s ])))
       | Cxx ->
         Need_full_expander
           (fun t ->

test/blackbox-tests/test-cases/coq/coq-version/coq-version.t

@@ -0,0 +1,19 @@
+  $ cat >dune-project <<EOF
+  > (lang dune 3.4)
+  > EOF
+
+  $ cat >dune <<EOF
+  > (rule
+  >  (action (with-stdout-to file (echo "8.15.2")))
+  >  (enabled_if (= %{coq_version} "8.15.2")))
+  > (rule
+  >  (action (with-stdout-to file (echo "8.15.1")))
+  >  (enabled_if (= %{coq_version} "8.15.1")))
+  > EOF
+
+  $ dune build ./file
+
+  $ cat _build/default/file
+  8.15.2
+
+  (>= 8.15.0-x12gn1 8.15.1) => false

test/blackbox-tests/test-cases/coq/coq-version/in-workspace.t/bin/coqc.ml

@@ -0,0 +1 @@
+let () = print_endline "1.2.3 x_x_x"

test/blackbox-tests/test-cases/coq/coq-version/in-workspace.t/bin/dune

@@ -0,0 +1,3 @@
+(executable
+ (libraries axsxasdsdads)
+ (public_name coqc))

test/blackbox-tests/test-cases/coq/coq-version/in-workspace.t/dune-project

@@ -0,0 +1,4 @@
+(lang dune 3.4)
+
+(package
+ (name foo))

test/blackbox-tests/test-cases/coq/coq-version/in-workspace.t/run.t

@@ -0,0 +1,27 @@
+
+#  $ cat >dune <<EOF
+#  > (rule
+#  >  (action (with-stdout-to file (echo %{coq_version}))))
+#  > EOF
+#
+#  $ dune build ./file
+#  $ cat _build/default/file
+
+  $ mkdir sub
+  $ cat >sub/dune <<EOF
+  > (rule
+  >  (enabled_if (>= %{coq_version} 8.15))
+  >  (action (with-stdout-to file (echo 123))))
+  > EOF
+
+  $ cat >dune <<EOF
+  > (rule
+  >  (action (with-stdout-to alwayspresent (echo 123))))
+  > EOF
+
+  $ dune build ./alwayspresent
+
+  (coq.theory
+   (name foo)
+   (native_theories mathcomp)
+   (theories mathcomp))