From f433b45e308b2738132061dca4ef5569a595ab6d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 11 Mar 2019 17:09:02 -0400 Subject: [PATCH 1/5] Fix incorrect change introduced by 168b8004e1e390d1a1260355c19b33dc6f5d9ef9 `_CoqProject.in` should be using `ML_COMPATIBILITY_FILES_PATTERN`, not `ML_COMPATIBILITY_FILES`, and the compatibility script uses `EXTRA_PIPE_SED_FOR_COQPROJECT` to update it. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 8a6cd1f98..ae2471506 100644 --- a/Makefile +++ b/Makefile @@ -314,7 +314,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 ...)) From d9511b0560c41c3d796ec0c275b4d85adac7db33 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 11 Mar 2019 17:12:10 -0400 Subject: [PATCH 2/5] Bump submodule Fix issue from 842c4c0e0b769d4cc0b5b27925ccefece61558eb --- etc/coq-scripts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/etc/coq-scripts b/etc/coq-scripts index 7bd683da1..2187c33d3 160000 --- a/etc/coq-scripts +++ b/etc/coq-scripts @@ -1 +1 @@ -Subproject commit 7bd683da1fac8b5eb42de1e44a3274db4fd0ce41 +Subproject commit 2187c33d3d08962d7ad11b9a1d5d1ea5f45d02ed From d865e59449d09527a4c471e8e64062f58d64f404 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 11 Mar 2019 17:23:14 -0400 Subject: [PATCH 3/5] Hopefully prevent future issues of silent failure --- Makefile | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Makefile b/Makefile index ae2471506..e47d35a52 100644 --- a/Makefile +++ b/Makefile @@ -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 From 2fbe30893793d338cd72d7b8761e3771e6806f8c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 11 Mar 2019 17:35:01 -0400 Subject: [PATCH 4/5] Bump submodule --- etc/coq-scripts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/etc/coq-scripts b/etc/coq-scripts index 2187c33d3..9dc70c73b 160000 --- a/etc/coq-scripts +++ b/etc/coq-scripts @@ -1 +1 @@ -Subproject commit 2187c33d3d08962d7ad11b9a1d5d1ea5f45d02ed +Subproject commit 9dc70c73be0d6a35c09136d65b5f21b75b77d273 From 100632b6a77a14993cae48c794c25ba029ba02f8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 11 Mar 2019 22:22:32 -0400 Subject: [PATCH 5/5] Fix _CoqProject.in We now correctly work on master again --- _CoqProject.in | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/_CoqProject.in b/_CoqProject.in index 021f42a5a..88f7d1d52 100644 --- a/_CoqProject.in +++ b/_CoqProject.in @@ -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