aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.checker
blob: 5b5855782fe9973d8c5d79d415692d850f1de3c8 (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
#######################################################################
#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
# <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
#   \VV/  #############################################################
#    //   #      This file is distributed under the terms of the      #
#         #       GNU Lesser General Public License Version 2.1       #
#######################################################################

## 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)

ifeq ($(BEST),opt)
$(CHICKEN): checker/check.cmxa checker/main.ml
	$(SHOW)'OCAMLOPT -o $@'
	$(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^
	$(STRIP) $@
	$(CODESIGN) $@
else
$(CHICKEN): $(CHICKENBYTE)
	cp $< $@
endif

$(CHICKENBYTE): checker/check.cma 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, $^)

$(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES))
	$(SHOW)'OCAMLDEP  checker/MLFILES checker/MLIFILES'
	$(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) $(filter checker/%, $(MLFILES) $(MLIFILES)) $(TOTARGET)

$(CHECKMLLIBFILE).d: $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) | $(OCAMLLIBDEP)
	$(SHOW)'OCAMLLIBDEP  checker/MLLIBFILES checker/MLPACKFILES'
	$(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) $(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 $<

md5chk:
	$(SHOW)'MD5SUM cic.mli'
	$(HIDE)v=`tr -d "\r" < checker/cic.mli | $(MD5SUM) | sed -n -e 's/ .*//' -e '/^/p'`; \
	       if grep -q "$$v" checker/values.ml; \
	       then true; else echo "Error: outdated checker/values.ml: $$v" >&2; false; fi

.PHONY: md5chk

# For emacs:
# Local Variables:
# mode: makefile
# End: