blob: 581d75146435b1748ecb6e2f7d86a6e3199aba71 (
plain)
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
|
# Main Makefile for Coq
include config/Makefile
noargument:
@echo Please use either
@echo " ./configure"
@echo " make world"
@echo " make install"
@echo " make cleanall"
@echo or make archclean
BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG)
OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF)
OCAMLDEP=ocamldep
DEPFLAGS=$(INCLUDES)
INCLUDES=-I config -I lib -I kernel -I library -I parsing -I $(CAMLP4LIB)
CAMLP4EXTEND=camlp4o $(INCLUDES) pa_extend.cmo
OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS)
OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS)
# Objects files
CLIBS=unix.cma
CAMLP4OBJS=gramlib.cma
CONFIG=config/coq_config.cmo
LIB=lib/pp_control.cmo lib/pp.cmo lib/system.cmo lib/util.cmo \
lib/hashcons.cmo lib/dyn.cmo
KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
kernel/sign.cmo kernel/evd.cmo kernel/constant.cmo \
kernel/inductive.cmo kernel/sosub.cmo kernel/abstraction.cmo \
kernel/environ.cmo kernel/instantiate.cmo \
kernel/closure.cmo kernel/reduction.cmo \
kernel/type_errors.cmo kernel/typeops.cmo kernel/indtypes.cmo \
kernel/typing.cmo
LIBRARY=library/libobject.cmo library/summary.cmo
PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \
parsing/g_prim.cmo parsing/g_basevernac.cmo parsing/g_vernac.cmo \
parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_multiple_case.cmo
OBJS=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PARSING)
# Targets
world: minicoq coqtop
# coqtop
coqtop: $(OBJS)
ocamlmktop $(INCLUDES) -o coqtop -custom $(CLIBS) $(CAMLP4OBJS) \
$(OBJS) $(OSDEPLIBS)
# minicoq
MINICOQOBJS=$(CONFIG) $(LIB) $(KERNEL) \
parsing/lexer.cmo parsing/g_minicoq.cmo toplevel/minicoq.cmo
minicoq: $(MINICOQOBJS)
$(OCAMLC) $(INCLUDES) -o minicoq -custom $(CLIBS) $(CAMLP4OBJS) \
$(MINICOQOBJS) $(OSDEPLIBS)
# Literate programming (with ocamlweb)
LPLIB = lib/doc.tex $(LIB:.cmo=.mli)
LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli)
LPLIBRARY = library/doc.tex $(LIBRARY:.cmo=.mli)
LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) $(LPLIBRARY)
lp: doc/coq.ps
doc/coq.ps: doc/coq.tex
cd doc; make coq.ps
doc/coq.tex: $(LPFILES)
ocamlweb -o doc/coq.tex $(LPFILES)
# Emacs tags
tags:
find . -name "*.ml*" | sort -r | xargs \
etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
"--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
"--regex=/and[ \t]+\([^ \t]+\)/\1/" \
"--regex=/type[ \t]+\([^ \t]+\)/\1/" \
"--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
"--regex=/val[ \t]+\([^ \t]+\)/\1/" \
"--regex=/module[ \t]+\([^ \t]+\)/\1/"
# Special rules
parsing/lexer.cmo: parsing/lexer.ml
$(OCAMLC_P4O) -c $<
beforedepend:: parsing/lexer.ml
# grammar modules with camlp4
parsing/q_coqast.cmo: parsing/q_coqast.ml4
$(OCAMLC) $(BYTEFLAGS) -c -pp "camlp4o q_MLast.cmo -impl" -impl $<
parsing/g_prim.cmo: parsing/g_prim.ml4
$(OCAMLC) $(BYTEFLAGS) -c -pp "camlp4o pa_extend.cmo -impl" -impl $<
GRAMMAROBJS=./lib/pp_control.cmo ./lib/pp.cmo ./lib/util.cmo ./lib/dyn.cmo \
./lib/hashcons.cmo ./parsing/coqast.cmo ./parsing/lexer.cmo \
./parsing/pcoq.cmo ./parsing/q_coqast.cmo ./parsing/g_prim.cmo
parsing/grammar.cma: $(GRAMMAROBJS)
$(OCAMLC) $(BYTEFLAGS) $(GRAMMAROBJS) -linkall -a -o $@
parsing/g_%.cmo: parsing/g_%.ml4 parsing/grammar.cma
$(OCAMLC) $(BYTEFLAGS) -c -pp "camlp4o -I parsing pa_extend.cmo grammar.cma -impl" -impl $<
beforedepend:: $(GRAMMAROBJS)
# Default rules
.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .ml4
.ml.cmo:
$(OCAMLC) $(BYTEFLAGS) -c $<
.mli.cmi:
$(OCAMLC) $(BYTEFLAGS) -c $<
.ml.cmx:
$(OCAMLOPT) $(OPTFLAGS) -c $<
.mll.ml:
ocamllex $<
.ml4.cmo:
$(OCAMLC) $(BYTEFLAGS) -I $(CAMLP4LIB) -pp "$(CAMLP4EXTEND) -impl" -c -impl $<
.ml44.cmx:
$(OCAMLOPT) $(OPTFLAGS) -I $(CAMLP4LIB) -pp "$(CAMLP4EXTEND) -impl" -c -impl $<
# Cleaning
archclean::
rm -f config/*.cmx config/*.[so]
rm -f lib/*.cmx lib/*.[so]
rm -f kernel/*.cmx kernel/*.[so]
rm -f library/*.cmx library/*.[so]
rm -f parsing/*.cmx parsing/*.[so]
cleanall:: archclean
rm -f *~
rm -f config/*.cm[io] config/*~
rm -f lib/*.cm[io] lib/*~
rm -f kernel/*.cm[io] kernel/*~
rm -f library/*.cm[io] library/*~
rm -f parsing/*.cm[io] parsing/*~
cleanconfig::
rm -f config/Makefile config/coq_config.ml
# Dependencies
depend: beforedepend
$(OCAMLDEP) $(DEPFLAGS) */*.mli */*.ml > .depend
for f in */*.ml4; do \
file=`dirname $$f`/`basename $$f .ml4`; \
camlp4o $(INCLUDES) pa_extend.cmo q_MLast.cmo $(GRAMMAROBJS) pr_o.cmo -impl $$f > $$file.ml; \
ocamldep $(DEPFLAGS) $$file.ml >> .depend; \
rm -f $$file.ml; \
done
include .depend
|