Makefile.example 4.02 KB
Newer Older
charguer's avatar
fixes  
charguer committed
1
.PHONY: all code cf depend quick proof proof_vo clean
charguer's avatar
charguer committed
2 3 4


##############################################################
charguer's avatar
charguer committed
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
#
# This script is meant to be included by immediate subfolders of $(CFML)/examples.
#
# Optionally, the variables $(ML) can be used to specify which sources to 
# build characteristic formulae for.
#
# Optionally, the variables $(ML_MAIN) can be used to specify which sources 
# to consider for compilation using ocamlbuild.
#
# Optionally, the variables $(V) can be used to specify which coq sources to 
# compile. $(V_IGNORED) can be used to specify instead which sources to ignore.
#
# Optionally, $(OCAML_FLAGS) can be set (e.g. to "-rectypes").
#
# The file settings.sh in the $(CFML) folder can bind path to OCAMLBIN and COQBIN.
#
charguer's avatar
charguer committed
21

charguer's avatar
charguer committed
22

charguer's avatar
charguer committed
23
##############################################################
charguer's avatar
charguer committed
24 25
# Parameters

POTTIER Francois's avatar
POTTIER Francois committed
26 27 28 29 30 31 32 33 34 35
READLINK = $(shell if hash greadlink 2>/dev/null ; then echo greadlink ; else echo readlink ; fi)

# Path to CFML relative to immediate subfolders of $(CFML)/examples.
CFML := ../..

# Absolute path to CFML.
CFML := $(shell $(READLINK) -f $(CFML))

# Include any local settings.
-include $(CFML)/settings.sh
charguer's avatar
charguer committed
36 37

ifndef ML
charguer's avatar
charguer committed
38
   ML := $(filter-out myocamlbuild.ml,$(shell ls *.ml))
charguer's avatar
charguer committed
39 40
endif

charguer's avatar
more  
charguer committed
41
ifndef ML_MAIN
charguer's avatar
charguer committed
42
   ML_MAIN := $(ML)
charguer's avatar
more  
charguer committed
43 44
endif

charguer's avatar
charguer committed
45 46 47
ifndef V
   V := $(wildcard *.v)
endif
charguer's avatar
more  
charguer committed
48

charguer's avatar
charguer committed
49 50
ifdef V_IGNORED
   V := $(filter-out $(V_IGNORED),$(V))
charguer's avatar
charguer committed
51 52
endif

charguer's avatar
charguer committed
53
ifndef COQINCLUDE
charguer's avatar
charguer committed
54
   COQINCLUDE := -R $(CFML)/lib/coq CFML -R $(CFML)/lib/tlc TLC -R $(CFML)/lib/stdlib/ STDLIB -R . EXAMPLE
charguer's avatar
charguer committed
55 56
endif

POTTIER Francois's avatar
POTTIER Francois committed
57 58 59
OCAMLBUILD := \
  $(OCAMLBIN)ocamlbuild \
    -I ocamllib \
charguer's avatar
demos  
charguer committed
60
    -classic-display -use-ocamlfind -cflags "-g" -lflags "-g" -X ocamllib -X .coq-native \
POTTIER Francois's avatar
POTTIER Francois committed
61
    $(OCAMLBUILD_FLAGS) \
charguer's avatar
charguer committed
62 63


charguer's avatar
open  
charguer committed
64
##############################################################
charguer's avatar
charguer committed
65
# Targets
charguer's avatar
open  
charguer committed
66

charguer's avatar
charguer committed
67 68
all:  cf proof  
# code => excluded cause does not work yet
charguer's avatar
open  
charguer committed
69

charguer's avatar
fix  
charguer committed
70 71
nocode: cf proof

charguer's avatar
charguer committed
72
# Targets coming from Makefile.coq: 
charguer's avatar
fixes  
charguer committed
73
#   quick, proof, proof_vo
charguer's avatar
open  
charguer committed
74 75


charguer's avatar
charguer committed
76
##############################################################
charguer's avatar
charguer committed
77
# Code compilation
charguer's avatar
charguer committed
78

POTTIER Francois's avatar
POTTIER Francois committed
79 80 81 82 83
# ocamlbuild refuses -I $(CFML)/lib/ocaml (either in relative or absolute form!).
# It accepts only "implicit" paths (which begin with none of ".", "..", "/").
# We have to create a symbolic link "ocamllib" so as to make it happy.
# A better solution would be not to use this -I directive at all.

charguer's avatar
charguer committed
84 85
ocamllib:
	ln -s $(CFML)/lib/ocaml ocamllib
charguer's avatar
charguer committed
86

charguer's avatar
charguer committed
87 88
code: ocamllib $(ML)
	$(OCAMLBUILD) $(ML_MAIN:.ml=.native)
charguer's avatar
charguer committed
89 90 91 92 93


##############################################################
# Characteristic formula generation

charguer's avatar
cp  
charguer committed
94 95
ifndef CFDEBUG

charguer's avatar
charguer committed
96
cf: $(ML)
97 98 99
# Make sure TLC and CFML itself are up-to-date.
# Needed only when developing TLC and CFML. Ideally, should be removed.
	@$(MAKE) -C $(CFML)/lib/tlc --no-print-directory quick
charguer's avatar
PRE  
charguer committed
100 101
#	@$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick_cf 
	@$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick 
charguer's avatar
charguer committed
102
	@$(MAKE) -C $(CFML)/lib/stdlib --no-print-directory quick
charguer's avatar
charguer committed
103
	@$(MAKE) CFML=$(CFML) OCAML_FLAGS=$(OCAML_FLAGS) COQINCLUDE="$(COQINCLUDE)" ML="$(ML)" --no-print-directory -f $(CFML)/lib/make/Makefile.cf all
charguer's avatar
charguer committed
104

charguer's avatar
cp  
charguer committed
105 106 107 108
else

#----------------FOR DIRECT TEST----------------------

charguer's avatar
charguer committed
109 110 111
#-strict_value_restriction
EXTRA= -only_normalize -debug

charguer's avatar
cp  
charguer committed
112 113 114 115 116
cf: $(ML)
	@$(MAKE) -C $(CFML)/lib/tlc --no-print-directory quick
	@$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick_cf 
#	@$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick 
	@$(MAKE) -C $(CFML)/lib/stdlib CFDEBUG=$(CFDEBUG) --no-print-directory cmj
charguer's avatar
charguer committed
117
	@$(MAKE) CFML=$(CFML) EXTRA="$(EXTRA)" OCAML_FLAGS="$(OCAML_FLAGS)" COQINCLUDE="$(COQINCLUDE)" ML="$(ML)" --no-print-directory -f $(CFML)/lib/make/Makefile.cf all
charguer's avatar
cp  
charguer committed
118 119 120 121 122

endif



charguer's avatar
charguer committed
123 124
proof:cf

charguer's avatar
charguer committed
125 126

##############################################################
charguer's avatar
fixes  
charguer committed
127
# Rules
charguer's avatar
working  
charguer committed
128 129 130 131

# ===> todo: need to force make in cf before coq files may be compiled
# VD := $(patsubst %.v,%.v.d,$(V) $(wildcard $(CFML)/lib/coq/*.v.d) $(wildcard $(CFML)/lib/tlc/*.v.d))

charguer's avatar
charguer committed
132

charguer's avatar
charguer committed
133
include $(CFML)/lib/make/Makefile.coq
charguer's avatar
charguer committed
134 135 136 137 138


##############################################################
# Cleanup

charguer's avatar
sieve  
charguer committed
139 140 141 142
# Do not delete intermediate files.
.SECONDARY:
.PRECIOUS: *.vio

charguer's avatar
charguer committed
143
clean::
POTTIER Francois's avatar
POTTIER Francois committed
144
	rm -rf _build *.native ocamllib
charguer's avatar
working  
charguer committed
145
	@make CFML=$(CFML) -f $(CFML)/lib/make/Makefile.cf clean
charguer's avatar
charguer committed
146 147