Makefile.checker

##########################################################################
##         #   The Coq Proof Assistant / The Coq Development Team       ##
##  v      #         Copyright INRIA, CNRS and contributors             ##
## <O___,, # (see version control and CREDITS file for authors & dates) ##
##   \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 -I kernel -I kernel/byterun

## 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): config/config.cmxa clib/clib.cmxa lib/lib.cmxa kernel/kernel.cmxa \
checker/check.cmxa $(LIBCOQRUN) checker/coqchk.mli checker/coqchk.ml
	$(SHOW)'OCAMLOPT -o $@'
	$(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^
	$(STRIP_HIDE) $@
	$(CODESIGN_HIDE) $@
else
$(CHICKEN): $(CHICKENBYTE)
	rm -f $@ && cp $< $@
endif

$(CHICKENBYTE): config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma \
checker/check.cma $(LIBCOQRUN) checker/coqchk.mli checker/coqchk.ml
	$(SHOW)'OCAMLC -o $@'
	$(HIDE)$(OCAMLC) -linkpkg $(SYSMOD) $(CHKLIBS) $(BYTEFLAGS) -cclib -lcoqrun $(VMBYTEFLAGS) -o $@ $^

checker/check.cma: checker/check.mllib
	$(SHOW)'OCAMLC -a -o $@'
	$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)

checker/check.cmxa: checker/check.mllib
	$(SHOW)'OCAMLOPT -a -o $@'
	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^)

CHECKMLFILES:=$(filter checker/%, $(MLFILES) $(MLIFILES))

$(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES))
	$(SHOW)'OCAMLDEP  checker/MLFILES checker/MLIFILES'
	$(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) $(CHECKMLFILES) $(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 $<

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