Merge pull request #339 from LPCIC/new-resolver

Prepare Coq-Elpi 1.13

Changelog.md

@@ -1,21 +1,34 @@
 # Changelog
 
-## UNRELEASED
+## [1.13.0] - 08-02-2022
 
 ### Performance
 - New 1 slot cache for context read back to improve the speed of FFI calls
   needing to read back a large `coq_context`
 - New `Conversion.t` for `gref` handwritten to minimize allocations
 - New terms of the form `(global ...)` are now hashconsed
+- New `extra_goals` postprocessing removing `declare-evar/rm-evar` pairs which
+  happen naturally writing code like `coq.unify-eq {{ f _ x }} {{ f y _ }}`
+  (the `_` are solved immediately, no need to declare them to elpi)
 
 ### API
 - New `coq.hints.opaque`
 - New `coq.hints.set-opaque`
 - Change load `coq.ltac.*` also in commands (and not just tactics) so that
   commands can easily turn holes into goals and inhabit them calling regular
-  tactics. 
-
-## [1.12.1] - 20-01-2021
+  tactics.
+- New `coq.hints.add-resolve`
+- Fix `coq.option.add` survives the end of a file
+- New `coq.env.begin-module-functor`
+- New `coq.env.begin-module-type-functor`
+- New `coq.env.apply-module-functor`
+- New `coq.env.apply-module-type-functor`
+- New `coq.inline` with constructors `coq.inline.no`, `coq.inline.at` and
+  `coq.inline.default`
+- New `@inline-at! N` and `@inline!` macros
+- Change `coq.env.add-axiom` honors `@inline` macros
+
+## [1.12.1] - 20-01-2022
 
 Requires Elpi 1.13.6 and Coq 8.15.
 

Makefile.coq.local

@@ -1,5 +1,6 @@
 CAMLPKGS+= -package elpi,stdlib-shims
 CAMLFLAGS+= -bin-annot -g
+OCAMLWARN+=-warn-error -32
 
 theories/elpi.vo: $(wildcard elpi/*.elpi)
 

README.md

@@ -55,7 +55,7 @@ At the time of writing Proof General does not handle quotations correctly, see P
 In particular `Elpi Accumulate lp:{{ .... }}.` is used in tutorials to mix Coq and Elpi code
 without escaping. Coq-Elpi also accepts `Elpi Accumulate " .... ".` but strings part of the
 Elpi code needs to be escaped. Finally, for non-tutorial material, one can always put
-the code in an external file and use `Elpi Accumulate File "filename".` instead.
+the code in an external file and use `Elpi Accumulate File "filename" From some.load.path.` instead.
 
 CoqIDE does not handle quotations correctly. The installation process puts
 [coq-elpi.lang](etc/coq-elpi.lang)
@@ -179,11 +179,13 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`.
 - `Elpi Program <qname> <code>` lower level primitive letting one crate a
   command/tactic with a custom preamble `<code>`.
 
-- `Elpi Accumulate [<qname>] [<code>|File <filename>|Db <dbname>]` adds code to
-  the current program (or `<qname>` if specified). The code can be verbatim,
-  from a file or a Db. It understands the `#[skip="rex"]` and `#[only="rex"]`
-  which make the command a no op if the Coq version is matched (or not) by the
-  given regular expression.
+- `Elpi Accumulate [<qname>] [<code>|File <filename> From <loadpath>|Db <dbname>]`
+  adds code to the current program (or `<qname>` if specified).
+  The code can be verbatim, from a file or a Db.
+  It understands the `#[skip="rex"]` and `#[only="rex"]` which make the command
+  a no op if the Coq version is matched (or not) by the given regular expression.
+  File names are relative to the directory mapped to `<loadpath>`; if more than
+  one such directory exists, the `<filename>` must exists only once.
 - `Elpi Typecheck [<qname>]` typechecks the current program (or `<qname>` if
   specified).
 - `Elpi Debug <string>` sets the variable `<string>`, relevant for conditional

_CoqProject

@@ -6,6 +6,7 @@
 -Q src      elpi
 -Q apps/derive/tests elpi.apps.derive.tests
 -Q tests    elpi.tests
+-Q elpi     elpi
 
 -R apps/derive/theories elpi.apps
 -R apps/derive/tests    elpi.apps.derive.tests

_CoqProject.test

@@ -5,6 +5,8 @@
 -Q examples elpi.examples
 -Q tests    elpi.tests
 -I src/
+-Q elpi     unreleased
+-docroot elpi
 
 examples/tutorial_elpi_lang.v
 examples/tutorial_coq_elpi_HOAS.v

apps/NES/_CoqProject

@@ -1,8 +1,10 @@
 # Hack to see Coq-Elpi even if it is not installed yet
 -Q ../../theories elpi
 -I ../../src
+-docroot elpi.apps
 
 -R theories elpi.apps
+-Q elpi elpi.apps.NES
 
 theories/NES.v
 

apps/NES/_CoqProject.test

@@ -1,6 +1,7 @@
 # Hack to see Coq-Elpi even if it is not installed yet
 -Q ../../theories elpi
 -I ../../src
+-docroot elpi.apps
 
 -R theories elpi.apps
 -R tests    elpi.apps.NES.tests

apps/NES/theories/NES.v

@@ -15,7 +15,7 @@ pred ns o:path, o:modpath.
 
 Elpi Command NES.Status.
 Elpi Accumulate Db NES.db.
-Elpi Accumulate File "elpi/nes.elpi".
+Elpi Accumulate File "nes.elpi" From elpi.apps.NES.
 Elpi Accumulate lp:{{
 
 main _ :-
@@ -29,7 +29,7 @@ Elpi Typecheck.
 Elpi Export NES.Status.
 
 Elpi Command NES.Begin.
-Elpi Accumulate File "elpi/nes.elpi".
+Elpi Accumulate File "nes.elpi" From elpi.apps.NES.
 Elpi Accumulate lp:{{
 
   main [str NS] :- nes.begin-path {nes.string->ns NS}.
@@ -41,7 +41,7 @@ Elpi Typecheck.
 Elpi Export NES.Begin.
 
 Elpi Command NES.End.
-Elpi Accumulate File "elpi/nes.elpi".
+Elpi Accumulate File "nes.elpi" From elpi.apps.NES.
 Elpi Accumulate lp:{{
 
   main [str NS] :- nes.end-path {nes.string->ns NS}.
@@ -55,7 +55,7 @@ Elpi Export NES.End.
 
 Elpi Command NES.Open.
 Elpi Accumulate Db NES.db.
-Elpi Accumulate File "elpi/nes.elpi".
+Elpi Accumulate File "nes.elpi" From elpi.apps.NES.
 Elpi Accumulate lp:{{
 
   main [str NS] :- nes.open-path {nes.string->ns NS}.

apps/derive/Makefile.coq.local

@@ -11,13 +11,13 @@ theories/derive/eqOK_trivial.vo: elpi/eqOK_trivial.elpi
 theories/derive/idx2inv.vo: elpi/idx2inv.elpi
 theories/derive/isK.vo: elpi/isK.elpi
 theories/derive/param1_functor.vo: elpi/param1_functor.elpi
-theories/derive/param1.vo: elpi/param1.elpi paramX-lib.elpi
+theories/derive/param1.vo: elpi/param1.elpi elpi/paramX-lib.elpi
 theories/derive/eqcorrect.vo: elpi/eqcorrect.elpi
 theories/derive/eqOK.vo: elpi/eqOK.elpi
 theories/derive/induction.vo: elpi/induction.elpi
 theories/derive/map.vo: elpi/map.elpi
 theories/derive/param1_inhab.vo: elpi/param1_inhab.elpi
-theories/derive/param2.vo: elpi/param2.elpi paramX-lib.elpi
+theories/derive/param2.vo: elpi/param2.elpi elpi/paramX-lib.elpi
 theories/derive/lens.vo: elpi/lens.elpi
 theories/derive/lens_laws.vo: elpi/lens_laws.elpi
 

apps/derive/_CoqProject

@@ -1,8 +1,10 @@
 # Hack to see Coq-Elpi even if it is not installed yet
 -Q ../../theories elpi
 -I ../../src
+-docroot elpi.apps
 
 -R theories elpi.apps
+-Q elpi elpi.apps.derive
 
 theories/derive.v
 theories/derive/bcongr.v

apps/derive/theories/derive.v

@@ -70,64 +70,64 @@ From elpi.apps Require Export
 Elpi Command derive.
 
 Elpi Accumulate Db derive.eq.db.
-Elpi Accumulate File "elpi/eq.elpi".
+Elpi Accumulate File "eq.elpi" From elpi.apps.derive.
 
 Elpi Accumulate Db derive.isK.db.
-Elpi Accumulate File "elpi/isK.elpi".
+Elpi Accumulate File "isK.elpi" From elpi.apps.derive.
 
 Elpi Accumulate Db derive.map.db.
-Elpi Accumulate File "elpi/map.elpi".
+Elpi Accumulate File "map.elpi" From elpi.apps.derive.
 
 Elpi Accumulate Db derive.projK.db.
-Elpi Accumulate File "elpi/projK.elpi".
+Elpi Accumulate File "projK.elpi" From elpi.apps.derive.
 
-Elpi Accumulate File "paramX-lib.elpi".
+Elpi Accumulate File "paramX-lib.elpi" From elpi.apps.derive.
 
-Elpi Accumulate File "elpi/param1.elpi".
+Elpi Accumulate File "param1.elpi" From elpi.apps.derive.
 Elpi Accumulate Db derive.param1.db.
 
 Elpi Accumulate Db derive.param1.functor.db.
-Elpi Accumulate File "elpi/param1_functor.elpi".
+Elpi Accumulate File "param1_functor.elpi" From elpi.apps.derive.
 
 Elpi Accumulate Db derive.param1.congr.db.
-Elpi Accumulate File "elpi/param1_congr.elpi".
+Elpi Accumulate File "param1_congr.elpi" From elpi.apps.derive.
 
 Elpi Accumulate Db derive.param1.inhab.db.
-Elpi Accumulate File "elpi/param1_inhab.elpi".
+Elpi Accumulate File "param1_inhab.elpi" From elpi.apps.derive.
 
 Elpi Accumulate Db derive.param1.trivial.db.
-Elpi Accumulate File "elpi/param1_trivial.elpi".
+Elpi Accumulate File "param1_trivial.elpi" From elpi.apps.derive.
 
 Elpi Accumulate Db derive.invert.db.
-Elpi Accumulate File "elpi/invert.elpi".
+Elpi Accumulate File "invert.elpi" From elpi.apps.derive.
 
 Elpi Accumulate Db derive.idx2inv.db.
-Elpi Accumulate File "elpi/idx2inv.elpi".
+Elpi Accumulate File "idx2inv.elpi" From elpi.apps.derive.
 
 Elpi Accumulate Db derive.induction.db.
-Elpi Accumulate File "elpi/induction.elpi".
+Elpi Accumulate File "induction.elpi" From elpi.apps.derive.
 
 Elpi Accumulate Db derive.bcongr.db.
-Elpi Accumulate File "elpi/injection.elpi".
-Elpi Accumulate File "elpi/bcongr.elpi".
+Elpi Accumulate File "injection.elpi" From elpi.apps.derive.
+Elpi Accumulate File "bcongr.elpi" From elpi.apps.derive.
 
 Elpi Accumulate Db derive.eqK.db.
-Elpi Accumulate File "elpi/discriminate.elpi".
-Elpi Accumulate File "elpi/eqK.elpi".
+Elpi Accumulate File "discriminate.elpi" From elpi.apps.derive.
+Elpi Accumulate File "eqK.elpi" From elpi.apps.derive.
 
 Elpi Accumulate Db derive.eqcorrect.db.
-Elpi Accumulate File "elpi/eqcorrect.elpi".
+Elpi Accumulate File "eqcorrect.elpi" From elpi.apps.derive.
 
-Elpi Accumulate File "elpi/eqOK.elpi".
+Elpi Accumulate File "eqOK.elpi" From elpi.apps.derive.
 
-Elpi Accumulate File "elpi/param2.elpi".
+Elpi Accumulate File "param2.elpi" From elpi.apps.derive.
 Elpi Accumulate Db derive.param2.db.
 
-Elpi Accumulate File "elpi/lens.elpi".
+Elpi Accumulate File "lens.elpi" From elpi.apps.derive.
 Elpi Accumulate Db derive.lens.db.
-Elpi Accumulate File "elpi/lens_laws.elpi".
+Elpi Accumulate File "lens_laws.elpi" From elpi.apps.derive.
 
-Elpi Accumulate File "elpi/derive.elpi".
+Elpi Accumulate File "derive.elpi" From elpi.apps.derive.
 Elpi Accumulate lp:{{
 
 % runs P in a context where Coq #[attributes] are parsed

apps/derive/theories/derive/bcongr.v

@@ -28,8 +28,8 @@ bcongr-db K _ :-
 Elpi Command derive.bcongr.
 Elpi Accumulate Db derive.bcongr.db.
 Elpi Accumulate Db derive.projK.db.
-Elpi Accumulate File "elpi/injection.elpi".
-Elpi Accumulate File "elpi/bcongr.elpi".
+Elpi Accumulate File "injection.elpi" From elpi.apps.derive.
+Elpi Accumulate File "bcongr.elpi" From elpi.apps.derive.
 Elpi Accumulate lp:{{
   main [str I, str O] :- !, coq.locate I (indt GR), derive.bcongr.main GR O _.
   main [str I] :- !,

apps/derive/theories/derive/cast.v

@@ -9,7 +9,7 @@ Elpi Db derive.cast.db lp:{{ type cast-db int -> term -> prop. }}.
 
 Elpi Command derive.cast.
 Elpi Accumulate Db derive.cast.db.
-Elpi Accumulate File "elpi/cast.elpi".
+Elpi Accumulate File "cast.elpi" From elpi.apps.derive.
 Elpi Accumulate  lp:{{
 
 main [int N] :-

apps/derive/theories/derive/eq.v

@@ -33,7 +33,7 @@ type eq-for inductive -> constant -> prop.
 
 Elpi Command derive.eq.
 Elpi Accumulate Db derive.eq.db.
-Elpi Accumulate File "elpi/eq.elpi".
+Elpi Accumulate File "eq.elpi" From elpi.apps.derive.
 Elpi Accumulate lp:{{
   main [str I, str O] :- !, coq.locate I (indt GR), derive.eq.main GR O _.
   main [str I] :- !, 

apps/derive/theories/derive/eqK.v

@@ -40,11 +40,11 @@ eqK-db K _ :-
 
 Elpi Command derive.eqK.
 Elpi Accumulate Db derive.isK.db.
-Elpi Accumulate File "elpi/discriminate.elpi".
+Elpi Accumulate File "discriminate.elpi" From elpi.apps.derive.
 Elpi Accumulate Db derive.bcongr.db.
 Elpi Accumulate Db derive.eq.db.
 Elpi Accumulate Db derive.eqK.db.
-Elpi Accumulate File "elpi/eqK.elpi".
+Elpi Accumulate File "eqK.elpi" From elpi.apps.derive.
 Elpi Accumulate lp:{{
   main [str I, str Prefix] :- !, coq.locate I (indt GR), derive.eqK.main GR Prefix _.
   main [str I] :- !, coq.locate I (indt GR), derive.eqK.main GR "eq_axiom_" _.

apps/derive/theories/derive/eqOK.v

@@ -8,14 +8,14 @@ From elpi Require Export elpi. From elpi.apps Require Export  derive.param1 deri
 
 Elpi Command derive.eqOK.
 
-Elpi Accumulate File "paramX-lib.elpi".
-Elpi Accumulate File "elpi/param1.elpi".
+Elpi Accumulate File "paramX-lib.elpi" From elpi.apps.derive.
+Elpi Accumulate File "param1.elpi" From elpi.apps.derive.
 Elpi Accumulate Db derive.param1.db.
 Elpi Accumulate Db derive.param1.inhab.db.
 Elpi Accumulate Db derive.param1.trivial.db.
 Elpi Accumulate Db derive.eqcorrect.db.
 
-Elpi Accumulate File "elpi/eqOK.elpi".
+Elpi Accumulate File "eqOK.elpi" From elpi.apps.derive.
 Elpi Accumulate lp:{{
   main [str I, str O] :- !, coq.locate I (indt GR), derive.eqOK.main GR O _.
   main [str I] :- !,

apps/derive/theories/derive/eqcorrect.v

@@ -35,7 +35,7 @@ Elpi Accumulate Db derive.param1.functor.db.
 Elpi Accumulate Db derive.eq.db.
 Elpi Accumulate Db derive.eqK.db.
 Elpi Accumulate Db derive.eqcorrect.db.
-Elpi Accumulate File "elpi/eqcorrect.elpi".
+Elpi Accumulate File "eqcorrect.elpi" From elpi.apps.derive.
 Elpi Accumulate lp:{{
   main [str I, str Name] :- !, coq.locate I (indt GR), derive.eqcorrect.main GR Name _.
   main [str I] :- !, coq.locate I (indt GR), coq.gref->id (indt GR) ID, Name is ID ^ "_eq_correct", derive.eqcorrect.main GR Name _.

apps/derive/theories/derive/idx2inv.v

@@ -11,13 +11,13 @@ Elpi Db derive.idx2inv.db lp:{{
 }}.
 
 Elpi Command derive.idx2inv.
-Elpi Accumulate File "paramX-lib.elpi".
+Elpi Accumulate File "paramX-lib.elpi" From elpi.apps.derive.
 Elpi Accumulate Db derive.param1.db.
 Elpi Accumulate Db derive.param1.functor.db.
-Elpi Accumulate File "elpi/param1_functor.elpi".
+Elpi Accumulate File "param1_functor.elpi" From elpi.apps.derive.
 Elpi Accumulate Db derive.invert.db.
 Elpi Accumulate Db derive.idx2inv.db.
-Elpi Accumulate File "elpi/idx2inv.elpi".
+Elpi Accumulate File "idx2inv.elpi" From elpi.apps.derive.
 Elpi Accumulate lp:{{
   main [str I, str O] :- !, coq.locate I (indt GR), derive.idx2inv.main GR O _.
   main [str I] :- !, coq.locate I (indt GR), derive.idx2inv.main GR "_to_" _.

apps/derive/theories/derive/induction.v

@@ -18,14 +18,14 @@ induction-db T _ :-
 
 Elpi Command derive.induction.
 
-Elpi Accumulate File "paramX-lib.elpi".
-Elpi Accumulate File "elpi/param1.elpi".
+Elpi Accumulate File "paramX-lib.elpi" From elpi.apps.derive.
+Elpi Accumulate File "param1.elpi" From elpi.apps.derive.
 Elpi Accumulate Db derive.param1.db.
 
 Elpi Accumulate Db derive.param1.functor.db.
 
 Elpi Accumulate Db derive.induction.db.
-Elpi Accumulate File "elpi/induction.elpi".
+Elpi Accumulate File "induction.elpi" From elpi.apps.derive.
 Elpi Accumulate lp:{{
   main [str I, str O] :- !, coq.locate I (indt GR), derive.induction.main GR O _.
   main [str I] :- !,

apps/derive/theories/derive/invert.v

@@ -10,7 +10,7 @@ Elpi Db derive.invert.db lp:{{ type invert-db gref -> gref -> prop. }}.
 
 Elpi Command derive.invert.
 Elpi Accumulate Db derive.invert.db.
-Elpi Accumulate File "elpi/invert.elpi".
+Elpi Accumulate File "invert.elpi" From elpi.apps.derive.
 Elpi Accumulate lp:{{
   main [str I, str O] :- !, coq.locate I (indt GR), derive.invert.main GR O _.
   main [str I] :- !, coq.locate I (indt GR), derive.invert.main GR "_inv" _.

apps/derive/theories/derive/isK.v

@@ -19,7 +19,7 @@ Elpi Db derive.isK.db lp:{{
 
 Elpi Command derive.isK.
 Elpi Accumulate Db derive.isK.db.
-Elpi Accumulate File "elpi/isK.elpi".
+Elpi Accumulate File "isK.elpi" From elpi.apps.derive.
 Elpi Accumulate lp:{{
   main [str I,str O] :- !, coq.locate I (indt GR), derive.isK.main GR O _.
   main [str I] :- !,

apps/derive/theories/derive/lens.v

@@ -26,7 +26,7 @@ Elpi Db derive.lens.db lp:{{
 }}.
 
 Elpi Command derive.lens.
-Elpi Accumulate File "elpi/lens.elpi".
+Elpi Accumulate File "lens.elpi" From elpi.apps.derive.
 Elpi Accumulate Db derive.lens.db.
 Elpi Accumulate lp:{{ 
   main [str I, str O] :- !, coq.locate I (indt GR), derive.lens.main GR O _.