From 79534f2079d6486557642af2f0ae593276550c3c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 15 Oct 2018 18:05:29 +0200 Subject: [PATCH] [dune] Switch to a Dune-based build system. Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see #8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until https://github.com/ocaml/dune/issues/1155 lands in Dune itself. https://github.com/ocaml/dune/issues/1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by #8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so. --- .gitlab-ci.yml | 120 ++---- .travis.yml | 4 +- Makefile | 371 +++--------------- Makefile.dune | 70 ---- Makefile.make | 345 ++++++++++++++++ config/dune | 7 +- dev/build/osx/make-macos-dmg.sh | 4 +- dev/build/windows/makecoq_mingw.sh | 6 +- dev/ci/ci-common.sh | 7 +- .../08729-ejgallego-dune+kill_make.sh | 14 + dev/doc/build-system.dune.md | 28 ++ dune | 1 - test-suite/dune | 2 +- tools/coqdep_common.ml | 2 + 14 files changed, 490 insertions(+), 491 deletions(-) delete mode 100644 Makefile.dune create mode 100644 Makefile.make create mode 100644 dev/ci/user-overlays/08729-ejgallego-dune+kill_make.sh diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index a0f44e0f483b..6f006fe129d1 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -54,6 +54,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" @@ -67,76 +81,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 @@ -144,7 +126,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/ @@ -189,39 +171,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 @@ -278,30 +253,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: @@ -336,19 +305,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 6f625b1c75bf..d20d82402e1f 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 b74e4e5d4ffa..0510eb18a69d 100644 --- a/Makefile +++ b/Makefile @@ -1,345 +1,64 @@ -########################################################################## -## # 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 '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 ML4FILES := $(call find, '*.ml4') -export MLGFILES := $(call find, '*.mlg') -export CFILES := $(call findindir, 'kernel/byterun', '*.c') +# use DUNEOPT=--display=short for a more verbose build +# DUNEOPT=--display=short -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 - -GENML4FILES:= $(ML4FILES:.ml4=.ml) -GENMLGFILES:= $(MLGFILES:.mlg=.ml) -export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) kernel/copcodes.ml -export GENHFILES:=kernel/byterun/coq_jumptbl.h -export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) - -# NB: all files in $(GENFILES) can be created initially, while -# .ml files in $(GENML4FILES) might need some intermediate building. -# That's why we keep $(GENML4FILES) out of $(GENFILES) - -## More complex file lists - -export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES) $(GENMLGFILES), $(EXISTINGML)) -export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) - -include Makefile.common - -########################################################################### -# Starting rules -########################################################################### - -NOARG: world - -.PHONY: NOARG help noconfig submake camldevfiles +BUILD_CONTEXT=_build/default 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 + @echo "Welcome to Coq's Dune-based build system. Targets are:" + @echo " - states: build a minimal functional coqtop" + @echo " - world: build all binaries and libraries" + @echo " - watch: build all binaries and libraries [continuous build]" + @echo " - release: build Coq in release mode" + @echo " - refman: build Coq's reference manual" + @echo " - apidoc: build ML API documentation" + @echo " - ocheck: build for all supported OCaml versions [requires OPAM]" + @echo " - clean: remove build directory and autogenerated files" + @echo " - help: show this message" -bin: - mkdir bin +voboot: + dune build $(DUNEOPT) @vodeps + dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d -submake: alienclean camldevfiles | bin - $(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS) +states: voboot + dune build $(DUNEOPT) theories/Init/Prelude.vo -noconfig: - @echo "Please run ./configure first" >&2; exit 1 +world: voboot + dune build $(DUNEOPT) @install -# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles +test-suite: voboot + dune $(DUNEOPT) runtest -Makefile $(wildcard Makefile.*) config/Makefile : ; +watch: voboot + dune build $(DUNEOPT) @install -w -########################################################################### -# OCaml dev files -########################################################################### -camldevfiles: $(MERLINFILES) META.coq +release: voboot + dune build $(DUNEOPT) -p coq -# prevent submake dependency -META.coq.in $(MERLININFILES): ; +refman: voboot + dune build @refman -.merlin: .merlin.in - cp -a "$<" "$@" +apidoc: voboot + dune build $(DUNEOPT) @doc -%/.merlin: %/.merlin.in - cp -a "$<" "$@" +ocheck: voboot + dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all -META.coq: META.coq.in - cp -a "$<" "$@" +clean: + dune clean -########################################################################### -# Cleaning -########################################################################### - -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean alienclean - -clean: objclean cruftclean depclean docclean camldevfilesclean - -cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean - -objclean: archclean indepclean - -cruftclean: ml4clean - 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) - -ml4clean: - rm -f $(GENML4FILES) $(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 dev/camlp5.dbg 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) $(GENML4FILES) $(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)) +# Other common dev targets +# +# dune build coq.install +# dune build ide/coqide.install -alienclean: - rm -f $(ALIENOBJS) $(ALIENVO) +# Packaging / OPAM targets: +# +# dune -p coq @install +# dune -p coqide @install -########################################################################### -# Continuous Intregration Tests -########################################################################### include Makefile.ci - -########################################################################### -# Emacs tags -########################################################################### - -.PHONY: tags printenv - -tags: - echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(ML4FILES) | 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 $(ML4FILES) | sort -r | xargs \ - etags --append --language=none\ - "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" - -checker-tags: - echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(ML4FILES) | 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 $(ML4FILES) | 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/Makefile.dune b/Makefile.dune deleted file mode 100644 index a2367bc5d668..000000000000 --- a/Makefile.dune +++ /dev/null @@ -1,70 +0,0 @@ -# -*- mode: makefile -*- -# Dune Makefile for Coq - -.PHONY: help voboot states world watch test-suite release refman apidoc ocheck ireport clean - -# use DUNEOPT=--display=short for a more verbose build -# DUNEOPT=--display=short - -BUILD_CONTEXT=_build/default - -help: - @echo "Welcome to Coq's Dune-based build system. Targets are:" - @echo " - states: build a minimal functional coqtop" - @echo " - world: build all binaries and libraries" - @echo " - watch: build all binaries and libraries [continuous build]" - @echo " - test-suite: run Coq's test suite" - @echo " - release: build Coq in release mode" - @echo " - refman: build Coq's reference manual" - @echo " - apidoc: build ML API documentation" - @echo " - ocheck: build for all supported OCaml versions [requires OPAM]" - @echo " - ireport: build with optimized flambda settings and emit an inline report" - @echo " - clean: remove build directory and autogenerated files" - @echo " - help: show this message" - -voboot: - dune build $(DUNEOPT) @vodeps - dune exec ./tools/coq_dune.exe $(BUILD_CONTEXT)/.vfiles.d - -states: voboot - dune build $(DUNEOPT) theories/Init/Prelude.vo - -world: voboot - dune build $(DUNEOPT) @install - -watch: voboot - dune build $(DUNEOPT) @install -w - -test-suite: voboot - dune $(DUNEOPT) runtest - -release: voboot - dune build $(DUNEOPT) -p coq - -refman: voboot - dune build @refman - -apidoc: voboot - dune build $(DUNEOPT) @doc - -ocheck: voboot - dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all - -ireport: - dune clean - dune build $(DUNEOPT) @vodeps --profile=ireport - dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d --profile=ireport - dune build $(DUNEOPT) @install --profile=ireport - -clean: - dune clean - -# Other common dev targets -# -# dune build coq.install -# dune build ide/coqide.install - -# Packaging / OPAM targets: -# -# dune -p coq @install -# dune -p coqide @install diff --git a/Makefile.make b/Makefile.make new file mode 100644 index 000000000000..b74e4e5d4ffa --- /dev/null +++ b/Makefile.make @@ -0,0 +1,345 @@ +########################################################################## +## # 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 '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 ML4FILES := $(call find, '*.ml4') +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 + +GENML4FILES:= $(ML4FILES:.ml4=.ml) +GENMLGFILES:= $(MLGFILES:.mlg=.ml) +export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) kernel/copcodes.ml +export GENHFILES:=kernel/byterun/coq_jumptbl.h +export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) + +# NB: all files in $(GENFILES) can be created initially, while +# .ml files in $(GENML4FILES) might need some intermediate building. +# That's why we keep $(GENML4FILES) out of $(GENFILES) + +## More complex file lists + +export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES) $(GENMLGFILES), $(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 ml4clean depclean cleanconfig distclean voclean timingclean alienclean + +clean: objclean cruftclean depclean docclean camldevfilesclean + +cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean + +objclean: archclean indepclean + +cruftclean: ml4clean + 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) + +ml4clean: + rm -f $(GENML4FILES) $(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 dev/camlp5.dbg 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) $(GENML4FILES) $(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)) $(ML4FILES) | 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 $(ML4FILES) | sort -r | xargs \ + etags --append --language=none\ + "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" + +checker-tags: + echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(ML4FILES) | 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 $(ML4FILES) | 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 c146e7df67fb..1175666b7fa9 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/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh index c450e8157a2d..6eb5f01c9cd2 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 c3d895784ec9..dcaf375ad3d4 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 7a450d0d482c..168b7d3886e7 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 000000000000..95b15c2ffc1b --- /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 91ab57f1e9b2..c1fa620c6cb1 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -131,3 +131,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 7d657563da1c..39c7723b7331 100644 --- a/dune +++ b/dune @@ -70,4 +70,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 c5fa0bb14a59..702d3158eea1 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/coqdep_common.ml b/tools/coqdep_common.ml index 6a913ea89476..74f84e6317d8 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 =