diff options
| author |  Benjamin Barenblat <bbaren@google.com> | 2019-04-26 16:41:41 -0400 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@google.com> | 2019-04-26 16:41:41 -0400 |
| commit | 4483d41d6a510e01041f05546643934c9d2a887b (patch) | |
| tree | 162e1630e3e4dc10d77a6587fa95d0e30f9cae25 | |
| parent | efdf63a5dd1dfbd4bafc121224c64822530185fe (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-- | .gitmodules | 3 | ||||
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | _CoqProject | 17 | ||||
| m--------- | bbv | 0 | ||||
| -rwxr-xr-x | etc/ci/travis.sh | 2 |
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 @@ -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 |