aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile25
1 files changed, 18 insertions, 7 deletions
diff --git a/Makefile b/Makefile
index 1dd4efca2e..a6a73d2499 100644
--- a/Makefile
+++ b/Makefile
@@ -52,7 +52,10 @@ FIND_VCS_CLAUSE:='(' \
-name '.bzr' -o \
-name 'debian' -o \
-name "$${GIT_DIR}" -o \
- -name '_build' \
+ -name '_build' -o \
+ -name '_build_ci' -o \
+ -name 'coq-makefile' -o \
+ -name '.opamcache' \
')' -prune -o
define find
@@ -86,8 +89,7 @@ EXISTINGMLI := $(call find, '*.mli')
GENML4FILES:= $(ML4FILES:.ml4=.ml)
export GENMLFILES:=$(LEXFILES:.mll=.ml) tools/tolink.ml kernel/copcodes.ml
export GENHFILES:=kernel/byterun/coq_jumptbl.h
-export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v
-export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES)
+export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
# NB: all files in $(GENFILES) can be created initially, while
# .ml files in $(GENML4FILES) might need some intermediate building.
@@ -113,16 +115,19 @@ NOARG: world
.PHONY: NOARG help noconfig submake
help:
- @echo "Please use either"
+ @echo "Please use either:"
@echo " ./configure"
@echo " make world"
@echo " make install"
@echo " make clean"
@echo "or make archclean"
- @echo
@echo "For make to be verbose, add VERBOSE=1"
+ @echo "If you want camlp5 to generate human-readable files, add READABLE_ML4=1"
@echo
- @echo "If you want camlp{4,5} to generate human-readable files, add READABLE_ML4=1"
+ @echo "Bytecode compilation is now a separate target:"
+ @echo " make byte"
+ @echo " make install-byte"
+ @echo "Please do not mix bytecode and native targets in the same make -j"
UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?')
ifdef UNSAVED_FILES
@@ -185,6 +190,7 @@ indepclean:
rm -f test-suite/check.log
rm -f glob.dump
rm -f config/revision.ml revision
+ rm -f plugins/micromega/.micromega.ml.generated
$(MAKE) -C test-suite clean
docclean:
@@ -231,7 +237,7 @@ cacheclean:
find theories plugins test-suite -name '.*.aux' -delete
cleanconfig:
- rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-v7 config/Info-*.plist
+ rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp4.dbg config/Info-*.plist
distclean: clean cleanconfig cacheclean
@@ -246,6 +252,11 @@ devdocclean:
rm -f $(OCAMLDOCDIR)/html/*.html
###########################################################################
+# Continuous Intregration Tests
+###########################################################################
+include Makefile.ci
+
+###########################################################################
# Emacs tags
###########################################################################