aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dune
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.dune')
-rw-r--r--Makefile.dune115
1 files changed, 51 insertions, 64 deletions
diff --git a/Makefile.dune b/Makefile.dune
index b77e78db69..b002c7709d 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -1,122 +1,109 @@
# -*- mode: makefile -*-
# Dune Makefile for Coq
-.PHONY: help voboot states world watch check # Main developer targets
-.PHONY: coq coqide coqide-server # Package targets
-.PHONY: quickbyte quickopt quickide # Partial / quick developer targets
+.PHONY: help states world watch check # Main developer targets
.PHONY: refman-html refman-pdf stdlib-html apidoc # Documentation targets
-.PHONY: test-suite release # Accessory targets
+.PHONY: test-suite
.PHONY: fmt ocheck ireport clean # Maintenance targets
+.PHONY: voboot release install # Added just not to break old scripts
# use DUNEOPT=--display=short for a more verbose build
# DUNEOPT=--display=short
-BOOT_DIR=_build_boot
-BOOT_CONTEXT=$(BOOT_DIR)/default
-
help:
- @echo "Welcome to Coq's Dune-based build system. Targets are:"
+ @echo "Welcome to Coq's Dune-based build system. Common developer targets are:"
@echo ""
@echo " - states: build a minimal functional coqtop"
- @echo " - world: build all binaries and libraries"
- @echo " - watch: build all binaries and libraries [continuous build]"
+ @echo " - world: build all public binaries and libraries"
+ @echo " - watch: build all public binaries and libraries [continuous build]"
@echo " - check: build all ML files as fast as possible"
+ @echo " - test-suite: run Coq's test suite"
@echo ""
- @echo " - coq: build package Coq [toplevel compilers, tools, stdlib, no GTK]"
- @echo " - coqide-server: build package coqide-server [XML protocol language server]"
- @echo " - coqide: build package CoqIDE [gtk application]"
+ @echo " Note: these targets produce a developer build,"
+ @echo " not suitable for distribution to end-users"
@echo ""
- @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 " - quickide: build main IDE files [client + server + prelude] using the optimizing compiler"
+ @echo " Documentation targets:"
@echo ""
- @echo " - test-suite: run Coq's test suite"
@echo " - refman-html: build Coq's reference manual [HTML version]"
@echo " - refman-pdf: build Coq's reference manual [PDF version]"
@echo " - stdlib-html: build Coq's Stdlib documentation [HTML version]"
@echo " - apidoc: build ML API documentation"
- @echo " - release: build Coq in release mode"
+ @echo ""
+ @echo " Miscellaneous targets:"
@echo ""
@echo " - fmt: run ocamlformat on the codebase"
@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"
+ @echo ""
+ @echo " To run an app \\in {coqc,coqtop,coqbyte,coqide}:"
+ @echo ""
+ @echo " - use 'dune exec -- dev/shim/app-prelude args'"
+ @echo ""
+ @echo " Provided opam/dune packages are:"
+ @echo ""
+ @echo " - coq: base Coq package, toplevel compilers, tools, stdlib, no GTK"
+ @echo " - coqide-server: XML protocol language server"
+ @echo " - coqide: CoqIDE gtk application"
+ @echo ""
+ @echo " To build a package, you can use:"
+ @echo ""
+ @echo " - 'dune build package.install' : build package in developer mode"
+ @echo " - 'dune build -p package' : build package in release mode"
+ @echo ""
+ @echo " Packages _must_ be installed using release mode, use: 'dune install -p package'"
+ @echo " See Dune documentation for more information."
-# We need to bootstrap with a dummy coq.plugins.ltac so install targets do work.
-plugins/ltac/dune:
- @echo "(library (name ltac_plugin) (public_name coq.plugins.ltac) (modules_without_implementation extraargs extratactics))" > plugins/ltac/dune
-
-voboot: plugins/ltac/dune
- dune build --build-dir=$(BOOT_DIR) $(DUNEOPT) @vodeps
- dune exec --build-dir=$(BOOT_DIR) -- ./tools/coq_dune.exe $(BOOT_CONTEXT)/.vfiles.d
+voboot:
+ @echo "This target is empty and not needed anymore"
-states: voboot
- dune build --display=short $(DUNEOPT) dev/shim/coqtop-prelude
+states:
+ dune build $(DUNEOPT) dev/shim/coqtop-prelude
NONDOC_INSTALL_TARGETS:=coq.install coqide-server.install coqide.install
-world: voboot
+world:
dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS)
-coq: voboot
- dune build $(DUNEOPT) coq.install
-
-coqide: voboot
- dune build $(DUNEOPT) coqide.install
-
-coqide-server: voboot
- dune build $(DUNEOPT) coqide-server.install
-
-watch: voboot
+watch:
dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) -w
-check: voboot
+check:
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
-QUICKBYTE_TARGETS=$(COQTOP_FILES) $(PLUGIN_FILES:.mlpack=.cma) $(PRINTER_FILES) topbin/coqtop_byte_bin.bc
-QUICKOPT_TARGETS=$(COQTOP_FILES:.bc=.exe) $(PLUGIN_FILES:.mlpack=.cmxs) $(PRINTER_FILES:.cma=.cmxa) topbin/coqtop_bin.exe
-
-quickbyte: voboot
- dune build $(DUNEOPT) $(QUICKBYTE_TARGETS)
-
-quickopt: voboot
- dune build $(DUNEOPT) $(QUICKOPT_TARGETS)
-
-quickide: states
- dune build $(DUNEOPT) dev/shim/coqide-prelude
-
-test-suite: voboot
+test-suite:
dune runtest --no-buffer $(DUNEOPT)
-refman-html: voboot
+refman-html:
dune build @refman-html
-refman-pdf: voboot
+refman-pdf:
dune build @refman-pdf
-stdlib-html: voboot
+stdlib-html:
dune build @stdlib-html
-apidoc: voboot
+apidoc:
dune build $(DUNEOPT) @doc
-release: voboot
+release:
+ @echo "release target is deprecated, use dune directly"
dune build $(DUNEOPT) -p coq
-fmt: voboot
+# We define this target as to override Make's built-in one
+install:
+ @echo "To install Coq using dune, use 'dune install -p PACKAGE' where"
+ @echo "PACKAGE is any of the packages defined by opam files in the root dira"
+
+fmt:
dune build @fmt --auto-promote
-ocheck: voboot
+ocheck:
dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all
ireport:
dune clean
- dune build --build-dir=$(BOOT_DIR) $(DUNEOPT) @vodeps
- dune exec --build-dir=$(BOOT_DIR) -- ./tools/coq_dune.exe $(BOOT_CONTEXT)/.vfiles.d
dune build $(DUNEOPT) @install --profile=ireport
clean: