Merge pull request #966 from LPCIC/revamp-ltac-API

ltac: API for simple tactics

Author: gares

.nix/config.nix

@@ -14,15 +14,15 @@ let master = [
     "trakt"
   ];
   rocq-common-bundles = {
-    rocq-elpi.override.elpi-version = "3.4.2";
+    rocq-elpi.override.elpi-version = "v3.6.1";
     hierarchy-builder.override.version = "master";
     rocq-elpi-tests.job = true;
     rocq-elpi-tests-stdlib.job = true;
   };
   coq-common-bundles = listToAttrs (forEach master (p:
     { name = p; value.override.version = "master"; }))
   // {
-    coq-elpi.override.elpi-version = "3.4.2";
+    coq-elpi.override.elpi-version = "v3.6.1";
 
     mathcomp-boot.job = true;
     mathcomp-fingroup.job = true;

Changelog.md

@@ -1,5 +1,7 @@
 # Unreleased
 
+Requires Elpi 3.6.0 and Rocq 9.0, 9.1 or 9.2.
+
 ### HOAS:
 - Fix explicitly declared goals are considered reachable, even if they
   do not occur in the proof term
@@ -13,6 +15,12 @@
 - New `coq.env.section-contents` listing the contents of sections.
 - New `coq.ltac.call-mltac` to call code defined via `TACTIC EXTEND` directives
   in OCaml.
+- New `coq.ltac.call-simple-mltac` for tactics not changing the proof context
+- New `coq.ltac.call-simple-ltac1` for tactics not changing the proof context
+- Rename `coq.ltac.collect-goals` -> `coq.ltac.collect-sealed-goals`
+- New `coq.ltac.collect-simple-goals` for goals in the current proof context
+- Change `coq.ltac.call-ltac1` also gives a diagnostic
+- Change `coq.ltac.call` also gives a diagnostic
 
 # [3.2.0] 19/09/2025
 

apps/coercion/README.md

@@ -61,7 +61,7 @@ coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [
   Solution = {{ @exist lp:Ty lp:P lp:X1 _ }},
   % we call the solver
   coq.ltac.collect-goals Solution [G] [],
-  coq.ltac.open (coq.ltac.call-ltac1 "my_solver") G [],
+  coq.ltac.open (x\y\coq.ltac.call-ltac1 "my_solver" x y ok) G [],
 ].
 
 }}.

apps/coercion/tests/test_open.v

@@ -12,7 +12,7 @@ coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [
   Solution = {{ @exist lp:Ty lp:P lp:X1 _ }},
   % we call the solver
   coq.ltac.collect-goals Solution [G] [],
-  coq.ltac.open (coq.ltac.call-ltac1 "my_solver") G [],
+  coq.ltac.open (x\y\coq.ltac.call-ltac1 "my_solver" x y ok) G [],
 ].
 
 }}.

apps/derive/elpi/eqbcorrect.elpi

@@ -128,7 +128,7 @@ search-eqcorrect-apply (eqb.inductive _ _) [] C R C R.
 
 func run-solver sealed-goal, string ->.
 run-solver G Name :-
-  if (coq.ltac.open (coq.ltac.call Name []) G []) true
+  if (coq.ltac.open (g\gl\coq.ltac.call Name [] g gl ok) G []) true
      ((@holes! => coq.sealed-goal->string G SG),
       std.fatal-error {calc ( "solver " ^ Name ^ " fails on goal:\n" ^ SG )}).
 

builtin-doc/coq-builtin.elpi

@@ -1634,7 +1634,7 @@ kind ltac1-tactic type.
 % Level can be left unspecified and defaults to 0
 external type coq.ltac.fail int -> variadic any (func).
 
-% [coq.ltac.collect-goals T Goals ShelvedGoals] 
+% [coq.ltac.collect-sealed-goals T Goals ShelvedGoals] 
 % Turns the holes in T into Goals.
 % Goals are closed with nablas.
 % ShelvedGoals are goals which can be solved by side effect (they occur
@@ -1643,11 +1643,23 @@ external type coq.ltac.fail int -> variadic any (func).
 % (a
 % fold_left over the terms, letin body comes before the type).
 % 
-external func coq.ltac.collect-goals term -> list sealed-goal, 
-                                    list sealed-goal.
+external func coq.ltac.collect-sealed-goals term -> list sealed-goal, 
+                                           list sealed-goal.
 
-% [coq.ltac.call-mltac PluginName BlockName BlockIndex G GL] Calls OCaml
-% code bound via TACTIC EXTEND. For example the
+
+func coq.ltac.collect-goals term -> list sealed-goal, list sealed-goal.
+coq.ltac.collect-goals T GA GB :- coq.ltac.collect-sealed-goals T GA GB.
+
+
+% [coq.ltac.collect-simple-goals T Goals ShelvedGoals] Like
+% coq.ltac.collect-sealed-goals turns the holes in T into
+% Goals but fails if the goals do not live in the current proof context.
+% 
+external func coq.ltac.collect-simple-goals term -> list goal, 
+                                           list sealed-goal.
+
+% [coq.ltac.call-mltac PluginName BlockName BlockIndex G GL Diagnostic]
+% Calls OCaml code bound via TACTIC EXTEND. For example the
 % OCaml code for lia looks like:
 % 
 %   DECLARE PLUGIN "rocq-runtime.plugins.micromega"
@@ -1665,13 +1677,27 @@ external func coq.ltac.collect-goals term -> list sealed-goal,
 % numbering
 % starts from 0. Also, each block has a name, "Lia" in this case.
 %     
+% When the diagnostic is (error Msg), then GL is not set.
+% 
 % Supported attributes:
 % - @no-tc! (default false, do not infer typeclasses)
 external func coq.ltac.call-mltac string, string, int, 
-                                 goal -> list sealed-goal.
+                                 goal -> list sealed-goal, diagnostic.
 
-% [coq.ltac.call-ltac1 Tac G GL] Calls Ltac1 tactic Tac on goal G (passing
-% the arguments of G, see coq.ltac.call for a handy wrapper).
+% [coq.ltac.call-simple-mltac PluginName BlockName BlockIndex G GL
+% Diagnostic] Like coq.ltac.call-mltac but Tac is not allowed to
+% generate new goals GL in different contexts. For example "intro" does
+% not
+% obey this restriction.
+% 
+% Supported attributes:
+% - @no-tc! (default false, do not infer typeclasses)
+external func coq.ltac.call-simple-mltac string, string, int, 
+                                        goal -> list goal, diagnostic.
+
+% [coq.ltac.call-ltac1 Tac G GL ...] Calls Ltac1 tactic Tac on goal G
+% (passing the arguments of G, see coq.ltac.call for a handy wrapper).
+% It accepts one diagnostic argument, defaults to ok if omitted.
 % Tac can either be a string (the tactic name), or a value
 % of type ltac1-tactic, see the tac argument constructor
 % and the ltac_tactic:(...) syntax to pass arguments to
@@ -1681,9 +1707,24 @@ external func coq.ltac.call-mltac string, string, int,
 %   "Ltac name := body", it cannot be a builtin one. For example
 %   "Ltac myapply x := apply x." lets one call apply by running
 %   coq.ltac.call-ltac1 "myapply" G GL.
+% 
+% When the diagnostic is (error Msg), then GL is not set.
+% 
+% Supported attributes:
+% - @no-tc! (default false, do not infer typeclasses)
+external func coq.ltac.call-ltac1 any, goal -> list sealed-goal, 
+                                 diagnostic.. .
+
+% [coq.ltac.call-simple-ltac1 Tac G GL Diagnostic] Like coq.ltac.call-ltac1
+% but Tac is not allowed to
+% generate new goals GL in different contexts. For example "intro" does
+% not
+% obey this restriction.
+% 
 % Supported attributes:
 % - @no-tc! (default false, do not infer typeclasses)
-external func coq.ltac.call-ltac1 any, goal -> list sealed-goal.
+external func coq.ltac.call-simple-ltac1 any, goal -> list goal, 
+                                        diagnostic.
 
 % [coq.ltac.id-free? ID G] 
 %     Fails if ID is already used in G. Note that ids which are taken are