Merge branch 'master' into fix-HOAS-primproj

.github/workflows/nix-action-coq-8.19.yml

@@ -314,6 +314,7 @@ jobs:
     - coq
     - mathcomp-classical
     - mathcomp-field
+    - mathcomp-bigenough
     - hierarchy-builder
     runs-on: ubuntu-latest
     steps:
@@ -368,6 +369,10 @@ jobs:
       name: 'Building/fetching previous CI target: mathcomp-field'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
         --argstr job "mathcomp-field"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-bigenough'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
+        --argstr job "mathcomp-bigenough"
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: hierarchy-builder'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
@@ -376,6 +381,63 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
         --argstr job "mathcomp-analysis"
+  mathcomp-bigenough:
+    needs:
+    - coq
+    - mathcomp-ssreflect
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to initially checkout
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
+        \ }}\" >> $GITHUB_ENV\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.target_commit }}
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
+        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
+        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
+        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
+        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
+        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
+        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v20
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq-elpi
+      uses: cachix/cachix-action@v12
+      with:
+        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+        extraPullNames: coq, coq-community, math-comp
+        name: coq-elpi
+    - id: stepCheck
+      name: Checking presence of CI target mathcomp-bigenough
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"coq-8.19\" --argstr job \"mathcomp-bigenough\" \\\n   --dry-run\
+        \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\
+        \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
+        --argstr job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
+        --argstr job "mathcomp-ssreflect"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: Building/fetching current CI target
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
+        --argstr job "mathcomp-bigenough"
   mathcomp-character:
     needs:
     - coq

.gitignore

@@ -48,3 +48,4 @@ META
 apps/coercion/src/coq_elpi_coercion_hook.ml
 .filestoinstall
 apps/tc/src/coq_elpi_tc_hook.ml
+apps/cs/src/coq_elpi_cs_hook.ml

.nix/config.nix

@@ -16,13 +16,13 @@
       odd-order.override.version = "master";
       odd-order.job = true;
 
-      mathcomp-analysis.override.version = "hierarchy-builder";
+      mathcomp-analysis.override.version = "master";
       mathcomp-analysis.job = true;
 
       mathcomp-finmap.override.version = "master";
       mathcomp-finmap.job = true;
 
-      mathcomp-classical.override.version = "hierarchy-builder";
+      mathcomp-classical.override.version = "master";
       mathcomp-classical.job = true;
 
       mathcomp-single-planB-src.job = false;

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"4e48948fa8252a2fc755182abdd4b199f4798724"
+"dd771a5001cd955514f2462cad7cdd90377530e3"

.nix/coq-overlays/coq-elpi/default.nix

@@ -10,7 +10,7 @@ with builtins; with lib; let
     { case = "8.16"; out = { version = "1.17.0"; };}
     { case = "8.17"; out = { version = "1.17.0"; };}
     { case = "8.18"; out = { version = "v1.18.1"; };}
-    { case = "8.19"; out = { version = "v1.18.1"; };}
+    { case = "8.19"; out = { version = "v1.18.2"; };}
   ] {} );
 in mkCoqDerivation {
   pname = "elpi";

.ocamlformat

@@ -0,0 +1 @@
+m=120

Changelog.md

@@ -2,11 +2,47 @@
 
 ## UNRELEASED
 
-### API:
+### Commands
+- New `Elpi Accumulate dbname File filename` allows to accumulate a file int a db
+- Change `Elpi Db` now only creates (and initialises) a database for the specified phase
+
+### API
+- New `coq.parse-attributes` support for the `attlabel` specification,
+  see `coq-lib-common.elpi` for its documentation.
+- New `coq.goal->pp`
+- Replace `coq.replay-all-missing-synterp-actions` by (nestable) groups of actions
+- New `coq.begin-synterp-group` and `coq.end-synterp-group` primitives
+- New `coq.replay-synterp-action-group` primitive (replaces `coq.replay-all-missing-synterp-actions` in conjunction with a group)
+- New `coq.replay-next-synterp-actions` to replay all synterp actions until the next beginning/end of a synterp group
 - New `coq.primitive.projection-unfolded` to fold/unfold a primitive projection.
   Note that unfolded primitive projections are still compact terms, but they
   are displayed as `match` expressions and some Ltac code can see that.
 
+## [2.0.2] - 01/02/2024
+
+Requires Elpi 1.18.2 and Coq 8.19.
+
+### API
+- Fix `coq.elaborate-*` does not erase the type annotation of `Let`s (regression
+  introduced in 2.0.1). This fix may introduce differences in generated names
+- Fix `coq.elaborate-*` are not affected anymore by printing options
+
+### Commands
+- Fix install the right initial parsing state (the one before any synterp action
+  is re-played)
+
+### HOAS
+- Fix evar instantiation loss when crossing the elpi/ltac border
+- Fix encoding of "definitional classes" (`Class` with no record)
+- Fix order of implicit arguments of `Record`
+
+### Misc
+- Change requiring `elpi` does not load primitive integers nor primitive floats
+
+### Apps
+- TC: avoid declaring options twice (could make vscoq2 fail)
+- CS: `cs` now takes a context, a term that is the projection of some structure applied to the parameters of the structure, a term to put a structure on and the solution to return
+
 ## [2.0.1] - 29/12/2023
 
 Requires Elpi 1.18.1 and Coq 8.19.

Makefile

@@ -21,7 +21,7 @@ export ELPIDIR
 
 DEPS=$(ELPIDIR)/elpi.cmxa $(ELPIDIR)/elpi.cma
 
-APPS=$(addprefix apps/, derive eltac NES locker coercion tc)
+APPS=$(addprefix apps/, derive eltac NES locker coercion cs tc)
 
 ifeq "$(COQ_ELPI_ALREADY_INSTALLED)" ""
 DOCDEP=build
@@ -151,3 +151,6 @@ SPACE=$(XXX) $(YYY)
 apps/%.vo: force
 	@$(MAKE) -C apps/$(word 1,$(subst /, ,$*)) \
 		$(subst $(SPACE),/,$(wordlist 2,99,$(subst /, ,$*))).vo
+
+nix:
+	nix-shell --arg do-nothing true --run "updateNixToolBox & genNixActions"

README.md

@@ -1,4 +1,6 @@
-[![Actions Status](https://github.com/LPCIC/coq-elpi/workflows/CI/badge.svg)](https://github.com/LPCIC/coq-elpi/actions)
+[![Docker CI](https://github.com/LPCIC/coq-elpi/actions/workflows/main.yml/badge.svg)](https://github.com/LPCIC/coq-elpi/actions/workflows/main.yml)
+[![Nix CI](https://github.com/LPCIC/coq-elpi/actions/workflows/nix-action-coq-8.19.yml/badge.svg)](https://github.com/LPCIC/coq-elpi/actions/workflows/nix-action-coq-8.19.yml)
+[![DOC](https://github.com/LPCIC/coq-elpi/actions/workflows/doc.yml/badge.svg)](https://github.com/LPCIC/coq-elpi/actions/workflows/doc.yml)
 [![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users.20.26.20devs)
 <img align="right" src="https://github.com/LPCIC/coq-elpi/raw/master/etc/logo.png" alt="Coq-Elpi logo" width="25%" />
 
@@ -179,14 +181,13 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`.
   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands).
 - `Elpi Program <qname> <code>` lower level primitive letting one crate a
   command/tactic with a custom preamble `<code>`.
-
-- `Elpi Accumulate [<qname>] [<code>|File <filename> From <loadpath>|Db <dbname>]`
-  adds code to the current program (or `<qname>` if specified).
+- `From some.load.path Extra Dependency <filename> as <fname>`.
+- `Elpi Accumulate [<dbname>|<qname>] [<code>|File <fname>|Db <dbname>]`
+  adds code to the current program (or `<dbname>` or `<qname>` if specified).
   The code can be verbatim, from a file or a Db.
+  File names `<fname>` must have been previously declared with the above command.
   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.
   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
 - `Elpi Typecheck [<qname>]` typechecks the current program (or `<qname>` if
   specified).
@@ -289,11 +290,23 @@ The synterp-command can output data of that type, but also any other data it
 wishes.
 
 The second way to communicate data is implicit, but limited to synterp actions.
-During the interp phase commands can use the `coq.next-synterp-action` API to
-peek into the list of actions yet to be performed.
-Once an action is performed, the API reveals the next one. See also the
-related utilities `coq.replay-synterp-action` and
-`coq.replay-all-missing-synterp-actions`.
+Such synterp actions can be recorded into (nested) groups whose structure is
+declared using well-bracketed calls to predicates `coq.begin-synterp-group`
+and `coq.end-synterp-group` in the synterp phase. In the interp phase, one can
+then use predicate `coq.replay-synterp-action-group` to replay all the synterp
+actions of the group with the given name at once.
+
+In the case where one wishes to interleave code between the actions of a given
+group, it is also possible to match the synterp group structure at interp, via
+`coq.begin-synterp-group` and `coq.end-synterp-group`. Individual actions that
+are contained in the group then need to be replayed individually.
+
+One can use `coq.replay-next-synterp-actions` to replay all synterp actions
+until the next beginning/end of a synterp group. However, this is discouraged
+in favour of using groups explicitly, as this is more modular. Code that used
+to rely on the now-removed `coq.replay-all-missing-synterp-actions` predicate
+can rely on `coq.replay-next-synterp-actions` instead, but this is discouraged
+in favour of using groups explicitly)
 
 ##### Syntax of the `#[phase]` attribute
 

_CoqProject

@@ -29,6 +29,11 @@
 -R apps/coercion/tests          elpi.apps.tc.coercion
 -I apps/coercion/src
 
+# CS
+-R apps/cs/theories       elpi.apps.cs
+-R apps/cs/tests          elpi.apps.tc.cs
+-I apps/cs/src
+
 # Type classes
 -R apps/tc/theories       elpi.apps.tc
 -R apps/tc/tests          elpi.apps.tc.tests

_CoqProject.test

@@ -55,3 +55,5 @@ tests/test_link_order_import3.v
 tests/test_query_extra_dep.v
 tests/test_toposort.v
 tests/test_synterp.v
+tests/test_checker.v
+tests/test_replay.v

apps/NES/elpi/nes_interp.elpi

@@ -8,6 +8,15 @@ print-path Path PP :- std.do! [
   coq.say {coq.pp->string Out},
 ].
 
+pred begin-path.
+begin-path :- coq.replay-synterp-action-group "nes.begin-path".
+
+pred end-path.
+end-path :- coq.replay-synterp-action-group "nes.end-path".
+
+pred open-path.
+open-path :- coq.replay-synterp-action-group "nes.open-path".
+
 namespace print {
 
   pred pp-list i:list A, i:(A -> coq.pp -> prop), o:coq.pp.
@@ -82,4 +91,4 @@ namespace print {
 }
 
 
-}
+}

apps/NES/elpi/nes_synterp.elpi

@@ -89,8 +89,12 @@ pred ns->string i:list string, o:string.
 ns->string NS S :- std.string.concat "." NS S.
 
 pred begin-path i:list string, o:list prop.
-begin-path [] [].
+begin-path [] [] :- std.do! [
+  coq.begin-synterp-group "nes.begin-path" Group,
+  coq.end-synterp-group Group,
+].
 begin-path ([_|_] as Path) Out :- std.do! [
+  coq.begin-synterp-group "nes.begin-path" Group,
   coq.env.current-path CP,
   if (open-ns _ NSCP) (std.assert! (NSCP = CP) "NS: cannot begin a namespace inside a module that is inside a namespace") true,
   std.map {std.findall (open-ns Y_ P_)} open-ns->string Stack,
@@ -107,7 +111,7 @@ begin-path ([_|_] as Path) Out :- std.do! [
   iter<- Stack {std.rev Path} begin-ns [] Out,
 
   open-super-path Path [],
-
+  coq.end-synterp-group Group,
 ].
 
 pred std.time-do! i:list prop.
@@ -118,18 +122,25 @@ std.time-do! [P|PS] :-
   std.time-do! PS.
 
 pred end-path i:list string, o:list prop.
-end-path [] [].
+end-path [] [] :- std.do! [
+  coq.begin-synterp-group "nes.end-path" Group,
+  coq.end-synterp-group Group,
+].
 end-path ([_|_] as Path) Out :- std.do! [
+  coq.begin-synterp-group "nes.end-path" Group,
   std.map {std.findall (open-ns X_ P_)} nes.open-ns->string Stack,
   std.assert! (std.appendR {std.rev Path} Bottom Stack) "NES: Ending a namespace that is not begun",
   nes.iter-> Bottom {std.rev Path} nes.end-ns [] Out,
+  coq.end-synterp-group Group,
 ].
 
 
 pred open-path i:list string.
 open-path Path :- std.do! [
+  coq.begin-synterp-group "nes.open-path" Group,
   std.map {std.findall (ns Path M_)} nes.ns->modpath Mods,
-  std.forall Mods coq.env.import-module
+  std.forall Mods coq.env.import-module,
+  coq.end-synterp-group Group,
 ].
 
 pred open-super-path i:list string, i:list string.

apps/NES/tests/test_NES.v

@@ -74,4 +74,4 @@ NES.Begin X.
 Module Y.
 Fail NES.Begin Z.
 End Y.
-NES.End X.
+NES.End X.

apps/NES/tests/test_NES_lib.v

@@ -1,25 +1,26 @@
 From elpi.apps.NES Extra Dependency "nes_synterp.elpi" as nes_synterp.
+From elpi.apps.NES Extra Dependency "nes_interp.elpi" as nes_interp.
 From elpi.apps Require Import NES.
 
 Elpi Command Make.
-#[synterp] Elpi Accumulate Db NES.db.
+#[phase="both"] Elpi Accumulate Db NES.db.
 #[synterp] Elpi Accumulate File nes_synterp.
+#[interp] Elpi Accumulate File nes_interp.
 #[synterp] Elpi Accumulate lp:{{
 
-  main-synterp [str Path] ActionsToOpen :- std.do! [
+  main [str Path] :- std.do! [
     nes.string->ns Path NS,
     nes.begin-path NS OpenNS,
-    coq.synterp-actions ActionsToOpen,
     OpenNS => nes.end-path NS _NewNS,
   ].
   main _ :- coq.error "usage: Make <DotSeparatedPath>".
 
 }}.
 #[interp] Elpi Accumulate lp:{{
-  main-interp [str _] ActionsBefore :- std.do! [
-    std.forall ActionsBefore coq.replay-synterp-action,
+  main _ :- std.do! [
+    nes.begin-path,
     coq.env.add-const "x" {{ 42 }} _ @transparent! _C,
-    coq.replay-all-missing-synterp-actions,
+    nes.end-path,
   ].
 }}.
 Elpi Typecheck.