aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorBenjamin Barenblat <bbaren@google.com>2019-04-26 16:41:41 -0400
committerBenjamin Barenblat <bbaren@google.com>2019-04-26 16:41:41 -0400
commit4483d41d6a510e01041f05546643934c9d2a887b (patch)
tree162e1630e3e4dc10d77a6587fa95d0e30f9cae25
parentefdf63a5dd1dfbd4bafc121224c64822530185fe (diff)
Remove bbv dependency
No code in fiat-crypto depends on bbv anymore, so delete it. Closes https://github.com/mit-plv/fiat-crypto/issues/481.
-rw-r--r--.gitmodules3
-rw-r--r--Makefile4
-rw-r--r--_CoqProject17
m---------bbv0
-rwxr-xr-xetc/ci/travis.sh2
5 files changed, 3 insertions, 23 deletions
diff --git a/.gitmodules b/.gitmodules
index 0a919ab11..ff4ce384d 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,9 +1,6 @@
[submodule "etc/coq-scripts"]
path = etc/coq-scripts
url = https://github.com/JasonGross/coq-scripts.git
-[submodule "bbv"]
- path = bbv
- url = ../../mit-plv/bbv.git
[submodule "coqprime"]
path = coqprime
url = https://github.com/thery/coqprime
diff --git a/Makefile b/Makefile
index fbd3bed0d..cd07dad19 100644
--- a/Makefile
+++ b/Makefile
@@ -37,7 +37,7 @@ include etc/coq-scripts/Makefile.vo_closure
SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g' | uniq
update-_CoqProject::
$(SHOW)'ECHO > _CoqProject'
- $(HIDE)(echo '-R $(SRC_DIR) $(MOD_NAME)'; echo '-R bbv/theories bbv'; ((git ls-files 'src/*.v'; (git submodule foreach 'git ls-files "*.v" 2>/dev/null | sed "s|^|$$path/|"' | grep 'bbv/')) | $(GREP_EXCLUDE_SPECIAL_VOFILES) | $(SORT_COQPROJECT))) > _CoqProject
+ $(HIDE)(echo '-R $(SRC_DIR) $(MOD_NAME)'; (git ls-files 'src/*.v' | $(GREP_EXCLUDE_SPECIAL_VOFILES) | $(SORT_COQPROJECT))) > _CoqProject
# coq .vo files that are not compiled using coq_makefile
SPECIAL_VOFILES := \
@@ -59,7 +59,7 @@ NOBIGMEM_UNMADE_VOFILES := \
src/Curves/Weierstrass/Projective.vo
REGULAR_VOFILES := $(filter-out $(SPECIAL_VOFILES),$(VOFILES))
PRE_STANDALONE_PRE_VOFILES := $(filter src/Standalone%.vo,$(REGULAR_VOFILES))
-UTIL_PRE_VOFILES := $(filter bbv/%.vo src/Algebra/%.vo src/Tactics/%.vo src/Util/%.vo,$(REGULAR_VOFILES))
+UTIL_PRE_VOFILES := $(filter src/Algebra/%.vo src/Tactics/%.vo src/Util/%.vo,$(REGULAR_VOFILES))
SOME_EARLY_VOFILES := \
src/Arithmetic/Core.vo \
src/Rewriter.vo
diff --git a/_CoqProject b/_CoqProject
index 6e7e43e64..db7e7ba8e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,21 +1,4 @@
-R src Crypto
--R bbv/theories bbv
-bbv/theories/BinNotation.v
-bbv/theories/BinNotationZ.v
-bbv/theories/DepEq.v
-bbv/theories/DepEqNat.v
-bbv/theories/HexNotation.v
-bbv/theories/HexNotationWord.v
-bbv/theories/HexNotationZ.v
-bbv/theories/NLib.v
-bbv/theories/N_Z_nat_conversions.v
-bbv/theories/NatLib.v
-bbv/theories/Nomega.v
-bbv/theories/ReservedNotations.v
-bbv/theories/Word.v
-bbv/theories/WordScope.v
-bbv/theories/ZHints.v
-bbv/theories/ZLib.v
src/AbstractInterpretation.v
src/AbstractInterpretationProofs.v
src/AbstractInterpretationWf.v
diff --git a/bbv b/bbv
deleted file mode 160000
-Subproject 143c47ba1267a0a700c17bdf5bbded9b6e4bfbb
diff --git a/etc/ci/travis.sh b/etc/ci/travis.sh
index 8942d1db7..f16f0e555 100755
--- a/etc/ci/travis.sh
+++ b/etc/ci/travis.sh
@@ -13,7 +13,7 @@ rm -f finished.ok
(make "$@" -j2 TIMED=1 2>&1 && touch finished.ok) | tee -a time-of-build.log
python "./etc/coq-scripts/timing/make-one-time-file.py" "time-of-build.log" "time-of-build-pretty.log" || exit $?
rm -f "${CUR_ARCHIVE}"
-tar -czf "${CUR_ARCHIVE}" time-of-build.log src bbv coqprime || exit $?
+tar -czf "${CUR_ARCHIVE}" time-of-build.log src coqprime || exit $?
git update-index --assume-unchanged _CoqProject
git status