diff options
| author | Emilio Jesus Gallego Arias | 2018-10-04 11:50:11 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-09 22:18:57 +0200 |
| commit | b70c5fd9cc29f32c87d72a6da3f731be25c42d85 (patch) | |
| tree | 5b8610aa38eee1eddffec112926ef8274de43a1a /Makefile.dune | |
| parent | 59de2827b63b5bc475452bef385a2149a10a631c (diff) | |
[dune] Provide an optimized build profile with inlining reports.
This satisfies a wish by @ppedrot
Diffstat (limited to 'Makefile.dune')
| -rw-r--r-- | Makefile.dune | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/Makefile.dune b/Makefile.dune index 6733c485fa..d9c1452cae 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -1,7 +1,7 @@ # -*- mode: makefile -*- # Dune Makefile for Coq -.PHONY: voboot states world watch release apidoc ocheck clean help +.PHONY: voboot states world watch release apidoc ocheck ireport clean help # use DUNEOPT=--display=short for a more verbose build # DUNEOPT=--display=short @@ -16,6 +16,7 @@ help: @echo " - release: build Coq in release mode" @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" @@ -41,6 +42,12 @@ apidoc: voboot 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 |