Commit 31aae4a8 authored by charguer's avatar charguer
Browse files

compile_lib

parent 8aa8a82c
# A new master Makefile for the components of CFML.
.PHONY: all clean install
# ------------------------------------------------------------------------------
# This defines TLC.
include Makefile.tlc
# ------------------------------------------------------------------------------
all:
# Compile the generator.
make -C generator
# Compile the Coq theory.
make -C lib/coq -j
clean:
make -C generator $@
make -C lib/coq $@
# ------------------------------------------------------------------------------
# We install:
# the executable in $(PREFIX)/bin
# the Coq library in $(PREFIX)/lib/coq
# the OCaml library in $(PREFIX)/lib/ocaml
# a symlink to TLC as $(PREFIX)/lib/tlc
# various Makefiles in $(PREFIX)/lib/make
ifndef PREFIX
# TEMPORARY
PREFIX := local
endif
PWD := $(shell pwd)
MLI := $(filter-out generator/stdlib/camlinternal% \
%genlex.mli %moreLabels.mli %oo.mli, \
$(wildcard generator/stdlib/*.mli)) \
$(wildcard camllib/*.mli)
MAKECMJ := $(PWD)/generator/makecmj.native
MYOCAMLDEP := $(PWD)/generator/myocamldep.native
install: all
rm -rf $(PREFIX)
# Copy the executable.
mkdir -p $(PREFIX)/bin
cp generator/main.native $(PREFIX)/bin/cfml
# Copy the Coq theory.
mkdir -p $(PREFIX)/lib
cp -r lib/coq $(PREFIX)/lib
cd $(PREFIX)/lib/coq && rm -f Makefile *.v.d *.glob
# Copy the OCaml standard library (plus additions) and compile it.
mkdir -p $(PREFIX)/lib/ocaml
cp -r $(MLI) $(PREFIX)/lib/ocaml
cp Makefile.camllib $(PREFIX)/lib/ocaml/Makefile
make MAKECMJ=$(MAKECMJ) MYOCAMLDEP=$(MYOCAMLDEP) -C $(PREFIX)/lib/ocaml
cd $(PREFIX)/lib/ocaml && rm -f .depend Makefile
# Install a symlink to TLC, since we know where it is.
ln -s $(TLC) $(PREFIX)/lib/tlc
# Install various Makefiles and scripts.
cp -r lib/make $(PREFIX)/lib
# Success.
@echo Successfully installed.
# Tell the user where we installed. This somewhat convoluted incantation is
# supposed to produce an absolute path even if $(PREFIX) is a relative path.
@echo Please use the following definition in your projects:
@echo CFML = $(shell cd $(PREFIX) && pwd)
# ------------------------------------------------------------------------------
# For README.html:
%.html: %.md
pandoc -o $@ $<
############################################################################
# You can define your own path to COQBIN, to CAMLBIN, and to TLC by
# creating a file called "settings.sh" and placing the right definitions
# into it, e.g.
#
# TLC=~/tlc/trunk
# COQBIN=/var/tmp/coq-8.3pl2/bin/
# CAMLBIN=
#
# Note that TLC should have no leading slash, whereas COQBIN and CAMLBIN
# should have one if they are not empty.
# Note that if you rebind COQBIN you need to do the same in the TLC folder.
# Note that if you add a settings.sh file, you will need to do "make depend".
# A new master Makefile for the components of CFML.
# Default paths are as follows:
.PHONY: all clean install
TLC=tlc
COQBIN=
CAMLBIN=
# ------------------------------------------------------------------------------
# This allows to assign path to TLC and to COQBIN
-include settings.sh
# Additional options that may be provided in settings.sh:
# - to prevent automatic recompilation of files on changes on TLC sources, add:
# NO_DEPENDENCIES_TLC=1
# This defines TLC.
include Makefile.tlc
# ------------------------------------------------------------------------------
############################################################################
############################################################################
# Sanity checks: make sure that 'make init' and 'make depend' have already been run
all:
# Compile the generator.
make -C generator
# Compile the Coq theory.
make -C lib/coq -j
# Commands
clean:
make -C generator $@
make -C lib/coq $@
CLEANCMD=clean clean_files clean_tools
DEPENDFIRST=
INITFIRST=
# ------------------------------------------------------------------------------
# Generate an error if there is the 'camllib/*.mli' files do not seem
# to be present and the target is not 'camllibsrc' or 'init' or 'clean*'
# We install:
# the executable in $(PREFIX)/bin
# the Coq library in $(PREFIX)/lib/coq
# the OCaml library in $(PREFIX)/lib/ocaml
# a symlink to TLC as $(PREFIX)/lib/tlc
# various Makefiles in $(PREFIX)/lib/make
ifeq ($(findstring camllib/pervasives.mli, $(wildcard camllib/*.mli)),)
ifeq ($(findstring $(MAKECMDGOALS),init camllibsrc $(CLEANCMD)),)
INITFIRST=initfirst
ifndef PREFIX
# TEMPORARY
PREFIX := local
endif
endif
# Generate an error if there is no 'depend' file and the target
# is not 'depend' nor 'init' nor nor 'camllibsrc' or 'clean*'
# (provided the error INITFIRST has not yet been triggered)
ifeq ($(INITFIRST),)
ifeq ($(findstring depend, $(wildcard depend)),)
ifeq ($(findstring $(MAKECMDGOALS),depend init camllibsrc $(CLEANCMD)),)
DEPENDFIRST=dependfirst
endif
endif
endif
############################################################################
############################################################################
# Filenames
# Files under developments in the imper/ folder
DEV=\
# Files under developments in the user/ folder
USER=\
user/DynArray \
user/Facto \
user/FQueue \
user/Demo
# Stable developments
IMPER=\
imper/ChunkedSeqDev \
imper/Compose \
imper/Swap \
imper/MutableList \
imper/Counter \
imper/Dijkstra \
imper/SparseArray \
imper/UnionFind \
imper/Fixpoint \
imper/BinarySearchTree \
imper/DFS \
imper/SequenceSig \
imper/CapacitySig \
imper/ReducerSig \
imper/FingerTree \
imper/Dom \
# Developments that do not compile currently
MORE=\
imper/BatchedQueue \
imper/SchurConjugate \
imper/Landin \
imper/Facto \
imper/FunctionalList \
imper/InOut \
imper/StrongUpdate \
imper/TreeCopy \
imper/LambdaByte \
imper/LambdaEval \
imper/Loops \
imper/BootSimpleChunkedSeq \
# Developments to be removed
DEPRECATED=\
imper/InhabTypeSig \
imper/CapacitySig \
imper/FastFingerTree
# Auxiliary Coq files to include in the computation of dependencies
AUX=\
imper/Common_proof \
imper/MinInf \
user/Facts \
user/FactsCredits \
user/DynArrayNoCredits_proof
############################################################################
# Source scripts of the CFML library
CFLIB=\
Shared \
CFHeaps \
CFSpec \
CFPrint \
CFTactics \
CFPrim \
CFRep \
CFCredits \
CFLib \
CFLibCredits
# Generator tools # TODO: rename programs
GENERATOR=./main.byte
MYOCAMLCMJ=./makecmj.byte
MYOCAMLDEP=./myocamldep.byte
# External tools
COQC=$(COQBIN)coqc -dont-load-proofs
COQDEP=$(COQBIN)coqdep
COQDOC=$(COQBIN)coqdoc
OCAMLBUILD=$(OCAMLBIN)ocamlbuild
OCAMLDEPWRAPPER=ocamldep.wrapper
OPENSCRIPT=open.sh
# Paths to include
INCLUDES=-I . -I camllib -I ./imper -I ./user -I $(TLC)
# Files for which _ml.v dependencies need to be computed
ML_SRC=$(TEMP) $(USER) $(IMPER)
############################################################################
############################################################################
# Static and dynamic dependencies
# Dependencies on the TLC library
TLC_SRC=$(wildcard $(TLC)/*.v)
TLC_VO=$(TLC_SRC:.v=.vo)
# Dependencies on the source code of the generator
CAML_FILES_IN=$(addprefix $(1)/,*.ml *.mli *.mll *.mly)
MAP=$(foreach a,$(2),$(call $(1),$(a)))
GENERATOR_SUBDIRS=lex parsing typing tools utils
GENERATOR_DIRS=gen $(addprefix gen/,$(GENERATOR_SUBDIRS))
GENERATOR_PATTERNS=$(call MAP, CAML_FILES_IN, $(GENERATOR_DIRS))
GENERATOR_SRC=$(wildcard $(GENERATOR_PATTERNS))
# Dependencies on the executables of the generator
MYTOOLS=$(GENERATOR) $(MYOCAMLCMJ) $(MYOCAMLDEP)
# Dependencies on the source code of the (extended) standard Caml library
CAMLLIB_MLI_PATH=$(filter-out gen/stdlib/camlinternal% %genlex.mli %moreLabels.mli %oo.mli, $(wildcard gen/stdlib/*.mli))
CAMLLIB_MLI=$(patsubst gen/stdlib/%,%,$(CAMLLIB_MLI_PATH))
CAMLLIB_CMJ=$(addprefix camllib/,$(CAMLLIB_MLI:.mli=.cmj))
EXTENDED_INTERFACES=\
camllib/NullPointers \
camllib/StrongPointers
SHARED_CMJ=$(CAMLLIB_CMJ) $(EXTENDED_INTERFACES:=.cmj)
OKASAKI_INTERFACES=\
okasaki/Okasaki \
okasaki/OkaStream
OKASAKI_CMJ=$(OKASAKI_INTERFACES:=.cmj)
# List of all dynamic dependency files
ifeq ($(NO_DEPENDENCIES_TLC),)
DEPENDENCIES_TLC=$(TLC_SRC:.v=.v.d)
else
DEPENDENCIES_TLC=
endif
DEPENDENCIES=$(CFLIB:=.v.d) $(ML_SRC:=.ml.d) $(ML_SRC:=_ml.v.d) $(ML_SRC:=_proof.v.d) $(AUX:=.v.d) $(DEPENDENCIES_TLC)
############################################################################
############################################################################
# Targets and intermediate targets
# Declare the complete list of special targets
.PHONY: all dependfirst initfirst depend tools cf camllib camllibsrc cf mlv mlvo dev clean clean clean_files clean_tools test contrib
# Declare the file extensions and declare intermediate files as precious
.SUFFIXES: .cmj .cmk .byte .ml .ml.d .v .v.d .vo _ml.v _ml.v.d _ml.vo _proof.v _proof.vo
.INTERMEDIATE: %.cmj %.cmk %.byte %.ml.d %.v.d %.vo %_ml.v %_ml.v.d %_ml.vo %_proof.vo
.PRECIOUS: %.cmj %.cmk %.byte %.ml.d %.v.d %.vo %_ml.v %_ml.v.d %_ml.vo %_proof.vo
############################################################################
############################################################################
# Execution of "make all"
all: $(INITFIRST) $(DEPENDFIRST) tools tlc cf imper
initfirst:
@echo you need to first call make init
@exit 1
dependfirst:
@echo you need to first call make depend
@exit 1
############################################################################
############################################################################
# Initialization: making a copy of Caml standard library
init: camllibsrc
@chmod +x $(OCAMLDEPWRAPPER)
@chmod +x $(OPENSCRIPT)
@echo MAKE INIT SUCCESSFUL: YOU MAY NOW RUN 'make -C tlc all', and then 'make depend'
camllibsrc:
@$(foreach file, $(CAMLLIB_MLI), cp gen/stdlib/$(file) camllib/; )
@echo camllib source files successfully copied
############################################################################
############################################################################
# DETAILED TARGETS
# Compilation of the characteristic formula generator
tools: $(MYTOOLS)
# Compilation of the standard Caml library
camllib: $(SHARED_CMJ)
# Generation of all the characteristic formulae files
mlv: $(ML_SRC:=_ml.v)
# Compilation of all the characteristic formulae files
mlvo: $(ML_SRC:=_ml.vo)
# Compilation of the CFML library
cf: $(CFLIB:=.vo)
# Compilation of the TLC library
tlclib:
echo $(TLC)
make -C $(TLC) all
# Compilation of all the proofs in development
dev: $(DEV:=_proof.vo)
# Compilation of all the proofs in /imper
imper: $(IMPER:=_proof.vo)
# Compilation of all the proofs in /user
user: $(USER:=_proof.vo)
# Compilation of characteristic formulae files in /user
user_mlvo: $(USER:=_ml.vo)
# Generation of all the dependency files (includes the generation of _ml.v files)
depend: $(DEPENDENCIES)
@touch depend
@echo MAKE DEPEND SUCCESSFUL: YOU MAY NOW RUN MAKE
# Compilation of the contributions. A separate Makefile is used.
contrib: tools camllib cf tlc
make -C contrib
############################################################################
############################################################################
# Computation of dependencies
# The rules for generating %.d files are only included when the goal is 'depend'
ifeq ($(findstring $(MAKECMDGOALS),depend),depend)
# To generate the *.ml.d files, we add a dummy target
# to avoid having a *.cmk file that depends on no other file
# (TODO: should use a better 'sed' command to instead add the ml file as dependency,
# but the difficulty is to escape the slashes that appear in the filename $<)
DUMMY_TARGET=dummy_target
%.ml.d: %.ml $(MYOCAMLDEP)
@echo $(MYOCAMLDEP) $(INCLUDES) $<
@$(MYOCAMLDEP) $(INCLUDES) $< | sed 's/:/: $(DUMMY_TARGET)/' > $@
# To generate *.v.d, we use the ocaml-wrapper trick to
# force dependencies to mention files that do not exist yet
%.v.d: %.v
@echo $(COQDEP) $(INCLUDES) $< > $@
@./$(OCAMLDEPWRAPPER) $(ML_SRC:=_ml.v) - $(COQDEP) $(INCLUDES) $< > $@
endif
dummy_target:
touch $@
############################################################################
############################################################################
# Include of dependency files
# Mycamldep generates dependencies over .cmk files (which are dynamically
# included in this makefile). The generation of an empty %.cmk files is
# used to indicate that the corresponding %_ml.v is ready to be generated.
# Indeed, it captures the fact that all the source files used by the %.ml file
# have already be compiled into %.cmj files.
VERBOSE=
%.cmk: %.ml dummy_target $(GENERATOR) # %.cmj
@echo producing $@
$(GENERATOR) -onlycmj -rectypes $(INCLUDES) $<
$(VERBOSE)touch $@
# We include all dependencies, unless the target is 'init*' or 'depend' or 'clean*'
# TODO: this test isn't robust because if cmd is "all" and we have "clean_all"
# as another possible target, then it will be recognized by findstring...
ifeq ($(findstring $(MAKECMDGOALS),depend init camllibsrc $(CLEANCMD)),)
-include $(DEPENDENCIES)
endif
# When target is 'depend', we include only the .ml.d dependencies
ifeq ($(findstring $(MAKECMDGOALS),depend),depend)
-include $(ML_SRC:=.ml.d)
endif
############################################################################
############################################################################
# Compilation
# Construction of the generator programs
# (the Makefile does not handle well the the fact that ocamlbuild
# generaters symbolic links, so we need to move the binary file)
%.byte: $(GENERATOR_SRC)
@rm -f $@
$(OCAMLBUILD) -I gen $(addprefix -I ,$(GENERATOR_DIRS)) $@
@mv $@ temp.byte
@cp -L temp.byte $@
@rm temp.byte
# Compilation of a Coq file
%.vo: %.v
$(COQC) $(INCLUDES) $<
# Additional dependencies for the compilation of a characteristic formula Coq file
%_ml.vo: CFLib.vo
%_proof.vo: CFLib.vo
# Generation of a characteristic formula file;
# We force the %.cmk to exists, so as to ensure that we have
# already treated all the ml files that are dependencies of %.ml.
%_ml.v: %.ml %.cmk $(GENERATOR) $(SHARED_CMJ)
$(GENERATOR) -rectypes $(INCLUDES) $<
# Generation of a %.cmj file (could also use MYOCAMLCMJ)
# TODO: use a function to factorize
imper/%.cmj: imper/%.ml $(GENERATOR) $(SHARED_CMJ)
@echo producing $@
$(GENERATOR) -onlycmj -rectypes $(INCLUDES) $<
user/%.cmj: user/%.ml $(GENERATOR) $(SHARED_CMJ)
@echo producing $@
$(GENERATOR) -onlycmj -rectypes $(INCLUDES) $<
# Compilation of the .mli files from the Caml standard library
camllib/pervasives.cmj: camllib/pervasives.mli $(MYOCAMLCMJ)
$(MYOCAMLCMJ) -nostdlib -nopervasives $<
camllib/%.cmj: camllib/%.mli camllib/pervasives.cmj $(MYOCAMLCMJ)
$(MYOCAMLCMJ) -nostdlib -I camllib $<
# Compiling of the .mli files extending the Caml standard library
camllib/NullPointers.cmj: camllib/NullPointers.mli $(CAMLLIB_CMJ) $(MYOCAMLCMJ)
$(MYOCAMLCMJ) -rectypes -I camllib $<
camllib/StrongPointers.cmj: camllib/StrongPointers.mli $(CAMLLIB_CMJ) $(MYOCAMLCMJ)
$(MYOCAMLCMJ) -rectypes -I camllib $<
# why needed?
imper/SequenceSig_proof.vo: imper/SequenceSig_ml.vo
imper/ChunkedSeq_proof.vo: imper/ChunkedSeq_ml.vo imper/CapacitySig_ml.vo
imper/BootSimpleChunkedSeq_proof.vo: imper/BootSimpleChunkedSeq_ml.vo imper/CapacitySig_ml.vo imper/Common_proof.vo
# depedencies accross ML files
imper/FingerTree_ml.cmk: imper/ReducerSig.cmj
imper/FastFingerTree_ml.cmk: imper/ReducerSig.cmj imper/CapacitySig.cmj imper/FingerTree.cmj
imper/Counter.cmk: imper/MutableList.cmj
############################################################################
############################################################################
# Cleaning
# TODO: factorize better
clean_files:
@rm -f *.vo *.glob *.cmk *.cmj *_ml.v *.v.d *.ml.d || echo ok
@rm -f imper/*_ml.v imper/*.vo imper/*.glob imper/*.cmk imper/*.cmj imper/*.ml.d imper/*.v.d || echo ok
@rm -f user/*_ml.v user/*.vo user/*.glob user/*.cmk user/*.cmj user/*.ml.d user/*.v.d || echo ok
@rm -f okasaki/*_ml.v okasaki/*.vo okasaki/*.glob okasaki/*.cmk okasaki/*.cmj okasaki/*.ml.d okasaki/*.v.d || echo ok
@rm -f camllib/*.cmj camllib/*.d || echo ok
@rm -f depend || echo ok
@echo "CLEANED DEVELOPMENTS"
clean_tlc:
@rm -f $(TLC)/*.vo $(TLC)/*.glob $(TLC)/*.v.d || echo ok
clean_tools:
@rm -Rf _build || echo ok
@rm -f *.byte *.out || echo ok
@$(foreach file, $(CAMLLIB_MLI), rm -f camllib/$(file); )
@echo "CLEANED GENERATOR"
clean: clean_files clean_tools
# note that make clean does not clean subfolder tlc.
############################################################################
############################################################################
# Debugging
test:
@echo $(TLC)
@echo $(TLC_SRC)
@echo $(OCAMLBUILD)
@echo $(GENERATOR_DIRS)
@echo $(GENERATOR_PATTERNS)
@echo $(GENERATOR_SRC)
@echo $(CAMLLIB_MLI_PATH)
@echo $(SHARED_CMJ)
@echo $(DEPENDENCIES)
############################################################################
############################################################################
# TODO
# compute dependencies between the /gen/stdlib/*.mli files
# to avoid the filter-out
# use myocamlcmj instead to generate imper/%.cmj files
# integrate shadow compilation of .vo files
# integrate parallel make
# have go.sh include local_settings.sh
# use immediate errors instead of INITFIRST= and DEPENDFIRST=
# have MYTOOLS be compiled in a single execution of ocamlbuild
# why demo_ml.v is always rebuilt?
# why imper/*.cmj files are deleted automatically?
############################################################################
############################################################################
# DEPRECATED
# okasaki/%.cmj: okasaki/%.ml $(GENERATOR) $(SHARED_CMJ) $(OKASAKI_CMJ)
# $(GENERATOR) -onlycmj -rectypes $(INCLUDES) $<
# Compilation of the .mli files for Okasaki
# okasaki/Okasaki.cmj: okasaki/Okasaki.mli $(CAMLLIB_CMJ) $(MYOCAMLCMJ)
# $(MYOCAMLCMJ) -rectypes -I camllib $<
# okasaki/OkaStream.cmj: okasaki/OkaStream.mli $(CAMLLIB_CMJ) $(MYOCAMLCMJ) okasaki/Okasaki.cmj
# $(MYOCAMLCMJ) -rectypes -I camllib $<
# Compilation of sig files
#imper/ReducerSig.cmj: imper/ReducerSig.ml $(CAMLLIB_CMJ) $(MYOCAMLCMJ)
# $(MYOCAMLCMJ) -rectypes -I camllib -I imper $<
# Compilation of only proofs that works in /okasaki