Skip to content

Commit 6488498

Browse files
womeierwomeier
committed
Rocq 9.0 update
1 parent 0681daf commit 6488498

23 files changed

+116
-73
lines changed

‎.github/workflows/docker-action.yml‎

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -18,14 +18,10 @@ jobs:
1818
matrix:
1919
image:
2020
- 'rocq/rocq-prover:dev'
21-
- 'coqorg/coq:8.20'
22-
- 'coqorg/coq:8.19'
23-
- 'coqorg/coq:8.18'
24-
- 'coqorg/coq:8.17'
25-
- 'coqorg/coq:8.16'
21+
- 'rocq/rocq-prover:9.0'
2622
fail-fast: false
2723
steps:
28-
- uses: actions/checkout@v3
24+
- uses: actions/checkout@v4
2925
- uses: coq-community/docker-coq-action@v1
3026
with:
3127
opam_file: 'coq-parseque.opam'

‎.github/workflows/nix-action-8.20.yml‎ renamed to ‎.github/workflows/nix-action-9.0.yml‎

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ jobs:
3939
- id: stepGetDerivation
4040
name: Getting derivation for current job (coq)
4141
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
42-
\"8.20\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch fail;
42+
\"9.0\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch fail;
4343
true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
4444
failed\"; exit 1; fi\n"
4545
- id: stepCheck
@@ -51,7 +51,7 @@ jobs:
5151
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
5252
- if: steps.stepCheck.outputs.status != 'fetched'
5353
name: Building/fetching current CI target
54-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
54+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" --argstr
5555
job "coq"
5656
parseque:
5757
needs:
@@ -94,7 +94,7 @@ jobs:
9494
- id: stepGetDerivation
9595
name: Getting derivation for current job (parseque)
9696
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
97-
\"8.20\" --argstr job \"parseque\" \\\n --dry-run 2> err > out || (touch
97+
\"9.0\" --argstr job \"parseque\" \\\n --dry-run 2> err > out || (touch
9898
fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
9999
failed\"; exit 1; fi\n"
100100
- id: stepCheck
@@ -106,20 +106,24 @@ jobs:
106106
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
107107
- if: steps.stepCheck.outputs.status != 'fetched'
108108
name: 'Building/fetching previous CI target: coq'
109-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
109+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" --argstr
110110
job "coq"
111+
- if: steps.stepCheck.outputs.status != 'fetched'
112+
name: 'Building/fetching previous CI target: stdlib'
113+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" --argstr
114+
job "stdlib"
111115
- if: steps.stepCheck.outputs.status != 'fetched'
112116
name: Building/fetching current CI target
113-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
117+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" --argstr
114118
job "parseque"
115-
name: Nix CI for bundle 8.20
119+
name: Nix CI for bundle 9.0
116120
on:
117121
pull_request:
118122
paths:
119-
- .github/workflows/nix-action-8.20.yml
123+
- .github/workflows/nix-action-9.0.yml
120124
pull_request_target:
121125
paths-ignore:
122-
- .github/workflows/nix-action-8.20.yml
126+
- .github/workflows/nix-action-9.0.yml
123127
types:
124128
- opened
125129
- synchronize

‎.gitignore‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,8 @@ nia.cache
3131
nlia.cache
3232
nra.cache
3333
.Makefile.d
34-
.Makefile.coq.d
35-
Makefile.coq
36-
Makefile.coq.conf
34+
.Makefile.rocq.d
35+
Makefile.rocq
36+
Makefile.rocq.conf
3737

3838
result

‎.nix/config.nix‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,9 @@
66

77
attribute = "parseque";
88

9-
default-bundle = "8.20";
10-
bundles."8.20" = {
11-
coqPackages.coq.override.version = "8.20";
9+
default-bundle = "9.0";
10+
bundles."9.0" = {
11+
rocqPackages.rocq-core.override.version = "9.0";
1212
};
1313

1414
## Cachix caches to use in CI

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
"944779fa54c48b734298bf78bd71a22eee0abe96"
1+
"ca2edb8c74419fdc0a3add0bbd26e4752fe1a457"

‎.nix/rocq-overlays/parseque/default.nix‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
{
2+
lib,
3+
mkRocqDerivation,
4+
which,
5+
stdlib,
6+
rocq-core,
7+
version ? null,
8+
}:
9+
10+
with lib;
11+
mkRocqDerivation {
12+
pname = "parseque";
13+
repo = "parseque";
14+
owner = "rocq-community";
15+
16+
inherit version;
17+
defaultVersion =
18+
with versions;
19+
switch
20+
[ rocq-core.rocq-version ]
21+
[
22+
{
23+
cases = [ (range "8.16" "8.20") ];
24+
out = "0.2.2";
25+
}
26+
{
27+
cases = [ (range "9.0" "9.0") ];
28+
out = "0.2.3";
29+
}
30+
]
31+
null;
32+
33+
release."0.2.2".sha256 = "sha256-O50Rs7Yf1H4wgwb7ltRxW+7IF0b04zpfs+mR83rxT+E=";
34+
35+
propagatedBuildInputs = [ stdlib ];
36+
37+
releaseRev = v: "v${v}";
38+
39+
meta = {
40+
description = "Total parser combinators in Rocq";
41+
maintainers = with maintainers; [ womeier ];
42+
license = licenses.mit;
43+
};
44+
}

‎Makefile‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,16 @@
1-
all: Makefile.coq
2-
@+$(MAKE) -f Makefile.coq all
1+
all: Makefile.rocq
2+
@+$(MAKE) -f Makefile.rocq all
33

4-
clean: Makefile.coq
5-
@+$(MAKE) -f Makefile.coq cleanall
6-
@rm -f Makefile.coq Makefile.coq.conf
4+
clean: Makefile.rocq
5+
@+$(MAKE) -f Makefile.rocq cleanall
6+
@rm -f Makefile.rocq Makefile.rocq.conf
77

8-
Makefile.coq: _CoqProject
9-
$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
8+
Makefile.rocq: _RocqProject
9+
$(COQBIN)rocq makefile -f _RocqProject -o Makefile.rocq
1010

11-
force _CoqProject Makefile: ;
11+
force _RocqProject Makefile: ;
1212

13-
%: Makefile.coq force
14-
@+$(MAKE) -f Makefile.coq $@
13+
%: Makefile.rocq force
14+
@+$(MAKE) -f Makefile.rocq $@
1515

1616
.PHONY: all clean force

‎README.md‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
99
[![Code of Conduct][conduct-shield]][conduct-link]
1010
[![Zulip][zulip-shield]][zulip-link]
1111

12-
[docker-action-shield]: https://github.com/coq-community/parseque/actions/workflows/docker-action.yml/badge.svg?branch=master
13-
[docker-action-link]: https://github.com/coq-community/parseque/actions/workflows/docker-action.yml
12+
[docker-action-shield]: https://github.com/rocq-community/parseque/actions/workflows/docker-action.yml/badge.svg?branch=master
13+
[docker-action-link]: https://github.com/rocq-community/parseque/actions/workflows/docker-action.yml
1414

1515
[contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
1616
[contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -23,18 +23,18 @@ Follow the instructions on https://github.com/coq-community/templates to regener
2323

2424

2525

26-
Port of the agdarsec total parser combinator library to Coq.
26+
Port of the agdarsec total parser combinator library to Rocq/Coq.
2727

2828
## Meta
2929

3030
- Author(s):
3131
- G. Allais (initial)
32-
- Coq-community maintainer(s):
32+
- Rocq-community maintainer(s):
3333
- Wolfgang Meier ([**@womeier**](https://github.com/womeier))
3434
- License: [MIT License](LICENSE)
35-
- Compatible Coq versions: 8.16 or later
35+
- Compatible Rocq/Coq versions: 9.0 or later (for older versions see opam/nix)
3636
- Additional dependencies: none
37-
- Coq namespace: `parseque`
37+
- Rocq/Coq namespace: `parseque`
3838
- Related publication(s):
3939
- [agdarsec - Total Parser Combinators](https://gallais.github.io/pdf/agdarsec18.pdf)
4040

@@ -51,7 +51,7 @@ opam install coq-parseque
5151
To instead build and install manually, do:
5252

5353
``` shell
54-
git clone https://github.com/coq-community/parseque.git
54+
git clone https://github.com/rocq-community/parseque.git
5555
cd parseque
5656
make # or make -j <number-of-cores-on-your-machine>
5757
make install
@@ -60,7 +60,7 @@ make install
6060

6161
## Documentation
6262

63-
This Coq library is a port of the [agdarsec](https://github.com/gallais/agdarsec)
63+
This Rocq/Coq library is a port of the [agdarsec](https://github.com/gallais/agdarsec)
6464
library for Agda. The core design of agdarsec is described in
6565
[this paper](https://gallais.github.io/pdf/agdarsec18.pdf), while
6666
[this blog post](https://gallais.github.io/blog/instrumenting-agdarsec)

‎_CoqProject‎ renamed to ‎_RocqProject‎

File renamed without changes.

‎coq-parseque.opam‎

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -5,19 +5,20 @@ opam-version: "2.0"
55
maintainer: "[email protected]"
66
version: "dev"
77

8-
homepage: "https://github.com/coq-community/parseque"
9-
dev-repo: "git+https://github.com/coq-community/parseque.git"
10-
bug-reports: "https://github.com/coq-community/parseque/issues"
8+
homepage: "https://github.com/rocq-community/parseque"
9+
dev-repo: "git+https://github.com/rocq-community/parseque.git"
10+
bug-reports: "https://github.com/rocq-community/parseque/issues"
1111
license: "MIT"
1212

13-
synopsis: "Total parser combinators in Coq"
13+
synopsis: "Total parser combinators in Rocq/Coq"
1414
description: """
15-
Port of the agdarsec total parser combinator library to Coq."""
15+
Port of the agdarsec total parser combinator library to Rocq/Coq."""
1616

1717
build: [make "-j%{jobs}%"]
1818
install: [make "install"]
1919
depends: [
20-
"coq" {>= "8.16"}
20+
"rocq-core" {>= "9.0"}
21+
"rocq-stdlib" {>= "9.0"}
2122
]
2223

2324
tags: [

0 commit comments

Comments
 (0)