From c29eb307760086fb5951a1771a91c25360248852 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 5 Nov 2018 01:37:15 +0100
Subject: [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.
---
 Makefile.dune | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

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
 
-- 
cgit v1.2.3