Skip to content

Commit e3b9e18

Browse files
authored
Update makefile and CI for Coq 8.20 (#803)
* Update makefile and CI for Coq 8.20 * Update CI; update InteractionTrees submodule * Bring submodules up to date
1 parent 426c7f4 commit e3b9e18

File tree

3 files changed

+11
-12
lines changed

3 files changed

+11
-12
lines changed

.github/workflows/coq-action.yml

+4-10
Original file line numberDiff line numberDiff line change
@@ -21,19 +21,16 @@ jobs:
2121
# except for the "make_target" field and make_target related excludes
2222
coq_version:
2323
# See https://github.com/coq-community/docker-coq/wiki for supported images
24-
# - '8.17'
25-
- '8.18'
2624
- '8.19'
25+
- '8.20'
2726
- 'dev'
2827
bit_size:
2928
- 32
3029
- 64
3130
make_target:
3231
- vst
3332
exclude:
34-
# - coq_version: 8.17
35-
# bit_size: 32
36-
- coq_version: 8.18
33+
- coq_version: 8.19
3734
bit_size: 32
3835
- coq_version: dev
3936
bit_size: 32
@@ -91,9 +88,8 @@ jobs:
9188
fail-fast: false
9289
matrix:
9390
coq_version:
94-
# - '8.17'
95-
- '8.18'
9691
- '8.19'
92+
- '8.20'
9793
- 'dev'
9894
make_target:
9995
- assumptions.txt
@@ -106,9 +102,7 @@ jobs:
106102
- 32
107103
- 64
108104
exclude:
109-
# - coq_version: 8.17
110-
# bit_size: 32
111-
- coq_version: 8.18
105+
- coq_version: 8.19
112106
bit_size: 32
113107
- coq_version: dev
114108
bit_size: 32

Makefile

+6-1
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ COQLIB=$(shell $(COQC) -where | tr -d '\r' | tr '\\' '/')
2121

2222
# Check Coq version
2323

24-
COQVERSION= 8.17.0 or-else 8.17.1 or-else 8.18.0 or-else 8.19.1
24+
COQVERSION= 8.19.1 or-else 8.19.2 or-else 8.20.0
2525

2626
COQV=$(shell $(COQC) -v)
2727
ifneq ($(IGNORECOQVERSION),true)
@@ -334,6 +334,11 @@ DEPFLAGS:=$(COQFLAGS)
334334

335335
COQFLAGS+=$(COQEXTRAFLAGS)
336336

337+
# The following extra flags can probably be removed with Coq 8.21,
338+
# after Coq pulls https://github.com/coq/coq/pull/19653
339+
# and/or https://github.com/coq/coq/pull/19981 are merged.
340+
COQFLAGS+= -w "-notation-incompatible-prefix,-automatic-prop-lowering"
341+
337342
PROFILING?=
338343

339344
ifneq (,$(PROFILING))

0 commit comments

Comments
 (0)