Skip to content

Commit

Permalink
Update makefile and CI for Coq 8.20 (#803)
Browse files Browse the repository at this point in the history
* Update makefile and CI for Coq 8.20

* Update CI; update InteractionTrees submodule

* Bring submodules up to date
  • Loading branch information
andrew-appel authored Jan 7, 2025
1 parent 426c7f4 commit e3b9e18
Show file tree
Hide file tree
Showing 3 changed files with 11 additions and 12 deletions.
14 changes: 4 additions & 10 deletions .github/workflows/coq-action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -21,19 +21,16 @@ jobs:
# except for the "make_target" field and make_target related excludes
coq_version:
# See https://github.com/coq-community/docker-coq/wiki for supported images
# - '8.17'
- '8.18'
- '8.19'
- '8.20'
- 'dev'
bit_size:
- 32
- 64
make_target:
- vst
exclude:
# - coq_version: 8.17
# bit_size: 32
- coq_version: 8.18
- coq_version: 8.19
bit_size: 32
- coq_version: dev
bit_size: 32
Expand Down Expand Up @@ -91,9 +88,8 @@ jobs:
fail-fast: false
matrix:
coq_version:
# - '8.17'
- '8.18'
- '8.19'
- '8.20'
- 'dev'
make_target:
- assumptions.txt
Expand All @@ -106,9 +102,7 @@ jobs:
- 32
- 64
exclude:
# - coq_version: 8.17
# bit_size: 32
- coq_version: 8.18
- coq_version: 8.19
bit_size: 32
- coq_version: dev
bit_size: 32
Expand Down
7 changes: 6 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ COQLIB=$(shell $(COQC) -where | tr -d '\r' | tr '\\' '/')

# Check Coq version

COQVERSION= 8.17.0 or-else 8.17.1 or-else 8.18.0 or-else 8.19.1
COQVERSION= 8.19.1 or-else 8.19.2 or-else 8.20.0

COQV=$(shell $(COQC) -v)
ifneq ($(IGNORECOQVERSION),true)
Expand Down Expand Up @@ -334,6 +334,11 @@ DEPFLAGS:=$(COQFLAGS)

COQFLAGS+=$(COQEXTRAFLAGS)

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

PROFILING?=

ifneq (,$(PROFILING))
Expand Down
2 changes: 1 addition & 1 deletion fcf

0 comments on commit e3b9e18

Please sign in to comment.