ifdefs on elpi version in source code

Author: gares

coq-elpi.opam

@@ -19,7 +19,7 @@ depends: [
   "ocaml" {>= "4.10.0"}
   "stdlib-shims"
   "elpi" {>= "1.18.2" & < "1.20.0~"}
-  "coq" {>= "8.20" & < "8.21"}
+  "coq" {>= "8.20+rc1" & < "8.21~"}
   "ppx_optcomp"
   "ocaml-lsp-server" {with-dev-setup}
   "odoc" {with-doc}

etc/dune

@@ -9,4 +9,11 @@
  (public_name coq_elpi_optcomp)
  (modules optcomp)
  (libraries str)
+ (package coq-elpi))
+
+(executable
+ (name version_parser)
+ (public_name coq_elpi_version_parser)
+ (modules version_parser)
+ (libraries str)
  (package coq-elpi))

etc/version_parser.ml

@@ -0,0 +1,17 @@
+
+let is_number x = try let _ = int_of_string x in true with _ -> false ;;
+
+let main () =
+  let v = Sys.argv.(1) in
+  let l = String.split_on_char '.' Str.(replace_first (regexp "^v") "" v) in
+  (* sanitization *)
+  let l =
+    match l with
+    | l when List.for_all is_number l -> l
+    | ["%%VERSION_NUM%%"] -> ["99";"99";"99"]
+    | _ -> Printf.eprintf "version_parser: cannot parse: %s\n" v; exit 1 in
+  let open Format in
+  printf "(%a)%!" (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ", ") pp_print_string) l
+;;
+
+main ()

src/coq_elpi_builtins_synterp.ml

@@ -2,6 +2,8 @@
 (* license: GNU Lesser General Public License Version 2.1 or later           *)
 (* ------------------------------------------------------------------------- *)
 
+[%%import "coq_elpi_config.mlh"]
+
 module API = Elpi.API
 module State = API.State
 module Conv = API.Conversion
@@ -150,6 +152,12 @@ let invocation_site_loc_synterp : API.Ast.Loc.t State.component =
   ~init:(fun () -> API.Ast.Loc.initial "(should-not-happen)")
   ~start:(fun x -> x) ()
 
+[%%if elpi >= (1, 20, 0)]
+let compat_graft x = x
+[%%else]
+let compat_graft = Option.map (function `Remove, _ -> nYI "clause removal" | ((`Replace | `Before | `After), _) as x -> x)
+[%%endif]
+
 type accumulation_item = qualified_name * API.Ast.program * Id.t list * Coq_elpi_utils.clause_scope
 let accumulate_clauses ~clauses_for_later ~accumulate_to_db ~preprocess_clause ~scope ~dbname clauses ~depth ~options state =
   let invocation_loc = State.get invocation_site_loc_synterp state in
@@ -158,7 +166,7 @@ let accumulate_clauses ~clauses_for_later ~accumulate_to_db ~preprocess_clause ~
   let clauses scope =
    clauses |> CList.rev_map (fun (name,graft,clause) ->
      let vars, clause = preprocess_clause ~depth clause in
-     let graft = Option.map (function `Remove, _ -> nYI "clause removal" | ((`Replace | `Before | `After), _) as x -> x) graft in
+     let graft = compat_graft graft in
      let clause = U.clause_of_term ?name ?graft ~depth loc clause in
      (dbname,clause,vars,scope)) in
   let local = (options : options).local = Some true in

src/dune

@@ -3,6 +3,7 @@
  (public_name coq-elpi.elpi)
  (synopsis "Elpi")
  (flags :standard -w -27)
+ (preprocessor_deps coq_elpi_config.mlh)
  (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")"))
  (libraries coq-core.plugins.ltac coq-core.vernac elpi))
 
@@ -30,7 +31,20 @@
   (target coq_elpi_config.ml)
   (action (with-stdout-to %{target}
     (progn
+      (echo "(* Automatically generated, don't edit *)\n")
+      (echo "[%%import \"coq_elpi_config.mlh\"]\n")
+      (echo "let elpi_version = \"%{version:elpi}\"\n")
       (echo "let elpi2html = \"%{lib:elpi:elpi2html.elpi}\";;")))))
 
+(rule
+  (target coq_elpi_config.mlh)
+  (action (with-stdout-to %{target}
+    (progn
+      (echo "(* Automatically generated, don't edit *)\n")
+      (echo "[%%define elpi ")
+      (run coq_elpi_version_parser %{version:elpi})
+      (echo "]\n")))))
+
+
 (coq.pp
  (modules coq_elpi_vernacular_syntax coq_elpi_arg_syntax))