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

Prevent future bugs that re-introduce silent failure in Coq's CI #2

Open
wants to merge 5 commits into
base: narcissus-release
Choose a base branch
from
Open

Prevent future bugs that re-introduce silent failure in Coq's CI #2

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
f433b45
Fix incorrect change introduced by 168b8004e1e390d1a1260355c19b33dc6f…
JasonGross Mar 11, 2019
d9511b0
Bump submodule
JasonGross Mar 11, 2019
d865e59
Hopefully prevent future issues of silent failure
JasonGross Mar 11, 2019
2fbe308
Bump submodule
JasonGross Mar 11, 2019
100632b
Fix _CoqProject.in
JasonGross Mar 12, 2019
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
7 changes: 6 additions & 1 deletion Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,6 +114,11 @@ ML_COMPATIBILITY_FILES_PATTERN := src/Common/Tactics/hint_db_extra_tactics.ml sr

ML_COMPATIBILITY_FILES := $(subst @ML4_OR_MLG@,$(ML4_OR_MLG),$(ML_COMPATIBILITY_FILES_PATTERN))

MAKEFILE_COQ_COMMON_CONTENTS := $(shell grep -- '-include Makefile.coq' etc/coq-scripts/Makefile.coq.common)
ifneq ($(MAKEFILE_COQ_COMMON_CONTENTS),)
$(error "Your coq-scripts submodule is too old! Please update it. Hopefully this error message will prevent future silent failures on Coq's CI as fixed twice now, e.g., by 75a2142c94a90a45287389d26a26ea5322e84f7e")
endif

include etc/coq-scripts/Makefile.coq.common

include etc/coq-scripts/compatibility/Makefile.coq.compat_84_85
Expand Down Expand Up @@ -314,7 +319,7 @@ install-fiat install-fiat-core install-querystructures install-parsers install-p
# This target is used to update the _CoqProject.in file.
# Use -R, not -I for Bedrock, as it is Coq input, not OCaml input.
$(UPDATE_COQPROJECT_TARGET):
(echo '-R src Fiat'; echo '-R Bedrock Bedrock'; echo '-I src/Common/Tactics'; git ls-files "*.v" | grep -v '^$(COMPATIBILITY_FILE)$$' | $(SORT_COQPROJECT); (echo '$(COMPATIBILITY_FILE)'; git ls-files "*.{ml4,mlg}" | $(SORT_COQPROJECT); (echo '$(ML_COMPATIBILITY_FILES)' | tr ' ' '\n'; echo 'src/Common/Tactics/transparent_abstract_plugin.mllib'; echo 'src/Common/Tactics/hint_db_extra_plugin.mllib') | $(SORT_COQPROJECT))) > _CoqProject.in
(echo '-R src Fiat'; echo '-R Bedrock Bedrock'; echo '-I src/Common/Tactics'; git ls-files "*.v" | grep -v '^$(COMPATIBILITY_FILE)$$' | $(SORT_COQPROJECT); (echo '$(COMPATIBILITY_FILE)'; git ls-files "*.{ml4,mlg}" | $(SORT_COQPROJECT); (echo '$(ML_COMPATIBILITY_FILES_PATTERN)' | tr ' ' '\n'; echo 'src/Common/Tactics/transparent_abstract_plugin.mllib'; echo 'src/Common/Tactics/hint_db_extra_plugin.mllib') | $(SORT_COQPROJECT))) > _CoqProject.in

ifeq ($(IS_FAST),0)
# see http://stackoverflow.com/a/9691619/377022 for why we need $(eval $(call ...))
Expand Down
4 changes: 2 additions & 2 deletions _CoqProject.in
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -312,9 +312,9 @@ src/QueryStructure/Specification/SearchTerms/InRange.v
src/QueryStructure/Specification/SearchTerms/ListInclusion.v
src/QueryStructure/Specification/SearchTerms/ListPrefix.v
src/Common/Coq__8_4__8_5__Compat.v
src/Common/Tactics/hint_db_extra_plugin.ml4
src/Common/Tactics/hint_db_extra_plugin.@ML4_OR_MLG@
src/Common/Tactics/hint_db_extra_plugin.mllib
src/Common/Tactics/hint_db_extra_tactics.ml
src/Common/Tactics/transparent_abstract_plugin.ml4
src/Common/Tactics/transparent_abstract_plugin.@ML4_OR_MLG@
src/Common/Tactics/transparent_abstract_plugin.mllib
src/Common/Tactics/transparent_abstract_tactics.ml
2 changes: 1 addition & 1 deletion etc/coq-scripts
Open in desktop
Submodule coq-scripts updated 23 files
+23 −18 Makefile.coq.common
+27 −0 compatibility/Coq__8_10__Compat.v
+1 −0 compatibility/Coq__8_10__Compat.v.in
+4 −4 compatibility/Coq__8_4__Compat.v
+4 −4 compatibility/Coq__8_5__Compat.v
+4 −4 compatibility/Coq__8_5beta1__Compat.v
+4 −4 compatibility/Coq__8_5beta2__Compat.v
+4 −4 compatibility/Coq__8_5beta3__Compat.v
+4 −4 compatibility/Coq__8_5pl1__Compat.v
+4 −4 compatibility/Coq__8_5pl2__Compat.v
+4 −4 compatibility/Coq__8_5rc1__Compat.v
+4 −4 compatibility/Coq__8_6__Compat.v
+4 −4 compatibility/Coq__8_6beta1__Compat.v
+4 −4 compatibility/Coq__8_7__Compat.v
+4 −4 compatibility/Coq__8_8__Compat.v
+27 −0 compatibility/Coq__8_9__Compat.v
+1 −0 compatibility/Coq__8_9__Compat.v.in
+6 −4 compatibility/Coq__master__Compat.v
+4 −4 compatibility/Coq__trunk__Compat.v
+14 −3 compatibility/Makefile.coq.compat_84_85-early
+1 −0 compatibility/fragments/Grab88.v
+4 −4 compatibility/fragments/VectorListNotations.v
+6 −4 compatibility/generate-compat-files.sh