-
Notifications
You must be signed in to change notification settings - Fork 0
/
Makefile.dune
185 lines (155 loc) · 6.35 KB
/
Makefile.dune
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
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
# -*- mode: makefile -*-
# Dune Makefile for Coq
.PHONY: help help-install states world watch check # Main developer targets
.PHONY: refman-html refman-pdf stdlib-html apidoc # Documentation targets
.PHONY: test-suite dev-targets
.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 ""
@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 [env NJOBS=N to set job parallelism]"
@echo ""
@echo " Note: running ./configure is not recommended,"
@echo " see dev/doc/build-system.dune.md for more info"
@echo " Note: these targets produce a developer build, not suitable"
@echo " for distribution to end-users or install"
@echo ""
@echo " To run an \$$app \\in {coqc,coqtop,coqbyte,coqide}:"
@echo ""
@echo " - use 'dune exec -- dev/shim/\$$app-prelude args'"
@echo " Example: 'dune exec -- dev/shim/coqc-prelude file.v'"
@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 " Type 'make help-install' for installation instructions"
@echo " Type 'make dev-targets' for more developer targets"
dev-targets:
@echo ""
@echo "In order to get a functional Coq install layout, the world target is required."
@echo "However, This is often inconvenient for developers, due to the large amount of"
@echo "files that world will build. We provide some useful subtargets here:"
@echo ""
@echo " - theories-foo: for each directory theories/Foo, build the vo files for it and set them up in _build/install/default."
@echo " For instance the init target builds the prelude, combined with coq-core.install it produces a fully functional layout in _build/install/default."
help-install:
@echo ""
@echo "The Dune-based Coq build is split in packages; see Dune and dev/doc"
@echo "documentation for more details. A quick install of Coq alone can done with"
@echo ""
@echo " $ ./configure -prefix <install_prefix>"
@echo " $ dune build -p coq-core,coq-stdlib && dune install coq-core coq-stdlib"
@echo ""
@echo " Provided opam/dune packages are:"
@echo ""
@echo " - coq-core: base Coq package, toplevel compilers, plugins, tools, no stdlib, no GTK"
@echo " - coq-stdlib: Coq's standard library"
@echo " - coqide-server: XML protocol language server"
@echo " - coqide: CoqIDE gtk application"
@echo " - coq: meta package depending on coq-core coq-stdlib"
@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 only if built using release mode, to install a package use: "
@echo ""
@echo " - 'dune install $install_opts package'"
@echo ""
@echo " Note that building a package in release mode ignores other packages present in"
@echo " the worktree. 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-core.install coq-stdlib.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 --no-buffer @refman-html
refman-pdf:
dune build --no-buffer @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 build -p P && dune install P'"
@echo "where P is any of the packages defined by opam files in the root dir"
@false
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
# ci-* targets
CI_PURE_DUNE:=1
export CI_PURE_DUNE
include Makefile.ci
# Custom targets to create subsets of the world target but with less
# compiled files. This is desired when we want to have our Coq Dune
# build with Coq developments that are not dunerized and thus still
# expect an install layout with a working Coq setup, but smaller than
# world.
#
# Unfortunately, Dune still lacks the capability to refer to install
# targets in rules, see https://github.com/ocaml/dune/issues/3192 ;
# thus we can't simply yet use `%{pkg:coq:theories/Arith/Arith.vo` to
# have the rule install the target, we thus imitate such behavior
# using make as a helper.
# $(1) is the directory (theories/Foo/)
# $(2) is the name (foo)
define subtarget =
.PHONY: theories-$(2)
$(2)_FILES=$$(wildcard $(1)*.v)
$(2)_FILES_PATH=$$(addprefix _build/install/default/lib/coq/, $$($(2)_FILES:.v=.vo))
theories-$(2):
@echo "DUNE $(1)*.vo"
@dune build $$($(2)_FILES_PATH)
endef
$(foreach subdir,$(wildcard theories/*/),$(eval $(call subtarget,$(subdir),$(shell echo $(subst /,,$(subst theories/,,$(subdir))) | tr A-Z a-z))))
# Other common dev targets:
#
# dune build coq-core.install
# dune build coq.install
# dune build coqide.install
#
# Packaging / OPAM targets:
#
# dune -p coq @install
# dune -p coqide @install