Merge pull request #584 from LPCIC/coq-8.18+fixes

Coq 8.18+fixes

.github/workflows/main.yml

@@ -9,7 +9,7 @@ on:
     branches: [ master ]
     tags: [ "v*.*.*" ]
   pull_request:
-    branches: [ master ]
+    branches: [ coq-8.18 ]
 jobs:
   build:
     runs-on: ubuntu-latest

Changelog.md

@@ -1,5 +1,13 @@
 # Changelog
 
+## [2.0.0.1] - 31/01/2024
+
+Requires Elpi 1.18.1 and Coq 8.18.
+
+Minor fixes backported from 2.0.2:
+- synterp initial state
+- loss of evars when calling ltac
+
 ## [2.0.0] - 23/12/2023
 
 Requires Elpi 1.18.1 and Coq 8.18.

coq-builtin-synterp.elpi

@@ -306,10 +306,12 @@ external pred coq.env.current-section-path o:list string.
 kind clause type.
 type clause id -> grafting -> prop -> clause.
 
-% Specify if the clause has to be grafted before or after a named clause
+% Specify if the clause has to be grafted before, grafted after or replace
+% a named clause
 kind grafting type.
 type before id -> grafting.
 type after id -> grafting.
+type replace id -> grafting.
 
 % Specify to which module the clause should be attached to
 kind scope type.

coq-builtin.elpi

@@ -1711,10 +1711,12 @@ external pred coq.extra-dep i:id, o:option id.
 kind clause type.
 type clause id -> grafting -> prop -> clause.
 
-% Specify if the clause has to be grafted before or after a named clause
+% Specify if the clause has to be grafted before, grafted after or replace
+% a named clause
 kind grafting type.
 type before id -> grafting.
 type after id -> grafting.
+type replace id -> grafting.
 
 % Specify to which module the clause should be attached to
 kind scope type.

coq-elpi.opam

@@ -15,7 +15,7 @@ install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
 depends: [
   "ocaml" {>= "4.09.0" }
   "stdlib-shims"
-  "elpi" {>= "1.18.1" & < "1.19.0~"}
+  "elpi" {= "1.18.1"}
   "coq" {>= "8.18" & < "8.19~" }
   "dot-merlin-reader" {with-dev}
   "ocaml-lsp-server" {with-dev}

examples/example_abs_evars.v

@@ -88,7 +88,7 @@ solve (goal _ _ _ _ [trm T] as G) GL :-
 solve (goal _ _ T _ [] as G) GL :-
   std.assert! (abs-evars T ClosedT N) "closure fails",
   coq.mk-app {{ (fun x : lp:ClosedT => x) _ }} {coq.mk-n-holes N} R,
-refine R G GL.
+  refine R G GL.
 
 }}.
 Elpi Typecheck.

src/coq_elpi_HOAS.ml

@@ -2402,7 +2402,10 @@ let get_declared_goals all_goals constraints state assignments pp_ctx =
 
 let rec reachable1 sigma root acc =
   let EvarInfo info = Evd.find sigma root in
-  let res = match Evd.evar_body info with Evd.Evar_empty -> Evar.Set.add root acc | Evd.Evar_defined _ -> acc in
+  let res =
+    match Evd.evar_body info with
+    | Evd.Evar_empty -> Evar.Set.add root acc
+    | Evd.Evar_defined d -> acc in
   let res = Evar.Set.union res @@ Evarutil.filtered_undefined_evars_of_evar_info sigma info in
   if Evar.Set.equal res acc then acc else reachable sigma res res
 and reachable sigma roots acc =
@@ -2420,13 +2423,14 @@ let reachable sigma roots acc =
 let solution2evd sigma0 { API.Data.constraints; assignments; state; pp_ctx } roots =
   let state, solved_goals, _, _gls = elpi_solution_to_coq_solution ~calldepth:0 constraints state in
   let sigma = get_sigma state in
-  let all_goals = reachable sigma roots Evar.Set.empty in
+  let roots = Evd.fold_undefined (fun k _ acc -> Evar.Set.add k acc) sigma0 roots in 
+  let reachable_undefined_evars = reachable sigma roots Evar.Set.empty in
   let declared_goals, shelved_goals =
-    get_declared_goals (Evar.Set.diff all_goals solved_goals) constraints state assignments pp_ctx in
+    get_declared_goals (Evar.Set.diff reachable_undefined_evars solved_goals) constraints state assignments pp_ctx in
   debug Pp.(fun () -> str "Goals: " ++ prlist_with_sep spc Evar.print declared_goals);
   debug Pp.(fun () -> str "Shelved Goals: " ++ prlist_with_sep spc Evar.print shelved_goals);
   Evd.fold_undefined (fun k _ sigma ->
-    if Evar.Set.mem k all_goals || Evd.mem sigma0 k then sigma
+    if Evar.Set.mem k reachable_undefined_evars then sigma
     else Evd.remove sigma k
     ) sigma sigma,
   declared_goals,

src/coq_elpi_vernacular.ml

@@ -567,10 +567,7 @@ module Interp = struct
         match syndata with
         | None -> [], fun ~target:_ ~depth -> Stdlib.Result.Ok ET.mkDiscard
         | Some (relocate_term,log) -> log, relocate_term in
-      let initial_synterp_state =
-        match synterplog with
-        | [] -> Vernacstate.Synterp.freeze ()
-        | x :: _ -> Coq_elpi_builtins_synterp.SynterpAction.synterp_state_after x in
+      let initial_synterp_state = Vernacstate.Synterp.freeze () in
       let query ~depth state =
         let state, args, gls = EU.map_acc
           (Coq_elpi_arg_HOAS.in_elpi_cmd ~depth ~raw:raw_args Coq_elpi_HOAS.(mk_coq_context ~options:(default_options ()) state))

tests/test_synterp.v

@@ -156,4 +156,22 @@ Elpi Accumulate Db db1.
 Elpi Accumulate lp:{{ main _. }}.
 #[synterp] Elpi Accumulate lp:{{ main _. }}.
 
-Elpi Typecheck.
+Elpi Typecheck.
+
+(* ********************************************* *)
+
+Set Implicit Arguments.
+Elpi Command foo3.
+Elpi Accumulate lp:{{
+  main _ :-
+    D = (record "foo" {{ Type }} "mkfoo" (field [] "f" {{ Type }} _\end-record)),
+    coq.typecheck-indt-decl D ok,
+    coq.env.add-indt D I, coq.env.begin-module "x" none, coq.env.end-module _.
+}}.
+#[synterp] Elpi Accumulate lp:{{
+  main _ :- coq.env.begin-module "x" none, coq.env.end-module _.
+}}.
+Elpi foo3.
+
+
+