blob: 775cdc3c78789356bdd61e29bd7ad306b481ed6b (
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
|
# 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
# Objects files
CONFIG=config/coq_config.cmo
LIB=lib/pp_control.cmo lib/pp.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
OBJS=$(CONFIG) $(LIB) $(KERNEL)
# Targets
world: $(OBJS)
$(OCAMLC) -o coqtop.byte $(OBJS)
# Literate programming (with ocamlweb)
LPLIB = lib/doc.tex $(LIB:.cmo=.mli)
LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli)
LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL)
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/"
# Default rules
.SUFFIXES: .ml .mli .cmo .cmi .cmx
.ml.cmo:
$(OCAMLC) $(BYTEFLAGS) -c $<
.mli.cmi:
$(OCAMLC) $(BYTEFLAGS) -c $<
.ml.cmx:
$(OCAMLOPT) $(OPTFLAGS) -c $<
# Cleaning
archclean::
rm -f config/*.cmx config/*.[so]
rm -f lib/*.cmx lib/*.[so]
rm -f kernel/*.cmx kernel/*.[so]
cleanall:: archclean
rm -f *~
rm -f config/*.cm[io] config/*~
rm -f lib/*.cm[io] lib/*~
rm -f kernel/*.cm[io] kernel/*~
cleanconfig::
rm -f config/Makefile config/coq_config.ml
# Dependencies
depend:
$(OCAMLDEP) $(DEPFLAGS) */*.mli */*.ml > .depend
include .depend
|
