Skip to content

Commit eed07eb

Browse files
garesgares
authored
Merge pull request #557 from LPCIC/fix-synterp
Support for synterp (Coq 8.18)
2 parents b92e2c8 + 03ce207 commit eed07eb

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

65 files changed

+5071
-2028
lines changed

‎.github/workflows/doc.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ jobs:
2525
- name: setup ocaml
2626
uses: avsm/setup-ocaml@v1
2727
with:
28-
ocaml-version: 4.09.1
28+
ocaml-version: 4.10.1
2929

3030
- name: install deps
3131
run: |

‎.github/workflows/main.yml‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,8 +18,7 @@ jobs:
1818
coq_version:
1919
- '8.18'
2020
ocaml_version:
21-
- '4.09-flambda'
22-
- '4.13-flambda'
21+
- '4.14-flambda'
2322
steps:
2423
- uses: actions/checkout@v2
2524
- uses: coq-community/docker-coq-action@v1

‎.github/workflows/nix-action-coq-8.18.yml‎

Lines changed: 78 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -462,6 +462,81 @@ jobs:
462462
name: Building/fetching current CI target
463463
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
464464
--argstr job "hierarchy-builder"
465+
interval:
466+
needs:
467+
- coq
468+
- coquelicot
469+
- mathcomp-ssreflect
470+
- mathcomp-fingroup
471+
runs-on: ubuntu-latest
472+
steps:
473+
- name: Determine which commit to initially checkout
474+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
475+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
476+
\ }}\" >> $GITHUB_ENV\nfi\n"
477+
- name: Git checkout
478+
uses: actions/checkout@v3
479+
with:
480+
fetch-depth: 0
481+
ref: ${{ env.target_commit }}
482+
- name: Determine which commit to test
483+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
484+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
485+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
486+
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
487+
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
488+
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
489+
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
490+
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
491+
- name: Git checkout
492+
uses: actions/checkout@v3
493+
with:
494+
fetch-depth: 0
495+
ref: ${{ env.tested_commit }}
496+
- name: Cachix install
497+
uses: cachix/install-nix-action@v20
498+
with:
499+
nix_path: nixpkgs=channel:nixpkgs-unstable
500+
- name: Cachix setup coq-elpi
501+
uses: cachix/cachix-action@v12
502+
with:
503+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
504+
extraPullNames: coq, coq-community, math-comp
505+
name: coq-elpi
506+
- id: stepCheck
507+
name: Checking presence of CI target interval
508+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
509+
\ bundle \"coq-8.18\" --argstr job \"interval\" \\\n --dry-run 2>&1 > /dev/null)\n\
510+
echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
511+
s/.*/built/\") >> $GITHUB_OUTPUT\n"
512+
- if: steps.stepCheck.outputs.status == 'built'
513+
name: 'Building/fetching previous CI target: coq'
514+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
515+
--argstr job "coq"
516+
- if: steps.stepCheck.outputs.status == 'built'
517+
name: 'Building/fetching previous CI target: bignums'
518+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
519+
--argstr job "bignums"
520+
- if: steps.stepCheck.outputs.status == 'built'
521+
name: 'Building/fetching previous CI target: coquelicot'
522+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
523+
--argstr job "coquelicot"
524+
- if: steps.stepCheck.outputs.status == 'built'
525+
name: 'Building/fetching previous CI target: flocq'
526+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
527+
--argstr job "flocq"
528+
- if: steps.stepCheck.outputs.status == 'built'
529+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
530+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
531+
--argstr job "mathcomp-ssreflect"
532+
- if: steps.stepCheck.outputs.status == 'built'
533+
name: 'Building/fetching previous CI target: mathcomp-fingroup'
534+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
535+
--argstr job "mathcomp-fingroup"
536+
- if: steps.stepCheck.outputs.status == 'built'
537+
name: Building/fetching current CI target
538+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
539+
--argstr job "interval"
465540
mathcomp:
466541
needs:
467542
- coq
@@ -1424,8 +1499,10 @@ name: Nix CI for bundle coq-8.18
14241499
'on':
14251500
pull_request:
14261501
paths:
1427-
- .github/workflows/**
1502+
- .github/workflows/nix-action-coq-8.18.yml
14281503
pull_request_target:
1504+
paths-ignore:
1505+
- .github/workflows/nix-action-coq-8.18.yml
14291506
types:
14301507
- opened
14311508
- synchronize

‎.nix/config.nix‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,13 @@
55
bundles = {
66

77
"coq-8.18".coqPackages = {
8-
hierarchy-builder.override.version = "master";
98
coq.override.version = "8.18";
9+
10+
hierarchy-builder.override.version = "coq-elpi-2";
1011
hierarchy-builder-shim.job = false;
1112

13+
coq-elpi.override.version = "fix-synterp";
14+
1215
mathcomp.override.version = "master";
1316
mathcomp.job = true;
1417

‎.nix/coq-nix-toolbox.nix‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
"e7a39f47847edcde691d7bf8f423e4806a1b660f"
1+
"68a4a68e689dca0d9c081a0f1b9a454379522d78"

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

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
{ lib, mkCoqDerivation, which, coq, version ? null }:
2+
3+
with builtins; with lib; let
4+
elpi = coq.ocamlPackages.elpi.override (lib.switch coq.coq-version [
5+
{ case = "8.11"; out = { version = "1.11.4"; };}
6+
{ case = "8.12"; out = { version = "1.12.0"; };}
7+
{ case = "8.13"; out = { version = "1.13.7"; };}
8+
{ case = "8.14"; out = { version = "1.13.7"; };}
9+
{ case = "8.15"; out = { version = "1.15.0"; };}
10+
{ case = "8.16"; out = { version = "1.17.0"; };}
11+
{ case = "8.17"; out = { version = "1.17.0"; };}
12+
{ case = "8.18"; out = { version = "v1.18.1"; };}
13+
] {} );
14+
in mkCoqDerivation {
15+
pname = "elpi";
16+
repo = "coq-elpi";
17+
owner = "LPCIC";
18+
inherit version;
19+
defaultVersion = lib.switch coq.coq-version [
20+
{ case = "8.18"; out = "1.19.0"; }
21+
{ case = "8.17"; out = "1.18.0"; }
22+
{ case = "8.16"; out = "1.15.6"; }
23+
{ case = "8.15"; out = "1.14.0"; }
24+
{ case = "8.14"; out = "1.11.2"; }
25+
{ case = "8.13"; out = "1.11.1"; }
26+
{ case = "8.12"; out = "1.8.3_8.12"; }
27+
{ case = "8.11"; out = "1.6.3_8.11"; }
28+
] null;
29+
release."1.19.0".sha256 = "sha256-kGoo61nJxeG/BqV+iQaV3iinwPStND+7+fYMxFkiKrQ=";
30+
release."1.18.0".sha256 = "sha256-2fCOlhqi4YkiL5n8SYHuc3pLH+DArf9zuMH7IhpBc2Y=";
31+
release."1.17.0".sha256 = "sha256-J8GatRKFU0ekNCG3V5dBI+FXypeHcLgC5QJYGYzFiEM=";
32+
release."1.15.6".sha256 = "sha256-qc0q01tW8NVm83801HHOBHe/7H1/F2WGDbKO6nCXfno=";
33+
release."1.15.1".sha256 = "sha256-NT2RlcIsFB9AvBhMxil4ZZIgx+KusMqDflj2HgQxsZg=";
34+
release."1.14.0".sha256 = "sha256:1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp";
35+
release."1.13.0".sha256 = "1j7s7dlnjbw222gnbrsjgmjck1yrx7h6hwm8zikcyxi0zys17w7n";
36+
release."1.12.1".sha256 = "sha256-4mO6/co7NcIQSGIQJyoO8lNWXr6dqz+bIYPO/G0cPkY=";
37+
release."1.11.2".sha256 = "0qk5cfh15y2zrja7267629dybd3irvxk1raz7z8qfir25a81ckd4";
38+
release."1.11.1".sha256 = "10j076vc2hdcbm15m6s7b6xdzibgfcbzlkgjnlkr2vv9k13qf8kc";
39+
release."1.10.1".sha256 = "1zsyx26dvj7pznfd2msl2w7zbw51q1nsdw0bdvdha6dga7ijf7xk";
40+
release."1.9.7".sha256 = "0rvn12h9dpk9s4pxy32p8j0a1h7ib7kg98iv1cbrdg25y5vs85n1";
41+
release."1.9.5".sha256 = "0gjdwmb6bvb5gh0a6ra48bz5fb3pr5kpxijb7a8mfydvar5i9qr6";
42+
release."1.9.4".sha256 = "0nii7238mya74f9g6147qmpg6gv6ic9b54x5v85nb6q60d9jh0jq";
43+
release."1.9.3".sha256 = "198irm800fx3n8n56vx1c6f626cizp1d7jfkrc6ba4iqhb62ma0z";
44+
release."1.9.2".sha256 = "1rr2fr8vjkc0is7vh1461aidz2iwkigdkp6bqss4hhv0c3ijnn07";
45+
release."1.8.3_8.12".sha256 = "15z2l4zy0qpw0ws7bvsmpmyv543aqghrfnl48nlwzn9q0v89p557";
46+
release."1.8.3_8.12".version = "1.8.3";
47+
release."1.8.2_8.12".sha256 = "1n6jwcdazvjgj8vsv2r9zgwpw5yqr5a1ndc2pwhmhqfl04b5dk4y";
48+
release."1.8.2_8.12".version = "1.8.2";
49+
release."1.8.1".sha256 = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r";
50+
release."1.8.0".sha256 = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1";
51+
release."1.7.0".sha256 = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8";
52+
release."1.6.3_8.11".sha256 = "1j340cr2bv95clzzkkfmsjkklham1mj84cmiyprzwv20q89zr1hp";
53+
release."1.6.3_8.11".version = "1.6.3";
54+
release."1.6.2_8.11".sha256 = "06xrx0ljilwp63ik2sxxr7h617dgbch042xfcnfpy5x96br147rn";
55+
release."1.6.2_8.11".version = "1.6.2";
56+
release."1.6.1_8.11".sha256 = "0yyyh35i1nb3pg4hw7cak15kj4y6y9l84nwar9k1ifdsagh5zq53";
57+
release."1.6.1_8.11".version = "1.6.1";
58+
release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq";
59+
release."1.6.0_8.11".version = "1.6.0";
60+
release."1.6.0".sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b";
61+
releaseRev = v: "v${v}";
62+
63+
buildFlags = [ "OCAMLWARN=" ];
64+
65+
mlPlugin = true;
66+
propagatedBuildInputs = [ coq.ocamlPackages.findlib elpi ];
67+
68+
meta = {
69+
description = "Coq plugin embedding ELPI.";
70+
maintainers = [ maintainers.cohencyril ];
71+
license = licenses.lgpl21Plus;
72+
};
73+
}

‎.nix/coq-overlays/hierarchy-builder/default.nix‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
{ lib, mkCoqDerivation, which, coq, coq-elpi,
2+
version ? null, shim ? false }:
3+
4+
with lib; mkCoqDerivation {
5+
pname = "hierarchy-builder" + optionalString shim "-shim";
6+
owner = "math-comp";
7+
inherit version;
8+
defaultVersion = with versions; switch coq.coq-version [
9+
{ case = range "8.13" "8.14"; out = "1.2.0"; }
10+
{ case = range "8.12" "8.13"; out = "1.1.0"; }
11+
{ case = isEq "8.11"; out = "0.10.0"; }
12+
] null;
13+
release."1.2.0".sha256 = "0sk01rvvk652d86aibc8rik2m8iz7jn6mw9hh6xkbxlsvh50719d";
14+
release."1.1.0".sha256 = "sha256-spno5ty4kU4WWiOfzoqbXF8lWlNSlySWcRReR3zE/4Q=";
15+
release."1.0.0".sha256 = "0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp";
16+
release."0.10.0".sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h";
17+
releaseRev = v: "v${v}";
18+
19+
nativeBuildInputs = [ which ];
20+
21+
propagatedBuildInputs = [ coq-elpi ];
22+
23+
mlPlugin = true;
24+
25+
buildPhase = "make build" + optionalString shim " -C shim";
26+
27+
installFlags = [ "DESTDIR=$(out)" "COQMF_COQLIB=lib/coq/${coq.coq-version}" ]
28+
++ optional shim "-C shim";
29+
30+
meta = {
31+
description = "High level commands to declare a hierarchy based on packed classes";
32+
maintainers = with maintainers; [ cohencyril siraben ];
33+
license = licenses.mit;
34+
};
35+
}

‎.nix/ocaml-overlays/elpi/default.nix‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
{ lib
2+
, buildDunePackage, camlp5
3+
, ocaml
4+
, menhir, menhirLib
5+
, atdgen
6+
, stdlib-shims
7+
, re, perl, ncurses
8+
, ppxlib, ppx_deriving
9+
, coqPackages
10+
, version ? if lib.versionAtLeast ocaml.version "4.08" then "1.17.0"
11+
else if lib.versionAtLeast ocaml.version "4.07" then "1.15.2" else "1.14.1"
12+
}:
13+
14+
let p5 = camlp5; in
15+
let camlp5 = p5.override { legacy = true; }; in
16+
17+
let fetched = coqPackages.metaFetch ({
18+
release."1.17.0".sha256 = "sha256-DTxE8CvYl0et20pxueydI+WzraI6UPHMNvxyp2gU/+w=";
19+
release."1.16.5".sha256 = "sha256-tKX5/cVPoBeHiUe+qn7c5FIRYCwY0AAukN7vSd/Nz9A=";
20+
release."1.15.2".sha256 = "sha256-XgopNP83POFbMNyl2D+gY1rmqGg03o++Ngv3zJfCn2s=";
21+
release."1.15.0".sha256 = "sha256:1ngdc41sgyzyz3i3lkzjhnj66gza5h912virkh077dyv17ysb6ar";
22+
release."1.14.1".sha256 = "sha256-BZPVL8ymjrE9kVGyf6bpc+GA2spS5JBpkUtZi04nPis=";
23+
release."1.13.7".sha256 = "10fnwz30bsvj7ii1vg4l1li5pd7n0qqmwj18snkdr5j9gk0apc1r";
24+
release."1.13.5".sha256 = "02a6r23mximrdvs6kgv6rp0r2dgk7zynbs99nn7lphw2c4189kka";
25+
release."1.13.1".sha256 = "12a9nbdvg9gybpw63lx3nw5wnxfznpraprb0wj3l68v1w43xq044";
26+
release."1.13.0".sha256 = "0dmzy058m1mkndv90byjaik6lzzfk3aaac7v84mpmkv6my23bygr";
27+
release."1.12.0".sha256 = "1agisdnaq9wrw3r73xz14yrq3wx742i6j8i5icjagqk0ypmly2is";
28+
release."1.11.4".sha256 = "1m0jk9swcs3jcrw5yyw5343v8mgax238cjb03s8gc4wipw1fn9f5";
29+
releaseRev = v: "v${v}";
30+
location = { domain = "github.com"; owner = "LPCIC"; repo = "elpi"; };
31+
}) version;
32+
in
33+
buildDunePackage rec {
34+
pname = "elpi";
35+
inherit (fetched) version src;
36+
37+
patches = lib.optional (version == "1.16.5")
38+
./atd_2_10.patch;
39+
40+
minimalOCamlVersion = "4.04";
41+
duneVersion = "3";
42+
43+
# atdgen is both a library and executable
44+
nativeBuildInputs = [ perl ]
45+
++ [ (if lib.versionAtLeast version "1.15" || version == "dev" then menhir else camlp5) ]
46+
++ lib.optional (lib.versionAtLeast version "1.16" || version == "dev") atdgen;
47+
buildInputs = [ ncurses ]
48+
++ lib.optional (lib.versionAtLeast version "1.16" || version == "dev") atdgen;
49+
50+
propagatedBuildInputs = [ re stdlib-shims ]
51+
++ [ menhirLib ]
52+
++ [ ppxlib ppx_deriving ]
53+
;
54+
55+
meta = with lib; {
56+
description = "Embeddable λProlog Interpreter";
57+
license = licenses.lgpl21Plus;
58+
maintainers = [ maintainers.vbgl ];
59+
homepage = "https://github.com/LPCIC/elpi";
60+
};
61+
62+
postPatch = ''
63+
substituteInPlace elpi_REPL.ml --replace "tput cols" "${ncurses}/bin/tput cols"
64+
'';
65+
}

‎Changelog.md‎

Lines changed: 21 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,21 @@
11
# Changelog
22

3-
## Unreleased - 09/11/2023
3+
## [2.0.0] - Unreleased
4+
5+
Requires Elpi 1.18.1 and Coq 8.18.
6+
7+
This major release accommodates for the separation of parsing from execution
8+
of Coq 8.18 enabling Coq-Elpi programs to be run efficiently (and correctly)
9+
under VSCoq 2.0.
10+
11+
### Documentation
12+
- New section about parsing/execution separation in the [Writing commands in Elpi](https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_command.html) tutorial
13+
14+
### Commands
15+
- New `Elpi *` commands understand the `#[phase]` attribute, see the doc in
16+
the [README](README.md#vernacular-commands) file, and the section
17+
about the [separation of parsing from execution](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
18+
- New `Elpi Export` understands an `As` clause to rename or alias a program when exported
419

520
### API
621
- Change `coq.elpi.add-predicate` now locality can be changed
@@ -13,6 +28,11 @@
1328
- New `coq.ltac.fresh-id` to generate fresh names in the proof context
1429
- New `@no-tc!` attribute supported by `coq.ltac.call-ltac1`
1530
- New `coq.TC.get-inst-prio` returns the `tc-priority` of an instance
31+
- New `synterp-action` datatype
32+
- New `coq.replay-all-missing-synterp-actions`
33+
- New `coq.replay-synterp-action`
34+
- New `coq.next-synterp-action`
35+
- New `coq.synterp-actions` (parsing phase only)
1636

1737
### Apps
1838
- New `tc` app providing an implementation of a type class solver written in elpi.

‎Makefile‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -91,13 +91,19 @@ doc: $(DOCDEP)
9191

9292
.PHONY: force build all test doc
9393

94-
Makefile.coq Makefile.coq.conf: src/coq_elpi_builtins_HOAS.ml src/coq_elpi_config.ml _CoqProject
94+
Makefile.coq Makefile.coq.conf: src/coq_elpi_builtins_HOAS.ml src/coq_elpi_builtins_arg_HOAS.ml src/coq_elpi_config.ml _CoqProject
9595
@$(COQBIN)/coq_makefile -f _CoqProject -o Makefile.coq
9696
@$(MAKE) --no-print-directory -f Makefile.coq .merlin
9797
Makefile.test.coq Makefile.test.coq.conf: _CoqProject.test
9898
@$(COQBIN)/coq_makefile -f _CoqProject.test -o Makefile.test.coq
9999
Makefile.examples.coq Makefile.examples.coq.conf: _CoqProject.examples
100100
@$(COQBIN)/coq_makefile -f _CoqProject.examples -o Makefile.examples.coq
101+
src/coq_elpi_builtins_arg_HOAS.ml: elpi/coq-arg-HOAS.elpi Makefile.coq.local
102+
echo "(* Automatically generated from $<, don't edit *)" > $@
103+
echo "(* Regenerate via 'make $@' *)" >> $@
104+
echo "let code = {|" >> $@
105+
cat $< >> $@
106+
echo "|}" >> $@
101107
src/coq_elpi_builtins_HOAS.ml: elpi/coq-HOAS.elpi Makefile.coq.local
102108
echo "(* Automatically generated from $<, don't edit *)" > $@
103109
echo "(* Regenerate via 'make $@' *)" >> $@

0 commit comments

Comments
 (0)