Skip to content

Commit

Permalink
[dune] Add "quick" and "check" targets for fast builds.
Browse files Browse the repository at this point in the history
In coq#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
ocaml/dune#1073, and not generating rules
for `.vo` files.
  • Loading branch information
ejgallego committed Nov 6, 2018
1 parent f603366 commit c29eb30
Showing 1 changed file with 19 additions and 1 deletion.
20 changes: 19 additions & 1 deletion Makefile.dune
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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"
Expand All @@ -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

Expand Down

0 comments on commit c29eb30

Please sign in to comment.