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
|
##########################################################################
## # The Coq Proof Assistant / The Coq Development Team ##
## v # INRIA, CNRS and contributors - Copyright 1999-2018 ##
## <O___,, # (see CREDITS file for the list of authors) ##
## \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) ##
##########################################################################
## Makefile rules for building Coqchk
## NB: For the moment, the build system of Coqchk is part of
## the one of Coq. In particular, this Makefile.checker is included in
## Makefile.build. Please ensure that the rules define here are
## indeed specific to files of the form checker/*
# The binaries
CHICKENBYTE:=bin/coqchk.byte$(EXE)
CHICKEN:=bin/coqchk$(EXE)
# The sources
CHKLIBS:= -I config -I clib -I lib -I checker
## NB: currently, both $(OPTFLAGS) and $(BYTEFLAGS) contain -thread
# The rules
CHECKMLDFILE := checker/.mlfiles
CHECKMLLIBFILE := checker/.mllibfiles
CHECKERDEPS := $(addsuffix .d, $(CHECKMLDFILE) $(CHECKMLLIBFILE))
-include $(CHECKERDEPS)
# Copied files
checker/esubst.mli: kernel/esubst.mli
cp -a $< $@
sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
checker/esubst.ml: kernel/esubst.ml
cp -a $< $@
sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
checker/names.mli: kernel/names.mli
cp -a $< $@
sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
checker/names.ml: kernel/names.ml
cp -a $< $@
sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
ifeq ($(BEST),opt)
$(CHICKEN): checker/check.cmxa checker/main.mli checker/main.ml
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^
$(STRIP_HIDE) $@
$(CODESIGN_HIDE) $@
else
$(CHICKEN): $(CHICKENBYTE)
cp $< $@
endif
$(CHICKENBYTE): checker/check.cma checker/main.mli checker/main.ml
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(OCAMLC) -linkpkg $(SYSMOD) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^
checker/check.cma: checker/check.mllib | md5chk
$(SHOW)'OCAMLC -a -o $@'
$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
checker/check.cmxa: checker/check.mllib | md5chk
$(SHOW)'OCAMLOPT -a -o $@'
$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^)
CHECKGENFILES:=$(addprefix checker/, names.mli names.ml esubst.mli esubst.ml)
CHECKMLFILES:=$(filter checker/%, $(MLFILES) $(MLIFILES)) $(CHECKGENFILES) \
$(filter dev/checker_%, $(MLFILES) $(MLIFILES))
$(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES) $(CHECKGENFILES))
$(SHOW)'OCAMLDEP checker/MLFILES checker/MLIFILES'
$(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) $(CHECKMLFILES) $(TOTARGET)
$(CHECKMLLIBFILE).d: $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES) $(CHECKGENFILES)) | $(OCAMLLIBDEP)
$(SHOW)'OCAMLLIBDEP checker/MLLIBFILES checker/MLPACKFILES'
$(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES) $(CHECKGENFILES)) $(TOTARGET)
checker/%.cmi: checker/%.mli
$(SHOW)'OCAMLC $<'
$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -c $<
checker/%.cmo: checker/%.ml
$(SHOW)'OCAMLC $<'
$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -c $<
checker/%.cmx: checker/%.ml
$(SHOW)'OCAMLOPT $<'
$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -c $<
dev/checker_%.cmo: dev/checker_%.ml
$(SHOW)'OCAMLC $<'
$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -I dev/ -c $<
dev/checker_%.cmi: dev/checker_%.mli
$(SHOW)'OCAMLC $<'
$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -I dev/ -c $<
md5chk:
$(SHOW)'MD5SUM cic.mli'
$(HIDE)if grep -q "^MD5 $$($(OCAML) tools/md5sum.ml checker/cic.mli)$$" checker/values.ml; \
then true; else echo "Error: outdated checker/values.ml" >&2; false; fi
.PHONY: md5chk
# For emacs:
# Local Variables:
# mode: makefile
# End:
|
