diff options
| author | Emilio Jesus Gallego Arias | 2018-11-05 01:37:15 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-06 17:42:18 +0100 |
| commit | c29eb307760086fb5951a1771a91c25360248852 (patch) | |
| tree | 8085676fa058b9ee90e4bbbdbb07f32a50d5b457 /Makefile.dune | |
| parent | f6033667bd9b8069308d4bcba420c4ce0771e44f (diff) | |
[dune] Add "quick" and "check" targets for fast builds.
In #8900 a quicker build target is requested, this PR does provide
targets towards that goal.
- `check`, introduced in Dune 1.5.0, will build all ml files in a fast way,
- `quick{byte,opt}`, does build a set of relevant hand-picked targets.
Further improvements could come from having `coq_dune` use
`coqtop.byte` when appropriate, taking advantage from
https://github.com/ocaml/dune/issues/1073, and not generating rules
for `.vo` files.
Diffstat (limited to 'Makefile.dune')
| -rw-r--r-- | Makefile.dune | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/Makefile.dune b/Makefile.dune index 298a27c93e..d201d1783a 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -1,7 +1,7 @@ # -*- mode: makefile -*- # Dune Makefile for Coq -.PHONY: help voboot states world watch test-suite release apidoc ocheck ireport clean +.PHONY: help voboot states world watch check quickbyte quickopt test-suite release apidoc ocheck ireport clean # use DUNEOPT=--display=short for a more verbose build # DUNEOPT=--display=short @@ -13,6 +13,9 @@ help: @echo " - states: build a minimal functional coqtop" @echo " - world: build all binaries and libraries" @echo " - watch: build all binaries and libraries [continuous build]" + @echo " - check: build all ML files as fast as possible [requires Dune >= 1.5.0]" + @echo " - quickbyte: build main ML files [coqtop + plugins + ide + printers] using the bytecode compiler" + @echo " - quickopt: build main ML files [coqtop + plugins + ide + printers] using the optimizing compiler" @echo " - test-suite: run Coq's test suite" @echo " - release: build Coq in release mode" @echo " - apidoc: build ML API documentation" @@ -34,6 +37,21 @@ world: voboot watch: voboot dune build $(DUNEOPT) @install -w +check: voboot + dune build $(DUNEOPT) @check + +COQTOP_FILES=ide/idetop.bc ide/coqide_main.bc checker/coqchk.bc +PLUGIN_FILES=$(wildcard plugins/*/*.mlpack) +PRINTER_FILES=dev/top_printers.cma dev/checker_printers.cma +QUICKBYTE_TARGETS=$(COQTOP_FILES) $(PLUGIN_FILES:.mlpack=.cma) $(PRINTER_FILES) topbin/coqtop_byte_bin.bc +QUICKOPT_TARGETS=$(COQTOP_FILES:.bc=.exe) $(PLUGIN_FILES:.mlpack=.cmxa) $(PRINTER_FILES:.cma=.cmxa) topbin/coqtop_bin.exe + +quickbyte: voboot + dune build $(DUNEOPT) $(QUICKBYTE_TARGETS) + +quickopt: voboot + dune build $(DUNEOPT) $(QUICKOPT_TARGETS) + test-suite: voboot dune $(DUNEOPT) runtest |