Commit 63a4201f authored by POTTIER Francois's avatar POTTIER Francois
Browse files

A lot of Makefile hacking.

Several Makefiles and scripts now installed in $(CFML)/lib/make.
parent 7a23d090
# A new master Makefile for the components of CFML.
.PHONY: all install
.PHONY: all clean install
# ------------------------------------------------------------------------------
......@@ -15,6 +15,10 @@ all:
# Compile the Coq theory.
make -C lib/coq -j
make -C generator $@
make -C lib/coq $@
# ------------------------------------------------------------------------------
# We install:
......@@ -22,6 +26,7 @@ all:
# 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
......@@ -53,10 +58,12 @@ install: all
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 Successfully installed.
@echo Please use the following definition in your projects:
@echo CFML = $(shell cd $(PREFIX) && pwd)
# We assume that CFML has not necessarily been installed.
# Find Makefile.tlc.
ROOT := $(shell while ! [ -f ./Makefile.tlc ] ; do cd .. ; done && pwd)
......@@ -6,5 +8,5 @@ include $(ROOT)/Makefile.tlc
# Compile.
include $(ROOT)/Makefile.coq
include $(ROOT)/lib/make/Makefile.coq
# This is
# We assume we are in a cf/ subdirectory.
# We assume $(CFML) is defined.
# Our job is to ensure that the OCaml code is well-typed and
# create a read-only copy of it in ./_stub. Then, we hand
# control off to
.PHONY: all clean
CODE := ../src
STUB := _stub
# We assume all .ml files in the directory $(CODE) should be
# copied (except This can be overridden by
# defining ML externally.
# We assume ML is a list of unqualified file names, which we
# interpret relative to the directory $(CODE).
ifndef ML
ML := $(filter-out,$(shell cd $(CODE) && ls *.ml))
# First, make sure the OCaml code is correct and compiled.
@make --no-print-directory -C $(CODE)
# Create the subdirectory _stub.
# Intentionally do not delete it if it exists already (it
# might contain valid compiled files, which we wish to keep).
@mkdir -p $(STUB)
# Remove any leftover .ml files in _stub.
@rm -f $(STUB)/*.ml
# Copy the .ml files to _stub.
# Do not copy the .mli files, which cause trouble with CFML.
# Use cp -a so as to keep the file modification dates.
@for f in $(ML) ; do \
cp -a $(CODE)/$$f $(STUB) ; \
# Make the copy read-only to avoid mistakes.
@chmod a-w $(STUB)/*.ml
# Then, invoke the second Makefile.
@make CFML=$(CFML) --no-print-directory -f $(CFML)/lib/make/ -j $@
@make CFML=$(CFML) --no-print-directory -f $(CFML)/lib/make/ $@
# This is, which runs behind
# We assume we are in a cf/ subdirectory.
# We assume $(CFML) is defined.
# We assume the code has been copied to the subdirectory _stub.
# There, we find the files
# In _stub, we create:
# - the files %.d (dependency files)
# - the files %.cmj (type information; .cmi files in disguise)
# In the current directory, we create:
# - the files %_ml.v (characteristic formulae)
# - the files %_ml.vo (compiled characteristic formulae)
# Idea/hack number 1:
# Because the CFML generator produces the files %_ml.v and %.cmj at
# the same time (in just one invocation), it is not necessary to
# tell "make" about both of these files. We adopt the convention
# that only the .cmj file is used as a target. This seems to help.
# Idea/hack number 2:
# If we must wait until the files %_ml.v are generated before we can
# run coqdep to find out about the dependencies, this is too late, or
# at least too complicated for "make" or for me. We avoid the problem
# by re-using the dependency information produced by ocamldep. After
# all, the dependencies between modules are the same at the OCaml level
# and at the Coq level, so we don't need to run coqdep at all. In one
# run of ocamldep, we generate at the same time the dependencies at the
# OCaml level and at the Coq level.
# ------------------------------------------------------------------------------
COQINCLUDE:= -I $(CFML)/lib/coq -I $(CFML)/lib/tlc
# ------------------------------------------------------------------------------
# The CFML generator.
GENERATOR := $(CFML)/bin/cfml
# The name of the directory _stub.
STUB := _stub
# Standard tools.
OCAMLDEP := ocamldep
COQC := coqc
# Extra scripts.
OCAMLPOST := $(CFML)/lib/make/
# ------------------------------------------------------------------------------
# The OCaml source files.
ML := $(shell cd $(STUB) && ls *.ml)
# The Coq files that we produce.
MLV := $(patsubst,%_ml.v,$(ML))
# The compiled Coq files.
MLVO := $(patsubst,%_ml.vo,$(ML))
# The dependency files.
D := $(patsubst,$(STUB)/%.d,$(ML))
.PHONY: all clean
# Do not delete intermediate files.
# ------------------------------------------------------------------------------
# The goal is to produce the compiled Coq files.
all: $(MLVO)
# Cleaning up.
rm -f *_ml.v *.vo *.glob
rm -rf $(STUB)
# ------------------------------------------------------------------------------
# As described by the recipe below, including the dependency files $(D)
# adds dependencies of the form:
# _stub/A.cmj: _stub/B.cmj
# A_ml.vo: B_ml.vo
# whenever module A depends on module B.
ifeq ($(findstring $(MAKECMDGOALS),clean),)
-include $(D)
$(STUB)/%.d: $(STUB)/
# We use ocamldep -modules to find out which modules A depends upon.
# (An advantage of ocamldep -modules is that its output does not
# depend on the presence or absence of certain .mli files.)
# (A disadvantage of ocamldep -modules is that does not filter
# out the standard library modules.)
# We use the script $(OCAMLPOST) to post-process the output of ocamldep
# and filter out the standard library modules.
@for B in `$(OCAMLDEP) -modules $< | CFML=$(CFML) $(OCAMLPOST)` ; do \
echo $(STUB)/$*.cmj: $(STUB)/$${B}.cmj ; \
echo $*_ml.vo: $${B}_ml.vo ; \
done > $@
# ------------------------------------------------------------------------------
# The generator produces %_ml.v and %.cmj file out of
# Only the %.cmj target is known to "make".
# The target %_ml.v is generated in _stub; we move it up.
@mv -f $*_ml.v .
# ------------------------------------------------------------------------------
# Coq produces a .vo file out of a .v file.
# We declare a dependency on the .cmj file, since %_ml.v is not known to "make".
%_ml.vo: $(STUB)/%.cmj
$(COQC) $(COQINCLUDE) $*_ml.v
#!/usr/bin/env ocaml
#load "str.cma"
(* This script reads one line produced by [ocamldep -modules] and echoes a
list (one per line) of the dependencies which are not standard library
modules. The environment variable $CFML must be defined, and the standard
library directory is assumed to be $CFML/lib/ocaml. *)
let warning msg =
Printf.fprintf stderr "%s: warning: %s.\n" Sys.argv.(0) msg;
flush stderr
let assert_end_of_stdin () =
let (_ : string) = input_line stdin in
warning "more than one line of input"
with End_of_file ->
let read_exactly_one_line () =
let line = input_line stdin in
let colon =
Str.regexp ":"
let whitespace =
Str.regexp "[ \t]+"
let dependencies (line : string) : string list =
(* Look for the colon, and move past it. *)
let (ofs : int) = Str.search_forward colon line 0 in
(* Extract the words on the remainder of the line. *)
Str.split whitespace (Str.string_after line (ofs + 1))
with Not_found ->
warning "did not find colon in input";
let is_stdlib_module (m : string) =
let m = String.uncapitalize m in
let cfml = Sys.getenv "CFML" in
Sys.file_exists (cfml ^ "/lib/ocaml/" ^ m ^ ".cmj")
with Not_found ->
warning "CFML is undefined";
let is_user_module (m : string) =
not (is_stdlib_module m)
let () =
(* There should be exactly one line of input. *)
let line = read_exactly_one_line() in
(* We expect the input to have been produced by [ocamldep -modules].
It should be of the form [ Bar Baz Quux]. *)
let modules = dependencies line in
(* Keep only the modules which are user modules. *)
let modules = List.filter is_user_module modules in
(* Echo a list of them. *)
List.iter print_endline modules;
flush stdout
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