diff options
author | Jason Gross <jgross@mit.edu> | 2019-04-11 13:10:30 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2019-04-11 13:10:30 -0400 |
commit | f626f41c8c5df7eb4131d16f8cc6e05140fd509c (patch) | |
tree | 933316180ed220f1e06e1defdfdad5ba253b8476 /Makefile | |
parent | 60520cd8d08f63337225c0a2938827e00a2c48a3 (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
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -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 \ |