blob: 2bcc9d3656f1b395ad0369fa35fc50b660e2551a (
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
|
OCAMLC=ocamlc
OCAMLOPT=ocamlopt
COQSRC=..
MLDIRS=-I $(COQSRC)/config -I $(COQSRC)/lib -I $(COQSRC)/kernel -I +camlp4
BYTEFLAGS=$(MLDIRS)
OPTFLAGS=$(MLDIRS)
CHECKERNAME=coqchk
BINARIES=../bin/$(CHECKERNAME)$(EXE) ../bin/$(CHECKERNAME).opt$(EXE)
MCHECKERLOCAL :=\
declarations.cmo environ.cmo \
closure.cmo reduction.cmo \
type_errors.cmo \
modops.cmo \
inductive.cmo typeops.cmo \
indtypes.cmo subtyping.cmo mod_checking.cmo \
validate.cmo \
safe_typing.cmo check.cmo \
check_stat.cmo checker.cmo
MCHECKER:=\
$(COQSRC)/config/coq_config.cmo \
$(COQSRC)/lib/pp_control.cmo $(COQSRC)/lib/pp.cmo $(COQSRC)/lib/compat.cmo \
$(COQSRC)/lib/util.cmo $(COQSRC)/lib/option.cmo $(COQSRC)/lib/hashcons.cmo \
$(COQSRC)/lib/system.cmo $(COQSRC)/lib/flags.cmo \
$(COQSRC)/lib/predicate.cmo $(COQSRC)/lib/rtree.cmo \
$(COQSRC)/kernel/names.cmo $(COQSRC)/kernel/univ.cmo \
$(COQSRC)/kernel/esubst.cmo term.cmo \
$(MCHECKERLOCAL)
all: $(BINARIES)
byte : ../bin/$(CHECKERNAME)$(EXE)
opt : ../bin/$(CHECKERNAME).opt$(EXE)
check.cma: $(MCHECKERLOCAL)
ocamlc $(BYTEFLAGS) -a -o $@ $(MCHECKER)
check.cmxa: $(MCHECKERLOCAL:.cmo=.cmx)
ocamlopt $(OPTFLAGS) -a -o $@ $(MCHECKER:.cmo=.cmx)
../bin/$(CHECKERNAME)$(EXE): check.cma
ocamlc $(BYTEFLAGS) -o $@ unix.cma gramlib.cma check.cma main.ml
../bin/$(CHECKERNAME).opt$(EXE): check.cmxa
ocamlopt $(OPTFLAGS) -o $@ unix.cmxa gramlib.cmxa check.cmxa main.ml
stats:
@echo STRUCTURE
@wc names.ml term.ml declarations.ml environ.ml type_errors.ml
@echo
@echo REDUCTION
@-wc esubst.ml closure.ml reduction.ml
@echo
@echo TYPAGE
@wc univ.ml inductive.ml indtypes.ml typeops.ml safe_typing.ml
@echo
@echo MODULES
@wc modops.ml subtyping.ml
@echo
@echo INTERFACE
@wc check*.ml main.ml
@echo
@echo TOTAL
@wc *.ml | tail -1
.SUFFIXES:.ml .mli .cmi .cmo .cmx
.ml.cmo:
$(OCAMLC) -c $(BYTEFLAGS) $<
.ml.cmx:
$(OCAMLOPT) -c $(OPTFLAGS) $<
.mli.cmi:
$(OCAMLC) -c $(BYTEFLAGS) $<
depend::
ocamldep *.ml* > .depend
clean::
rm -f *.cm* *.o *.a *~ $(BINARIES)
-include .depend
|
