forked from coq/coq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Makefile.dev
76 lines (63 loc) · 3.01 KB
/
Makefile.dev
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
##########################################################################
## # The Coq Proof Assistant / The Coq Development Team ##
## v # Copyright INRIA, CNRS and contributors ##
## <O___,, # (see version control and CREDITS file for authors & dates) ##
## \VV/ ###############################################################
## // # This file is distributed under the terms of the ##
## # GNU Lesser General Public License Version 2.1 ##
## # (see LICENSE file for the text of the license) ##
##########################################################################
# Extra targets for developers :
# partial targets ...
###################
# Partial builds
###################
# The following partial targets are normally not necessary
# for a complete build of coq, see instead 'make world' for that.
# But these partial targets could be quite handy for quick builds
# of specific components of Coq.
###############################
### 1) general-purpose targets
###############################
coqlight: theories-light tools coqbinaries
.PHONY: coqlight
######################
### 3) theories files
######################
theories:=$(VO_OUT_DIR)theories
arith: $(filter $(theories)/Arith/%, $(THEORIESVO))
bool: $(filter $(theories)/Bool/%, $(THEORIESVO))
classes: $(filter $(theories)/Classes/%, $(THEORIESVO))
compat: $(filter $(theories)/Compat/%, $(THEORIESVO))
fsets: $(filter $(theories)/FSets/%, $(THEORIESVO))
init: $(filter $(theories)/Init/%, $(THEORIESVO))
lists: $(filter $(theories)/Lists/%, $(THEORIESVO))
logic: $(filter $(theories)/Logic/%, $(THEORIESVO))
msets: $(filter $(theories)/MSets/%, $(THEORIESVO))
narith: $(filter $(theories)/NArith/%, $(THEORIESVO))
numbers: $(filter $(theories)/Numbers/%, $(THEORIESVO))
parith: $(filter $(theories)/PArith/%, $(THEORIESVO))
program: $(filter $(theories)/Program/%, $(THEORIESVO))
qarith: $(filter $(theories)/QArith/%, $(THEORIESVO))
reals: $(filter $(theories)/Reals/%, $(THEORIESVO))
relations: $(filter $(theories)/Relations/%, $(THEORIESVO))
setoids: $(filter $(theories)/Setoids/%, $(THEORIESVO))
sets: $(filter $(theories)/Sets/%, $(THEORIESVO))
sorting: $(filter $(theories)/Sorting/%, $(THEORIESVO))
strings: $(filter $(theories)/Strings/%, $(THEORIESVO))
structures: $(filter $(theories)/Structures/%, $(THEORIESVO))
unicode: $(filter $(theories)/Unicode/%, $(THEORIESVO))
vectors: $(filter $(theories)/Vectors/%, $(THEORIESVO))
wellfounded: $(filter $(theories)/Wellfounded/%, $(THEORIESVO))
zarith: $(filter $(theories)/ZArith/%, $(THEORIESVO))
theories-light: $(THEORIESLIGHTVO)
noreal: unicode logic arith bool zarith qarith lists sets fsets \
relations wellfounded setoids sorting
.PHONY: init theories-light noreal
.PHONY: logic arith bool narith zarith qarith lists strings sets
.PHONY: fsets relations wellfounded reals setoids sorting numbers
.PHONY: msets mmaps compat parith classes program unicode structures vectors
# For emacs:
# Local Variables:
# mode: makefile
# End: