Commit b9567bca authored by POTTIER Francois's avatar POTTIER Francois

Simplification of Makefile.example, assuming CFML is installed.

parent b9c38e20
##############################################################################
#
# This script is meant to be included by immediate subfolders of
# $(CFML)/examples.
# This Makefile is meant to be included by immediate subfolders of
# examples.
#
# We assume that CFML has been installed.
#
# Optionally, the variable $(ML) can be used to specify which sources
# to build characteristic formulae for.
......@@ -17,8 +19,8 @@
# Optionally, $(OCAML_FLAGS) can be set (e.g. to "-rectypes").
#
# Optionally, $(CFML_FLAGS) can be set (e.g. to "-debug").
#
# The file $(CFML)/settings.sh may define $(COQBIN).
CFML := $(shell cfmlc -where)
##############################################################################
......@@ -26,44 +28,22 @@
export
##############################################################################
# CFML setup.
# The variable TLC is used to find $(TLC)/Makefile.coq.
# Path to CFML relative to immediate subfolders of $(CFML)/examples.
CFML := ../..
include $(CFML)/Makefile.common
TLC := $(shell $(COQBIN)coqc -where)/user-contrib/TLC
##############################################################################
# Options for CFML.
# The line "-R $(TLC) TLC" is required only if we wish to write just
# "LibFoo", as opposed to "TLC.LibFoo". In the long run, I believe it
# would be preferable to explicitly use the TLC prefix.
PWD := $(shell pwd)
ifndef V
V := $(wildcard $(PWD)/*.v)
endif
# By default, V_AUX contains all of TLC and CFML libraries;
# additional files may be provided in the $(V_AUX_EXAMPLE) command.
ifndef V_AUX
V_AUX := \
$(wildcard $(TLC)/*.v) \
$(wildcard $(CFML)/lib/coq/*.v) \
$(wildcard $(CFML)/lib/stdlib/*.v) \
$(V_AUX_EXAMPLE)
endif
COQINCLUDE := \
-R $(TLC) TLC \
-R $(CFML)/lib/coq CFML \
-R $(CFML)/lib/stdlib STDLIB \
-R $(PWD) EXAMPLE
##############################################################################
# Options for OCaml.
......@@ -73,7 +53,6 @@ endif
ifndef OCAML_INCLUDE
OCAML_INCLUDE := \
-I $(CFML)/lib/stdlib \
-I $(PWD)
endif
......@@ -99,13 +78,9 @@ all:
# to proceed unless the previous phase was successful.
# 1. Compile the OCaml code.
@ $(OCAMLBUILD) $(ML_MAIN:.ml=.native)
# 2. Compile the characteristic formula generator.
@ $(MAKE) -C $(CFML)/generator
# 3. Compile the CFML library.
@ $(MAKE) -C $(CFML)/lib/stdlib
# 4. Build the characteristic formulae.
@ $(MAKE) --no-print-directory -f $(CFML)/lib/make/Makefile.cfml
# 5. Check the Coq proofs.
# 2. Build the characteristic formulae.
@ $(MAKE) --no-print-directory -f $(CFML)/make/Makefile.cfml
# 3. Check the Coq proofs.
# While we're at it, regenerate the _CoqProject file. (Optional.)
@ $(MAKE) -f $(TLC)/Makefile.coq _CoqProject proof
......@@ -114,6 +89,6 @@ all:
clean:
rm -rf _build *.native
@make CFML=$(CFML) -f $(CFML)/lib/make/Makefile.cfml $@
@make -f $(CFML)/make/Makefile.cfml $@
$(MAKE) -f $(TLC)/Makefile.coq $@
rm -f _CoqProject
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment