Merge pull request #579 from proux01/no_primitive

Don't Require PrimInt63 and PrimFloat by default

.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

.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;

apps/derive/theories/derive/eq.v

@@ -9,15 +9,17 @@ From Coq Require Import Bool.
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.
 
+From Coq Require Import PrimInt63 PrimFloat.
+
 Register Coq.Numbers.Cyclic.Int63.PrimInt63.eqb as elpi.derive.eq_unit63.
 Register Coq.Floats.PrimFloat.eqb as elpi.derive.eq_float64.
 
 Elpi Db derive.eq.db lp:{{
 
 % full resolution (composes with eq functions for parameters)
 type eq-db term -> term -> term -> prop.
-eq-db {{ lib:elpi.uint63 }} {{ lib:elpi.uint63 }} {{ lib:elpi.derive.eq_unit63 }} :- !.
-eq-db {{ lib:elpi.float64 }} {{ lib:elpi.float64 }} {{ lib:elpi.derive.eq_float64 }} :- !.
+eq-db {{ lib:num.int63.type }} {{ lib:num.int63.type }} {{ lib:elpi.derive.eq_unit63 }} :- !.
+eq-db {{ lib:num.float.type }} {{ lib:num.float.type }} {{ lib:elpi.derive.eq_float64 }} :- !.
 
 :name "eq-db:fail"
 eq-db A B F :-

apps/derive/theories/derive/eqType_ast.v

@@ -1,4 +1,5 @@
 From elpi Require Import elpi.
+From Coq Require Import PrimInt63 PrimFloat.
 From elpi.apps Require Import derive.
 
 From elpi.apps.derive Extra Dependency "eqType.elpi" as eqType.

apps/derive/theories/derive/eqcorrect.v

@@ -22,8 +22,8 @@ Register uint63_eq_correct as elpi.derive.uint63_eq_correct.
 Elpi Db derive.eqcorrect.db lp:{{
   type eqcorrect-db gref -> term -> prop.
 
-eqcorrect-db X {{ lib:elpi.derive.uint63_eq_correct }} :- {{ lib:elpi.uint63 }} = global X, !.
-eqcorrect-db X _ :- {{ lib:elpi.float64 }} = global X, !, stop "float64 comparison is not syntactic".
+eqcorrect-db X {{ lib:elpi.derive.uint63_eq_correct }} :- {{ lib:num.int63.type }} = global X, !.
+eqcorrect-db X _ :- {{ lib:num.float.type }} = global X, !, stop "float64 comparison is not syntactic".
 
 :name "eqcorrect-db:fail"
 eqcorrect-db T _ :-

apps/derive/theories/derive/param1.v

@@ -40,6 +40,8 @@ Class reali {X : Type} {XR : X -> Type} (x : X) (xR : XR x) := Reali {}.
 
 Register store_reali as param1.store_reali.
 
+From Coq Require Import PrimInt63 PrimFloat.
+
 Inductive is_uint63 : PrimInt63.int -> Type := uint63 (i : PrimInt63.int) : is_uint63 i.
 Register is_uint63 as elpi.derive.is_uint63.
 
@@ -55,8 +57,8 @@ pred reali-done i:gref.
 :index(3)
 pred reali i:term, o:term.
 
-reali {{ lib:elpi.uint63 }} {{ lib:elpi.derive.is_uint63 }} :- !.
-reali {{ lib:elpi.float64 }} {{ lib:elpi.derive.is_float64 }} :- !.
+reali {{ lib:num.int63.type }} {{ lib:elpi.derive.is_uint63 }} :- !.
+reali {{ lib:num.float.type }} {{ lib:elpi.derive.is_float64 }} :- !.
 
 :name "reali:fail"
 reali X _ :-
@@ -66,8 +68,8 @@ reali X _ :-
 
 type realiR term -> term -> prop.
 
-realiR {{ lib:elpi.uint63 }} {{ lib:elpi.derive.is_uint63 }} :- !.
-realiR {{ lib:elpi.float64 }} {{ lib:elpi.derive.is_float64 }} :- !.
+realiR {{ lib:num.int63.type }} {{ lib:elpi.derive.is_uint63 }} :- !.
+realiR {{ lib:num.float.type }} {{ lib:elpi.derive.is_float64 }} :- !.
 
 :name "realiR:fail"
 realiR T TR :-

elpi/elpi_elaborator.elpi

@@ -308,8 +308,8 @@ of (global GR as X) T X :- coq.env.typeof GR T1, unify-leq T1 T.
 of (pglobal GR I as X) T X :-
   @uinstance! I => coq.env.typeof GR T1, unify-leq T1 T.
 
-of (primitive (uint63 _) as X) T X :- unify-leq {{ lib:elpi.uint63 }} T.
-of (primitive (float64 _) as X) T X :- unify-leq {{ lib:elpi.float64 }} T.
+of (primitive (uint63 _) as X) T X :- unify-leq {{ lib:num.int63.type }} T.
+of (primitive (float64 _) as X) T X :- unify-leq {{ lib:num.float.type }} T.
 
 of (uvar as X) T Y :- !, evar X T Y.
 

src/coq_elpi_vernacular_syntax.mlg

@@ -59,6 +59,15 @@ let warning_legacy_accumulate_gen =
 let warning_legacy_accumulate ?loc () = warning_legacy_accumulate_gen ?loc true
 let warning_legacy_accumulate2 ?loc () = warning_legacy_accumulate_gen ?loc false
 
+let lib_ref id =
+  let id = String.concat "." (snd id) in
+  try Coqlib.lib_ref id
+  with Coqlib.NotFoundRef _ ->
+    CErrors.user_err
+      Pp.(str "Global reference not found: lib:" ++ str id
+          ++ str " (you may need to require some .v file with \
+                  `Register ... as " ++ str id ++ str ".`).")
+
 }
 GRAMMAR EXTEND Gram
   GLOBAL: term;
@@ -84,11 +93,11 @@ GRAMMAR EXTEND Gram
 
   term: LEVEL "0"
     [ [ "lib"; ":"; id = qualified_name -> {
-          let ref = Coqlib.lib_ref (String.concat "." (snd id)) in
+          let ref = lib_ref id in
           let path = Nametab.path_of_global ref in
           CAst.make ~loc Constrexpr.(CRef (Libnames.qualid_of_path ~loc:(fst id) path,None)) }
       | "lib"; ":"; "@"; id = qualified_name -> {
-          let ref = Coqlib.lib_ref (String.concat "." (snd id)) in
+          let ref = lib_ref id in
           let path = Nametab.path_of_global ref in
           let f = Libnames.qualid_of_path ~loc:(fst id) path in
           CAst.make ~loc Constrexpr.(CAppExpl((f,None),[])) } ] ]

tests/test_elaborator.v

@@ -1,5 +1,6 @@
 From unreleased Extra Dependency "elpi_elaborator.elpi" as elab.
 
+From Coq Require Import PrimInt63 PrimFloat.
 From elpi Require Import elpi.
 
 Elpi Command test.refiner.

theories/elpi.v

@@ -45,8 +45,3 @@ From Coq Require Bool.
 Register Coq.Bool.Bool.reflect  as elpi.reflect.
 Register Coq.Bool.Bool.ReflectF as elpi.ReflectF.
 Register Coq.Bool.Bool.ReflectT as elpi.ReflectT.
-
-From Coq Require PrimFloat PrimInt63.
-
-Register Coq.Floats.PrimFloat.float as elpi.float64.
-Register Coq.Numbers.Cyclic.Int63.PrimInt63.int as elpi.uint63.