Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Don't Require PrimInt63 and PrimFloat by default #579

Merged
merged 3 commits into from
Jan 29, 2024
Merged

Don't Require PrimInt63 and PrimFloat by default #579

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
69952aa
Don't Require PrimInt63 and PrimFloat by default
proux01 Jan 26, 2024
7641839
Improve error message for unfound lib:... globrefs
proux01 Jan 26, 2024
8ad13ee
[CI] Update Nix CI
proux01 Jan 28, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
62 changes: 62 additions & 0 deletions .github/workflows/nix-action-coq-8.19.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -314,6 +314,7 @@ jobs:
- coq
- mathcomp-classical
- mathcomp-field
- mathcomp-bigenough
- hierarchy-builder
runs-on: ubuntu-latest
steps:
Expand Down Expand Up @@ -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"
Expand All @@ -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
Expand Down
4 changes: 2 additions & 2 deletions .nix/config.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
6 changes: 4 additions & 2 deletions apps/derive/theories/derive/eq.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 :-
Expand Down
1 change: 1 addition & 0 deletions apps/derive/theories/derive/eqType_ast.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
Expand Down
4 changes: 2 additions & 2 deletions apps/derive/theories/derive/eqcorrect.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 _ :-
Expand Down
10 changes: 6 additions & 4 deletions apps/derive/theories/derive/param1.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand All @@ -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 _ :-
Expand All @@ -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 :-
Expand Down
4 changes: 2 additions & 2 deletions elpi/elpi_elaborator.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
13 changes: 11 additions & 2 deletions src/coq_elpi_vernacular_syntax.mlg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

not really related to this PR but looking up lib_ref and nametab during parsing is pretty bad with parsing/execution separated

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed...

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, this is really tricky. I do extend the Coq grammar, so there is a bug, but we only use it inside elpi code, hence inside a quotation. The text between {{ ... }} is parsed as a string, and the Coq parser is called at run time. So I think it is mostly fine for the use we make.

Anyway, lib: predates the ability of elpi to compile units, we don't need that anymore. So maybe it is just better to wipe it out.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe should we deprecate it first? In any case, that should probably happen in another PR.

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),[])) } ] ]
Expand Down
1 change: 1 addition & 0 deletions tests/test_elaborator.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
Expand Down
5 changes: 0 additions & 5 deletions theories/elpi.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Loading