aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJason Gross <jgross@mit.edu>2019-04-11 13:10:30 -0400
committerJason Gross <jgross@mit.edu>2019-04-11 13:10:30 -0400
commitf626f41c8c5df7eb4131d16f8cc6e05140fd509c (patch)
tree933316180ed220f1e06e1defdfdad5ba253b8476
parent60520cd8d08f63337225c0a2938827e00a2c48a3 (diff)
Don't include extraction .vo files in the all target
We run coqc on these files via the c-files target, which is also included in the all target
-rw-r--r--Makefile3
-rw-r--r--_CoqProject8
2 files changed, 3 insertions, 8 deletions
diff --git a/Makefile b/Makefile
index 17d57cb07..fbd3bed0d 100644
--- a/Makefile
+++ b/Makefile
@@ -37,12 +37,13 @@ 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/')) | $(SORT_COQPROJECT))) > _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
# coq .vo files that are not compiled using coq_makefile
SPECIAL_VOFILES := \
src/ExtractionOCaml/%.vo \
src/ExtractionHaskell/%.vo
+GREP_EXCLUDE_SPECIAL_VOFILES := grep -v '^src/Extraction\(OCaml\|Haskell\)/'
# add files to this list to prevent them from being built as final
# targets by the "lite" target
LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \
diff --git a/_CoqProject b/_CoqProject
index 4d4b652ff..8859f08ed 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -35,9 +35,9 @@ src/MiscCompilerPasses.v
src/MiscCompilerPassesProofs.v
src/PreLanguage.v
src/Rewriter.v
-src/RewriterInterpProofs1.v
src/RewriterAll.v
src/RewriterAllTactics.v
+src/RewriterInterpProofs1.v
src/RewriterRules.v
src/RewriterRulesProofs.v
src/RewriterWf1.v
@@ -91,12 +91,6 @@ src/Curves/Weierstrass/Affine.v
src/Curves/Weierstrass/AffineProofs.v
src/Curves/Weierstrass/Jacobian.v
src/Curves/Weierstrass/Projective.v
-src/ExtractionHaskell/saturated_solinas.v
-src/ExtractionHaskell/unsaturated_solinas.v
-src/ExtractionHaskell/word_by_word_montgomery.v
-src/ExtractionOCaml/saturated_solinas.v
-src/ExtractionOCaml/unsaturated_solinas.v
-src/ExtractionOCaml/word_by_word_montgomery.v
src/Fancy/Barrett256.v
src/Fancy/Compiler.v
src/Fancy/Montgomery256.v