use elpi 2.0.7

Changelog.md

@@ -1,3 +1,11 @@
+# UNRELEASED
+
+Requires Elpi 2.0.7 and Coq 8.20.
+
+### API
+- Change `coq.env.add-section-variable` now takes the implicit status of the
+  variable
+
 # [2.3.0] - 6/12/2024
 
 Requires Elpi 2.0.3 and Coq 8.20.

coq-elpi.opam

@@ -17,7 +17,7 @@ bug-reports: "https://github.com/LPCIC/coq-elpi/issues"
 depends: [
   "dune" {>= "3.13"}
   "ocaml" {>= "4.10.0"}
-  "elpi" {>= "2.0.3" & < "2.1.0~"}
+  "elpi" {>= "2.0.7" & < "2.1.0~"}
   "coq" {>= "8.20+rc1" & < "8.21~"}
   "ppx_optcomp"
   "ocaml-lsp-server" {with-dev-setup}

etc/dune

@@ -15,5 +15,5 @@
  (name version_parser)
  (public_name coq_elpi_version_parser)
  (modules version_parser)
- (libraries str)
+ (libraries str elpi)
  (package coq-elpi))

etc/version_parser.ml

@@ -1,19 +1,9 @@
 
-let is_number x = try let _ = int_of_string x in true with _ -> false ;;
-
 let main () =
   let v = Sys.argv.(1) in
-  let v' = Str.(replace_first (regexp "^v") "" v) in     (* v1.20... -> 1.20... *)
-  let v' = Str.(replace_first (regexp "-.*$") "" v') in  (* ...-10-fjdnfs -> ... *)
-  let l = String.split_on_char '.' v' in
-  (* sanitization *)
-  let l =
-    match l with
-    | l when List.for_all is_number l -> l
-    | [_] -> ["99";"99";"99"]
-    | _ -> Printf.eprintf "version_parser: cannot parse: %s\n" v; exit 1 in
+  let a,b,c = Elpi.API.Utils.version_parser ~what:"elpi" v in
   let open Format in
-  printf "(%a)%!" (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ", ") pp_print_string) l
+  printf "(%d,%d,%d)%!" a b c
 ;;
 
 main ()

src/coq_elpi_programs.ml

@@ -959,12 +959,21 @@ let file_resolver ?cwd:_ ~unit:file () =
 
 (***********************************************************************)
 
+let versions =
+  let open API.Setup.StrMap in
+  empty
+  |> add "coq-elpi" (API.Utils.version_parser ~what:"coq-elpi" "%%VERSION_NUM%%")
+  |> add "rocq-elpi" (API.Utils.version_parser ~what:"rocq-elpi" "%%VERSION_NUM%%")
+  |> add "coq" (API.Utils.version_parser ~what:"coq" Coq_config.version)
+  |> add "rocq" (API.Utils.version_parser ~what:"rocq" Coq_config.version)
+
 module Synterp : Programs = struct
   module S = struct
     let stage = Summary.Stage.Synterp
     let in_stage x = x ^ "-synterp"
     let init () =
-      API.Setup.init ~state:synterp_state ~hoas:synterp_hoas
+      API.Setup.init ~versions
+        ~state:synterp_state ~hoas:synterp_hoas
         ~quotations:synterp_quotations ~builtins:[elpi_builtins;coq_synterp_builtins] ~file_resolver ()
   end
   include SourcesStorage(S)
@@ -986,7 +995,8 @@ module Interp : Programs = struct
     let stage = Summary.Stage.Interp
     let in_stage x = x ^ "-interp"
     let init () =
-      API.Setup.init ~state:interp_state ~hoas:interp_hoas
+      API.Setup.init ~versions
+        ~state:interp_state ~hoas:interp_hoas
         ~quotations:interp_quotations ~builtins:[elpi_builtins;coq_interp_builtins] ~file_resolver ()
   end)
 

src/coq_elpi_utils.ml

@@ -785,21 +785,7 @@ let option_map_acc2 f s = function
 let option_default f = function Some x -> x | None -> f ()
 
 let coq_version_parser version =
-  let ( !! ) x = try int_of_string x with Failure _ -> -100 in
-  match Str.split (Str.regexp_string ".") version with
-  | major :: minor :: patch :: _ -> (!!major, !!minor, !!patch)
-  | [ major ] -> (!!major, 0, 0)
-  | [] -> (0, 0, 0)
-  | [ major; minor ] -> (
-      match Str.split (Str.regexp_string "+") minor with
-      | [ minor ] -> (!!major, !!minor, 0)
-      | [] -> (!!major, !!minor, 0)
-      | minor :: prerelease :: _ ->
-          if Str.string_match (Str.regexp_string "beta") prerelease 0 then
-            (!!major, !!minor, !!("-" ^ String.sub prerelease 4 (String.length prerelease - 4)))
-          else if Str.string_match (Str.regexp_string "alpha") prerelease 0 then
-            (!!major, !!minor, !!("-" ^ String.sub prerelease 5 (String.length prerelease - 5)))
-          else (!!major, !!minor, -100))
+  Elpi.API.Utils.version_parser ~what:"coq" version
 
 let mp2path x =
   let open Names in

tests/test_API.v

@@ -11,6 +11,17 @@ Elpi Query lp:{{
   coq.say "Coq version:" V "=" MA "." MI "." P.
 }}.
 
+Elpi Command version.
+Elpi Accumulate lp:{{
+
+% elpi:if version coq-elpi < 2.0.0
+main _ :- coq.error "bad".
+% elpi:endif
+
+main _ :- true.
+
+}}.
+Elpi version.
 
 (****** say *************************************)