Codebase list coq / upstream/8.9.1 Makefile.checker
upstream/8.9.1

Tree @upstream/8.9.1 (Download .tar.gz)

Makefile.checker @upstream/8.9.1 — raw · history · blame 

  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
##########################################################################
##         #   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 $< $@
checker/esubst.ml: kernel/esubst.ml
	cp -a $< $@
checker/names.mli: kernel/names.mli
	cp -a $< $@
checker/names.ml: kernel/names.ml
	cp -a $< $@

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: