1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
# -*- mode: makefile -*-
# Dune Makefile for Coq
.PHONY: help states world watch check # Main developer targets
.PHONY: refman-html refman-pdf stdlib-html apidoc # Documentation 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
help:
@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 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 " Note: these targets produce a developer build,"
@echo " not suitable for distribution to end-users"
@echo ""
@echo " Documentation targets:"
@echo ""
@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 ""
@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."
voboot:
@echo "This target is empty and not needed anymore"
states:
dune build $(DUNEOPT) dev/shim/coqtop-prelude
NONDOC_INSTALL_TARGETS:=coq.install coqide-server.install coqide.install
world:
dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS)
watch:
dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) -w
check:
dune build $(DUNEOPT) @check
test-suite:
dune runtest --no-buffer $(DUNEOPT)
refman-html:
dune build @refman-html
refman-pdf:
dune build @refman-pdf
stdlib-html:
dune build @stdlib-html
apidoc:
dune build $(DUNEOPT) @doc
release:
@echo "release target is deprecated, use dune directly"
dune build $(DUNEOPT) -p coq
# 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:
dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all
ireport:
dune clean
dune build $(DUNEOPT) @install --profile=ireport
clean:
dune clean
# Other common dev targets:
#
# dune build coq.install
# dune build coqide.install
#
# Packaging / OPAM targets:
#
# dune -p coq @install
# dune -p coqide @install
|
