diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index acdb03da7eb0e..652c98417abdd 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -55,6 +55,20 @@ after_script: # TODO figure out how to build doc for installed Coq .build-template: &build-template + stage: build + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build + expire_in: 1 week + script: + - set -e + - echo 'start:coq.build' + - make world + - echo 'end:coq:build' + - set +e + +.build-make-template: &build-make-template stage: build artifacts: name: "$CI_JOB_NAME" @@ -68,76 +82,44 @@ after_script: - set -e - echo 'start:coq.clean' - - make clean # ensure that `make clean` works on a fresh clone + - make -f Makefile.make clean # ensure that `make clean` works on a fresh clone - echo 'end:coq.clean' - echo 'start:coq.config' - - ./configure -warn-error yes -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE" + - ./configure -warn-error yes -prefix "$(pwd)/_install_ci" - echo 'end:coq.config' - echo 'start:coq.build' - - make -j "$NJOBS" byte - - make -j "$NJOBS" world $EXTRA_TARGET - - make test-suite/misc/universes/all_stdlib.v + - make -f Makefile.make -j "$NJOBS" byte + - make -f Makefile.make -j "$NJOBS" world + - make -f Makefile.make test-suite/misc/universes/all_stdlib.v - echo 'end:coq:build' - echo 'start:coq.install' - - make install - - make install-byte + - make -f Makefile.make install + - make -f Makefile.make install-byte - cp bin/fake_ide _install_ci/bin/ - echo 'end:coq.install' - set +e -.dune-template: &dune-template - dependencies: [] - stage: build - artifacts: - name: "$CI_JOB_NAME" - paths: - - _build/ - expire_in: 1 week - script: - - set -e - - make -f Makefile.dune "$DUNE_TARGET" - - set +e - # every non build job must set dependencies otherwise all build # artifacts are used together and we may get some random Coq. To that # purpose, we add a spurious dependency `not-a-real-job` that must be # overridden otherwise the CI will fail. -.doc-template: &doc-template - stage: test - dependencies: - - not-a-real-job - script: - - SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/" COQBOOT=no' - - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= refman - - make install-doc-sphinx - artifacts: - name: "$CI_JOB_NAME" - paths: - - _install_ci/share/doc/coq/ - # set dependencies when using .test-suite-template: &test-suite-template stage: test dependencies: - not-a-real-job script: - - cd test-suite - - make clean - # careful with the ending / - - BIN=$(readlink -f ../_install_ci/bin)/ - - LIB=$(readlink -f ../_install_ci/lib/coq)/ - - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH" - - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" all + - make test-suite artifacts: name: "$CI_JOB_NAME.logs" when: on_failure paths: - - test-suite/logs + - _build/default/test-suite/logs # set dependencies when using .validate-template: &validate-template @@ -145,7 +127,7 @@ after_script: dependencies: - not-a-real-job script: - - cd _install_ci + - cd _build/install/default - find lib/coq/ -name '*.vo' -print0 > vofiles - for regexp in 's/.vo//' 's:lib/coq/plugins:Coq:' 's:lib/coq/theories:Coq:' 's:/:.:g'; do sed -z -i "$regexp" vofiles; done - xargs -0 --arg-file=vofiles bin/coqchk -boot -silent -o -m -coqlib lib/coq/ @@ -190,39 +172,32 @@ after_script: variables: - $WINDOWS =~ /enabled/ +build:make:base: + <<: *build-make-template + build:base: <<: *build-template - variables: - COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" - # coqdoc for stdlib, until we know how to build it from installed Coq - EXTRA_TARGET: "stdlib" # no coqide for 32bit: libgtk installation problems build:base+32bit: <<: *build-template + script: + - make voboot + - dune build coq.install + - dune build coqide-server.install variables: OPAM_VARIANT: "+32bit" - COQ_EXTRA_CONF: "-native-compiler yes" build:edge: <<: *build-template variables: OPAM_SWITCH: edge - COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" build:edge+flambda: <<: *build-template variables: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" - COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -flambda-opts " - COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures" - -build:egde:dune:dev: - <<: *dune-template - variables: - OPAM_SWITCH: edge - DUNE_TARGET: world windows64: <<: *windows-template @@ -279,30 +254,24 @@ pkg:nix: - nix-build-coq.drv-0/*/test-suite/logs doc:refman: - <<: *doc-template - dependencies: - - build:base - -doc:refman:dune: - <<: *dune-template - dependencies: - - build:base stage: test dependencies: - - build:egde:dune:dev + - build:edge + script: + - make refman variables: OPAM_SWITCH: edge - DUNE_TARGET: refman artifacts: name: "$CI_JOB_NAME" paths: - _build/default/doc/sphinx/_build/html -doc:ml-api:odoc: +doc:ml-api: stage: test dependencies: - - build:egde:dune:dev - script: make -f Makefile.dune apidoc + - build:edge + script: + - make apidoc variables: OPAM_SWITCH: edge artifacts: @@ -337,19 +306,6 @@ test-suite:edge+flambda: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" -test-suite:egde:dune:dev: - stage: test - dependencies: - - build:egde:dune:dev - script: make -f Makefile.dune test-suite - variables: - OPAM_SWITCH: edge - artifacts: - name: "$CI_JOB_NAME.logs" - when: on_failure - paths: - - _build/default/test-suite/logs - validate:base: <<: *validate-template dependencies: diff --git a/.travis.yml b/.travis.yml index 6f625b1c75bfe..d20d82402e1f2 100644 --- a/.travis.yml +++ b/.travis.yml @@ -110,11 +110,11 @@ script: - echo -en 'travis_fold:end:coq.config\\r' - echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r' -- make -j $NJOBS $MAIN_TARGET +- make -f Makefile.make -j $NJOBS $MAIN_TARGET - echo -en 'travis_fold:end:coq.build\\r' - echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r' -- if [ -n "$TEST_TARGET" ]; then $TW make -j $NJOBS $TEST_TARGET; fi +- if [ -n "$TEST_TARGET" ]; then $TW make -f Makefile.make -j $NJOBS $TEST_TARGET; fi - echo -en 'travis_fold:end:coq.test\\r' - set +e diff --git a/Makefile b/Makefile index e0ab169eda94e..159211f1652e4 100644 --- a/Makefile +++ b/Makefile @@ -8,333 +8,5 @@ ## # (see LICENSE file for the text of the license) ## ########################################################################## - # Makefile for Coq -# -# To be used with GNU Make >= 3.81. -# -# This Makefile is now separated into Makefile.{common,build,doc}. -# You won't find Makefiles in sub-directories and this is done on purpose. -# If you are not yet convinced of the advantages of a single Makefile, please -# read -# http://aegis.sourceforge.net/auug97.pdf -# before complaining. -# -# When you are working in a subdir, you can compile without moving to the -# upper directory using "make -C ..", and the output is still understood -# by Emacs' next-error. -# -# Specific command-line options to this Makefile: -# -# make VERBOSE=1 # restore the raw echoing of commands -# make NO_RECALC_DEPS=1 # avoid recomputing dependencies -# -# Nota: the 1 above can be replaced by any non-empty value -# -# ---------------------------------------------------------------------- -# See dev/doc/build-system*.txt for more details/FAQ about this Makefile -# ---------------------------------------------------------------------- - - -########################################################################### -# File lists -########################################################################### - -# NB: due to limitations in Win32, please refrain using 'export' too much -# to communicate between make sub-calls (in Win32, 8kb max per env variable, -# 32kb total) - -# !! Before using FIND_SKIP_DIRS, please read how you should in the !! -# !! FIND_SKIP_DIRS section of dev/doc/build-system.dev.txt !! -FIND_SKIP_DIRS:='(' \ - -name '{arch}' -o \ - -name '.svn' -o \ - -name '_darcs' -o \ - -name '.git' -o \ - -name '.bzr' -o \ - -name 'debian' -o \ - -name "$${GIT_DIR}" -o \ - -name '_build' -o \ - -name '_build_ci' -o \ - -name '_install_ci' -o \ - -name 'gramlib' -o \ - -name 'user-contrib' -o \ - -name 'test-suite' -o \ - -name '.opamcache' -o \ - -name '.coq-native' \ -')' -prune -o - -define find - $(shell find . $(FIND_SKIP_DIRS) '(' -name $(1) ')' -print | sed 's|^\./||') -endef - -define findindir - $(shell find $(1) $(FIND_SKIP_DIRS) '(' -name $(2) ')' -print | sed 's|^\./||') -endef - -## Files in the source tree - -LEXFILES := $(call find, '*.mll') -YACCFILES := $(call find, '*.mly') -export MLLIBFILES := $(call find, '*.mllib') -export MLPACKFILES := $(call find, '*.mlpack') -export MLGFILES := $(call find, '*.mlg') -export CFILES := $(call findindir, 'kernel/byterun', '*.c') - -MERLININFILES := $(call find, '.merlin.in') -export MERLINFILES := $(MERLININFILES:.in=) - -# NB: The lists of currently existing .ml and .mli files will change -# before and after a build or a make clean. Hence we do not export -# these variables, but cleaned-up versions (see below MLFILES and co) - -EXISTINGML := $(call find, '*.ml') -EXISTINGMLI := $(call find, '*.mli') - -## Files that will be generated - -GENMLGFILES:= $(MLGFILES:.mlg=.ml) -export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml -export GENHFILES:=kernel/byterun/coq_jumptbl.h -export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) - -## More complex file lists - -export MLSTATICFILES := $(filter-out $(GENMLFILES), $(EXISTINGML)) -export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) - -include Makefile.common - -########################################################################### -# Starting rules -########################################################################### - -NOARG: world - -.PHONY: NOARG help noconfig submake camldevfiles - -help: - @echo "Please use either:" - @echo " ./configure" - @echo " make world" - @echo " make install" - @echo " make clean" - @echo "or make archclean" - @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 "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 -$(error You have unsaved changes in your editor (emacs?) [$(UNSAVED_FILES)]; \ -cancel them or save before proceeding. Or your editor crashed. \ -Then, you may want to consider whether you want to restore the autosaves) -#If you try to simply remove this explicit test, the compilation may -#fail later. In particular, if a .#*.v file exists, coqdep fails to -#run. -endif - -# Apart from clean and a few misc files, everything will be done in a -# sub-call to make on Makefile.build. This way, we avoid doing here -# the -include of .d : since they trigger some compilations, we do not -# want them for a mere clean. Moreover, we regroup this sub-call in a -# common target named 'submake'. This way, multiple user-given goals -# (cf the MAKECMDGOALS variable) won't trigger multiple (possibly -# parallel) make sub-calls - -ifdef COQ_CONFIGURED -%:: submake ; -else -%:: noconfig ; -endif - -MAKE_OPTS := --warn-undefined-variable --no-builtin-rules - -bin: - mkdir bin - -submake: alienclean camldevfiles | bin - $(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS) - -noconfig: - @echo "Please run ./configure first" >&2; exit 1 - -# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles - -Makefile $(wildcard Makefile.*) config/Makefile : ; - -########################################################################### -# OCaml dev files -########################################################################### -camldevfiles: $(MERLINFILES) META.coq - -# prevent submake dependency -META.coq.in $(MERLININFILES): ; - -.merlin: .merlin.in - cp -a "$<" "$@" - -%/.merlin: %/.merlin.in - cp -a "$<" "$@" - -META.coq: META.coq.in - cp -a "$<" "$@" - -########################################################################### -# Cleaning -########################################################################### - -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean - -clean: objclean cruftclean depclean docclean camldevfilesclean - -cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean - -objclean: archclean indepclean - -cruftclean: mlgclean - find . \( -name '*~' -o -name '*.annot' \) -exec rm -f {} + - rm -f gmon.out core - -camldevfilesclean: - rm -f $(MERLINFILES) META.coq - -indepclean: - rm -f $(GENFILES) - rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(TOPBYTE) - find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -exec rm -f {} + - rm -f */*.pp[iox] plugins/*/*.pp[iox] - rm -rf $(SOURCEDOCDIR) - rm -f toplevel/mltop.byteml toplevel/mltop.optml - rm -f glob.dump - rm -f config/revision.ml revision - rm -f plugins/micromega/.micromega.ml.generated - $(MAKE) -C test-suite clean - -docclean: - rm -f doc/*/*.dvi doc/*/*.aux doc/*/*.log doc/*/*.bbl doc/*/*.blg doc/*/*.toc \ - doc/*/*.idx doc/*/*~ doc/*/*.ilg doc/*/*.ind doc/*/*.dvi.gz doc/*/*.ps.gz doc/*/*.pdf.gz\ - doc/*/*.???idx doc/*/*.???ind doc/*/*.v.tex doc/*/*.atoc doc/*/*.lof\ - doc/*/*.hatoc doc/*/*.haux doc/*/*.hcomind doc/*/*.herrind doc/*/*.hidx doc/*/*.hind \ - doc/*/*.htacind doc/*/*.htoc doc/*/*.v.html - rm -f doc/stdlib/index-list.html doc/stdlib/index-body.html \ - doc/stdlib/*Library.coqdoc.tex doc/stdlib/library.files \ - doc/stdlib/library.files.ls doc/stdlib/FullLibrary.tex - rm -f doc/*/*.ps doc/*/*.pdf doc/*/*.eps doc/*/*.pdf_t doc/*/*.eps_t - rm -rf doc/stdlib/html doc/tutorial/tutorial.v.html - rm -f doc/common/version.tex - rm -f doc/coq.tex - rm -rf doc/sphinx/_build - -archclean: clean-ide optclean voclean - rm -rf _build - rm -f $(ALLSTDLIB).* - -optclean: - rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBINOPT) - rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT) - find . \( -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' \) -exec rm -f {} + - -clean-ide: - rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDE) - rm -f ide/input_method_lexer.ml - rm -f ide/highlight.ml ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml - rm -f ide/utf8_convert.ml - rm -rf $(COQIDEAPP) - -mlgclean: - rm -f $(GENMLGFILES) - -depclean: - find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -exec rm -f {} + - -cacheclean: - find theories plugins test-suite -name '.*.aux' -exec rm -f {} + - -cleanconfig: - rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq config/Info-*.plist - -distclean: clean cleanconfig cacheclean timingclean - -voclean: - find theories plugins test-suite \( -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" \ - -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -exec rm -f {} + - find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} + - -timingclean: - find theories plugins test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' \ - -o -name "*.v.after-timing" -o -name "*.v.timing.diff" -o -name "time-of-build.log" \ - -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" \ - -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -exec rm -f {} + - -# Ensure that every compiled file around has a known source file. -# This should help preventing weird compilation failures caused by leftover -# compiled files after deleting or moving some source files. - -EXISTINGVO:=$(call find, '*.vo') -KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) -ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO)) - -EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa') -KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(MLPACKFILES:.mlpack=.ml) \ - $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp)) -KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \ - $(MLIFILES:.mli=.cmi) \ - $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma -ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS)) - -alienclean: - rm -f $(ALIENOBJS) $(ALIENVO) - -########################################################################### -# Continuous Intregration Tests -########################################################################### -include Makefile.ci - -########################################################################### -# Emacs tags -########################################################################### - -.PHONY: tags printenv - -tags: - echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \ - etags --language=none\ - "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/and[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/type[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/module[ \t]+\([^ \t]+\)/\1/" - echo $(MLGFILES) | sort -r | xargs \ - etags --append --language=none\ - "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" - -checker-tags: - echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \ - etags --language=none\ - "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/and[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/type[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/module[ \t]+\([^ \t]+\)/\1/" - echo $(MLGFILES) | sort -r | xargs \ - etags --append --language=none\ - "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" - -# Useful to check that the exported variables are within the win32 limits - -printenv: - @env - @echo - @echo -n "Maxsize (win32 limit is 8k) : " - @env | wc -L - @echo -n "Total (win32 limit is 32k) : " - @env | wc -m +include Makefile.dune diff --git a/Makefile.make b/Makefile.make new file mode 100644 index 0000000000000..e0ab169eda94e --- /dev/null +++ b/Makefile.make @@ -0,0 +1,340 @@ +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## = 3.81. +# +# This Makefile is now separated into Makefile.{common,build,doc}. +# You won't find Makefiles in sub-directories and this is done on purpose. +# If you are not yet convinced of the advantages of a single Makefile, please +# read +# http://aegis.sourceforge.net/auug97.pdf +# before complaining. +# +# When you are working in a subdir, you can compile without moving to the +# upper directory using "make -C ..", and the output is still understood +# by Emacs' next-error. +# +# Specific command-line options to this Makefile: +# +# make VERBOSE=1 # restore the raw echoing of commands +# make NO_RECALC_DEPS=1 # avoid recomputing dependencies +# +# Nota: the 1 above can be replaced by any non-empty value +# +# ---------------------------------------------------------------------- +# See dev/doc/build-system*.txt for more details/FAQ about this Makefile +# ---------------------------------------------------------------------- + + +########################################################################### +# File lists +########################################################################### + +# NB: due to limitations in Win32, please refrain using 'export' too much +# to communicate between make sub-calls (in Win32, 8kb max per env variable, +# 32kb total) + +# !! Before using FIND_SKIP_DIRS, please read how you should in the !! +# !! FIND_SKIP_DIRS section of dev/doc/build-system.dev.txt !! +FIND_SKIP_DIRS:='(' \ + -name '{arch}' -o \ + -name '.svn' -o \ + -name '_darcs' -o \ + -name '.git' -o \ + -name '.bzr' -o \ + -name 'debian' -o \ + -name "$${GIT_DIR}" -o \ + -name '_build' -o \ + -name '_build_ci' -o \ + -name '_install_ci' -o \ + -name 'gramlib' -o \ + -name 'user-contrib' -o \ + -name 'test-suite' -o \ + -name '.opamcache' -o \ + -name '.coq-native' \ +')' -prune -o + +define find + $(shell find . $(FIND_SKIP_DIRS) '(' -name $(1) ')' -print | sed 's|^\./||') +endef + +define findindir + $(shell find $(1) $(FIND_SKIP_DIRS) '(' -name $(2) ')' -print | sed 's|^\./||') +endef + +## Files in the source tree + +LEXFILES := $(call find, '*.mll') +YACCFILES := $(call find, '*.mly') +export MLLIBFILES := $(call find, '*.mllib') +export MLPACKFILES := $(call find, '*.mlpack') +export MLGFILES := $(call find, '*.mlg') +export CFILES := $(call findindir, 'kernel/byterun', '*.c') + +MERLININFILES := $(call find, '.merlin.in') +export MERLINFILES := $(MERLININFILES:.in=) + +# NB: The lists of currently existing .ml and .mli files will change +# before and after a build or a make clean. Hence we do not export +# these variables, but cleaned-up versions (see below MLFILES and co) + +EXISTINGML := $(call find, '*.ml') +EXISTINGMLI := $(call find, '*.mli') + +## Files that will be generated + +GENMLGFILES:= $(MLGFILES:.mlg=.ml) +export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml +export GENHFILES:=kernel/byterun/coq_jumptbl.h +export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) + +## More complex file lists + +export MLSTATICFILES := $(filter-out $(GENMLFILES), $(EXISTINGML)) +export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) + +include Makefile.common + +########################################################################### +# Starting rules +########################################################################### + +NOARG: world + +.PHONY: NOARG help noconfig submake camldevfiles + +help: + @echo "Please use either:" + @echo " ./configure" + @echo " make world" + @echo " make install" + @echo " make clean" + @echo "or make archclean" + @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 "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 +$(error You have unsaved changes in your editor (emacs?) [$(UNSAVED_FILES)]; \ +cancel them or save before proceeding. Or your editor crashed. \ +Then, you may want to consider whether you want to restore the autosaves) +#If you try to simply remove this explicit test, the compilation may +#fail later. In particular, if a .#*.v file exists, coqdep fails to +#run. +endif + +# Apart from clean and a few misc files, everything will be done in a +# sub-call to make on Makefile.build. This way, we avoid doing here +# the -include of .d : since they trigger some compilations, we do not +# want them for a mere clean. Moreover, we regroup this sub-call in a +# common target named 'submake'. This way, multiple user-given goals +# (cf the MAKECMDGOALS variable) won't trigger multiple (possibly +# parallel) make sub-calls + +ifdef COQ_CONFIGURED +%:: submake ; +else +%:: noconfig ; +endif + +MAKE_OPTS := --warn-undefined-variable --no-builtin-rules + +bin: + mkdir bin + +submake: alienclean camldevfiles | bin + $(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS) + +noconfig: + @echo "Please run ./configure first" >&2; exit 1 + +# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles + +Makefile $(wildcard Makefile.*) config/Makefile : ; + +########################################################################### +# OCaml dev files +########################################################################### +camldevfiles: $(MERLINFILES) META.coq + +# prevent submake dependency +META.coq.in $(MERLININFILES): ; + +.merlin: .merlin.in + cp -a "$<" "$@" + +%/.merlin: %/.merlin.in + cp -a "$<" "$@" + +META.coq: META.coq.in + cp -a "$<" "$@" + +########################################################################### +# Cleaning +########################################################################### + +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean + +clean: objclean cruftclean depclean docclean camldevfilesclean + +cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean + +objclean: archclean indepclean + +cruftclean: mlgclean + find . \( -name '*~' -o -name '*.annot' \) -exec rm -f {} + + rm -f gmon.out core + +camldevfilesclean: + rm -f $(MERLINFILES) META.coq + +indepclean: + rm -f $(GENFILES) + rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(TOPBYTE) + find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -exec rm -f {} + + rm -f */*.pp[iox] plugins/*/*.pp[iox] + rm -rf $(SOURCEDOCDIR) + rm -f toplevel/mltop.byteml toplevel/mltop.optml + rm -f glob.dump + rm -f config/revision.ml revision + rm -f plugins/micromega/.micromega.ml.generated + $(MAKE) -C test-suite clean + +docclean: + rm -f doc/*/*.dvi doc/*/*.aux doc/*/*.log doc/*/*.bbl doc/*/*.blg doc/*/*.toc \ + doc/*/*.idx doc/*/*~ doc/*/*.ilg doc/*/*.ind doc/*/*.dvi.gz doc/*/*.ps.gz doc/*/*.pdf.gz\ + doc/*/*.???idx doc/*/*.???ind doc/*/*.v.tex doc/*/*.atoc doc/*/*.lof\ + doc/*/*.hatoc doc/*/*.haux doc/*/*.hcomind doc/*/*.herrind doc/*/*.hidx doc/*/*.hind \ + doc/*/*.htacind doc/*/*.htoc doc/*/*.v.html + rm -f doc/stdlib/index-list.html doc/stdlib/index-body.html \ + doc/stdlib/*Library.coqdoc.tex doc/stdlib/library.files \ + doc/stdlib/library.files.ls doc/stdlib/FullLibrary.tex + rm -f doc/*/*.ps doc/*/*.pdf doc/*/*.eps doc/*/*.pdf_t doc/*/*.eps_t + rm -rf doc/stdlib/html doc/tutorial/tutorial.v.html + rm -f doc/common/version.tex + rm -f doc/coq.tex + rm -rf doc/sphinx/_build + +archclean: clean-ide optclean voclean + rm -rf _build + rm -f $(ALLSTDLIB).* + +optclean: + rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBINOPT) + rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT) + find . \( -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' \) -exec rm -f {} + + +clean-ide: + rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDE) + rm -f ide/input_method_lexer.ml + rm -f ide/highlight.ml ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml + rm -f ide/utf8_convert.ml + rm -rf $(COQIDEAPP) + +mlgclean: + rm -f $(GENMLGFILES) + +depclean: + find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -exec rm -f {} + + +cacheclean: + find theories plugins test-suite -name '.*.aux' -exec rm -f {} + + +cleanconfig: + rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq config/Info-*.plist + +distclean: clean cleanconfig cacheclean timingclean + +voclean: + find theories plugins test-suite \( -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" \ + -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -exec rm -f {} + + find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} + + +timingclean: + find theories plugins test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' \ + -o -name "*.v.after-timing" -o -name "*.v.timing.diff" -o -name "time-of-build.log" \ + -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" \ + -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -exec rm -f {} + + +# Ensure that every compiled file around has a known source file. +# This should help preventing weird compilation failures caused by leftover +# compiled files after deleting or moving some source files. + +EXISTINGVO:=$(call find, '*.vo') +KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) +ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO)) + +EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa') +KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(MLPACKFILES:.mlpack=.ml) \ + $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp)) +KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \ + $(MLIFILES:.mli=.cmi) \ + $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma +ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS)) + +alienclean: + rm -f $(ALIENOBJS) $(ALIENVO) + +########################################################################### +# Continuous Intregration Tests +########################################################################### +include Makefile.ci + +########################################################################### +# Emacs tags +########################################################################### + +.PHONY: tags printenv + +tags: + echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \ + etags --language=none\ + "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/and[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/type[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/module[ \t]+\([^ \t]+\)/\1/" + echo $(MLGFILES) | sort -r | xargs \ + etags --append --language=none\ + "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" + +checker-tags: + echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \ + etags --language=none\ + "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/and[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/type[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/module[ \t]+\([^ \t]+\)/\1/" + echo $(MLGFILES) | sort -r | xargs \ + etags --append --language=none\ + "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" + +# Useful to check that the exported variables are within the win32 limits + +printenv: + @env + @echo + @echo -n "Maxsize (win32 limit is 8k) : " + @env | wc -L + @echo -n "Total (win32 limit is 32k) : " + @env | wc -m diff --git a/config/dune b/config/dune index c146e7df67fb4..1175666b7fa9a 100644 --- a/config/dune +++ b/config/dune @@ -9,5 +9,10 @@ (rule (targets coq_config.ml coq_config.py Makefile) (mode fallback) - (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX)) + (deps + ; This is needed for the generation of `all_src_dirs` from `plugins` + (source_tree %{project_root}/plugins) + %{project_root}/configure.ml + %{project_root}/dev/ocamldebug-coq.run + (env_var COQ_CONFIGURE_PREFIX)) (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no)))) diff --git a/configure.ml b/configure.ml index 39c65683ff588..a257db798a422 100644 --- a/configure.ml +++ b/configure.ml @@ -1211,10 +1211,10 @@ let write_configml f = pr_b "bytecode_compiler" !prefs.bytecodecompiler; pr_b "native_compiler" !prefs.nativecompiler; - let core_src_dirs = [ "config"; "dev"; "lib"; "clib"; "kernel"; "library"; + let core_src_dirs = [ "config"; "lib"; "clib"; "kernel"; "library"; "engine"; "pretyping"; "interp"; "parsing"; "proofs"; "tactics"; "toplevel"; "printing"; - "grammar"; "ide"; "stm"; "vernac" ] in + "gramlib"; "ide"; "stm"; "vernac" ] in let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ " \"" ^ core_src_subdir ^ "\";\n") "" core_src_dirs in diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh index c450e8157a2d6..6eb5f01c9cd24 100755 --- a/dev/build/osx/make-macos-dmg.sh +++ b/dev/build/osx/make-macos-dmg.sh @@ -10,10 +10,10 @@ VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml) APP=bin/CoqIDE_${VERSION}.app # Create a .app file with CoqIDE, without signing it -make PRIVATEBINARIES="$APP" -j "$NJOBS" -l2 "$APP" +make -f Makefile.make PRIVATEBINARIES="$APP" -j "$NJOBS" -l2 "$APP" # Add Coq to the .app file -make OLDROOT="$OUTDIR" COQINSTALLPREFIX="$APP/Contents/Resources/" install-coq install-ide-toploop +make -f Makefile.make OLDROOT="$OUTDIR" COQINSTALLPREFIX="$APP/Contents/Resources/" install-coq install-ide-toploop # Create the dmg bundle mkdir -p "$DMGDIR" diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 71207bb0404cd..7623fe28399e3 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1428,17 +1428,17 @@ function make_coq { # 8.4x doesn't support parallel make if [[ $COQ_VERSION == 8.4* ]] ; then - log1 make + log1 make -f Makefile.make else # shellcheck disable=SC2086 - log1 make $MAKE_OPT + log1 make -f Makefile.make $MAKE_OPT fi if [ "$INSTALLMODE" == "relocatable" ]; then logn reconfigure ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib/coq" -mandir "$PREFIXCOQ/man" fi - log2 make install + log2 make -f Makefile.make install log1 copy_coq_dlls if [ "$INSTALLOCAML" == "Y" ]; then copy_coq_objects diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 7a450d0d482cc..168b7d3886e7e 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -8,9 +8,10 @@ export NJOBS if [ -n "${GITLAB_CI}" ]; then - # Gitlab build, Coq installed into `_install_ci` - export OCAMLPATH="$PWD/_install_ci/lib:$OCAMLPATH" - export COQBIN="$PWD/_install_ci/bin" + # Gitlab build with Dune + export OCAMLPATH="$PWD/_build/install/default/lib/" + export COQBIN="$PWD/_build/install/default/bin" + export COQLIB="$PWD/_build/install/default/lib/coq" export CI_BRANCH="$CI_COMMIT_REF_NAME" if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]] then diff --git a/dev/ci/user-overlays/08729-ejgallego-dune+kill_make.sh b/dev/ci/user-overlays/08729-ejgallego-dune+kill_make.sh new file mode 100644 index 0000000000000..95b15c2ffc1b1 --- /dev/null +++ b/dev/ci/user-overlays/08729-ejgallego-dune+kill_make.sh @@ -0,0 +1,14 @@ +if [ "$CI_PULL_REQUEST" = "8729" ] || [ "$CI_BRANCH" = "dune+kill_make" ]; then + + true + + # ltac2_CI_REF=rm-section-path + # ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 + + # Elpi_CI_REF=fix_ltac_packing + # Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + + # Equations_CI_REF=vernac+monify_hook + # Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index c5ea88aaf6bf3..0375b5de4caf9 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -152,3 +152,31 @@ useful to Coq, some examples are: - Cross-compilation. - Automatic Generation of OPAM files. - Multi-directory libraries. + +## Internals + +The build setup is mostly vanilla for the OCaml part, however the `.v` +to `.vo` compilation relies on `coq_dune` a `coqdep` wrapper that will +generate the necessary `dune` files. + +As a developer, you should not have to deal with Dune configuration +files on a regular basis unless adding a new library or plugin. + +The vanilla setup declares all the Coq libraries and binaries [we must +respect proper containment/module implementation rules as to allow +packing], and we build custom preprocessors (based on `camlp5` and +`coqpp`) that will process the `ml4`/`mlg` files. + +This suffices to build `coqtop` and `coqide`, all that remains to +handle is `.vo` compilation. + +To teach Dune about the `.vo`, we use a small utility `coq_dune`, +that will generate a `dune` file for each directory in `plugins` and +`theories`. The code is pretty straightforward and declares build +and install rules for each `.v` straight out of `coqdep`. Thus, our +build strategy looks like this: + +1. Use `dune` to build `coqdep` and `coq_dune`. +2. Use `coq_dune` to generate `dune` files for each directory with `.v` files. +3. ? +4. Profit! [Seriously, at this point Dune has the rules to build the stdlib] diff --git a/dune b/dune index 5ec8fa8a0b9eb..53b5785713276 100644 --- a/dune +++ b/dune @@ -71,4 +71,3 @@ ; This will force us to build coqdoc for now (run coqdoc) (run sphinx-build -j4 -b html -d doc/sphinx/_build/doctrees doc/sphinx doc/sphinx/_build/html)))) - diff --git a/test-suite/dune b/test-suite/dune index c5fa0bb14a591..702d3158eea1d 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -4,8 +4,8 @@ ; File that should be promoted. misc/universes/all_stdlib.v ; Dependencies of the legacy makefile - ../Makefile.common ../config/Makefile + ../Makefile.common ; Stuff for the compat script test ../dev/header.ml ../dev/tools/update-compat.py diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index b187aaa563902..33891f310d3c3 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -105,7 +105,7 @@ BEFORE ?= AFTER ?= # FIXME this should be generated by Coq (modules already linked by Coq) -CAMLDONTLINK=camlp5.gramlib,unix,str +CAMLDONTLINK=unix,str # OCaml binaries CAMLC ?= "$(OCAMLFIND)" ocamlc -c @@ -198,7 +198,7 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP5LIB) +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -open Gramlib # ocamldoc fails with unknown argument otherwise CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 713b2ad2b62e4..ed0d224a506a8 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -502,6 +502,8 @@ let add_caml_known phys_dir _ f = | ".mli" -> add_mli_known basename (Some phys_dir) suff | ".mllib" -> add_mllib_known basename (Some phys_dir) suff | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff + (* Must add support to remove the mlpack files *) + (* | ".dune" -> add_mlpack_known basename (Some phys_dir) suff *) | _ -> () let add_coqlib_known recur phys_dir log_dir f =