aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/Makefile
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