Commit 8ec95c50 authored by charguer's avatar charguer
Browse files

compilation

parent 31aae4a8
......@@ -12,10 +12,14 @@ include Makefile.tlc
# ------------------------------------------------------------------------------
all:
all: cfmlgenerator cfmllib
# Compile the generator.
cfmlgenerator:
make -C generator
# Compile the Coq theory.
cfmllib:
make -C lib/coq -j
clean:
......@@ -72,6 +76,12 @@ install: all
# ------------------------------------------------------------------------------
demos:
make -C examples
# ------------------------------------------------------------------------------
# For README.html:
%.html: %.md
......
(*---------simple record------------*)
type 'a myrec = {
......
Set Implicit Arguments.
Require Import CFLib LibInt LibWf Facts Demo_ml.
Require Import CFLib LibInt LibWf (*Facts*) Demo_ml.
(*************************************************************************)
(* If demo *)
......@@ -203,6 +203,10 @@ Proof.
Qed.
(*************************************************************************)
(*************************************************************************)
(*
(*************************************************************************)
......
include ../Makefile.example
EXAMPLE_DIRS=\
BasicDemos
# References
default: all
$(EXAMPLE_DIRS)::
$(MAKE) -C $@ $(MAKECMDGOALS)
all clean : $(EXAMPLE_DIRS)
# if (m = "Array.cmj" || m = "List.cmj") then true else
# in Makefile.cf.2
#COQINCLUDE:= -R $(CFML)/lib/coq CFML -R $(TLC) TLC
#GENERATOR := $(CFML)/local/bin/cfml
# ================ TODO: how to make ocamlbuild happy with MLINCLUDE??
# MLINCLUDE := -I $(CFML)/lib/ocaml/
# The environment variable $CFML must be defined, and the standard
# library directory is assumed to be $CFML/local/lib/ocaml.
.PHONY: all code cf proof clean
##############################################################
# Configuration
OCAMLBIN=
COQBIN=
CFML := ../../
-include $(CFML)/settings.sh
STUB := _stub
# TODO: $(STUB) should be passed to the script Makefile.cf.2
##############################################################
# Default target files
ifndef ML_MAIN
ML_MAIN := main
endif
ifndef ML
# ML := $(wildcard *.ml)
ML := $(filter-out myocamlbuild.ml,$(shell ls *.ml))
endif
ifndef PREFIX
PREFIX := $(CFML)/local
endif
ifndef TLC
TLC := $(PREFIX)/lib/tlc/
endif
##############################################################
# Program compilation
OCAMLBUILD := $(OCAMLBIN)ocamlbuild
OCAMLBUILD_WITH_OPTIONS := $(OCAMLBUILD) -classic-display -use-ocamlfind -cflags "-g" -lflags "-g"
%.native: $(ML)
$(OCAMLBUILD_WITH_OPTIONS) $(basename $<).native
code: $(ML_MAIN).native
##############################################################
# Characteristic formula generation
## TODO: factorize better with $(CFML)/lib/make/Makefile.cf.1
## TODO: could require the code to typecheck before generating cf,
# or we may disable it in order to avoid the call to ocamlbuild
cf: $(ML)
@echo "Setting up characteristic formula files"
@mkdir -p $(STUB)
@rm -f $(STUB)/*.ml
@for f in $(ML) ; do \
cp -a $$f $(STUB) ; \
done
@chmod a-w $(STUB)/*.ml
@make COQBIN=$(COQBIN) CFML=$(CFML) --no-print-directory -f $(CFML)/lib/make/Makefile.cf.2 -j all
test:
echo $(TLC)
test2:
@make CFML=$(CFML) --no-print-directory -f $(CFML)/lib/make/Makefile.cf.2 -j test
cf_old: $(ML)
# 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 $$f $(STUB) ; \
done
# Make the copy read-only to avoid mistakes.
@chmod a-w $(STUB)/*.ml
# Then, invoke the second Makefile.
@make CFML=$(CFML) TLC=$(TLC) --no-print-directory -f $(CFML)/lib/make/Makefile.cf.2 -j $@
##############################################################
# Verification proof
COQINCLUDE := -R $(CFML)/lib/coq CFML -R $(TLC) TLC -I .
#include $(CFML)/lib/make/Makefile.coq
# TODO: better factorized
COQC := $(COQBIN)coqc
COQDEP := $(COQBIN)coqdep
COQIDE := $(COQBIN)coqide
V := $(wildcard *.v)
VO := $(patsubst %.v,%.vo,$(V))
VIO := $(patsubst %.v,%.vio,$(V))
VD := $(patsubst %.v,%.v.d,$(V))
proof: cf $(VO)
quick: cf $(VIO)
ifeq ($(findstring $(MAKECMDGOALS),clean),)
-include $(VD)
endif
%.v.d: %.v
@$(COQDEP) $(COQINCLUDE) -I . $< > $@
%.vo: %.v
$(COQC) $(COQINCLUDE) -I . $<
%.vio: %.v
$(COQC) -quick $(COQINCLUDE) -I . $<
##############################################################
# ALL
all: proof
##############################################################
# Cleanup
clean:
rm -rf _build *.native
rm -f *.cmj
rm -rf output *_ml.v
rm -f *.v.d *.vio *.vo *.glob
rm -rf $(STUB)
include ../Makefile.example
# This is Makefile.cf.2, which runs behind Makefile.cf.1.
# This is Makefile.cf.2, which runs behind Makefile.cf.1.
# We assume we are in a cf/ subdirectory.
......@@ -33,12 +33,14 @@
# ------------------------------------------------------------------------------
COQINCLUDE:= -R $(CFML)/lib/coq CFML -R $(TLC) TLC
PREFIX := $(CFML)/local
COQINCLUDE:= -R $(PREFIX)/lib/coq/ CFML -R $(PREFIX)/lib/tlc/ TLC
# ------------------------------------------------------------------------------
# The CFML generator.
GENERATOR := $(CFML)/bin/cfml
# The CFML generator.
GENERATOR := $(CFML)/local/bin/cfml
# The name of the directory _stub.
STUB := _stub
......@@ -69,6 +71,7 @@ D := $(patsubst %.ml,$(STUB)/%.d,$(ML))
# ------------------------------------------------------------------------------
# The goal is to produce the compiled Coq files.
all: $(MLVO)
......@@ -88,6 +91,11 @@ ifeq ($(findstring $(MAKECMDGOALS),clean),)
-include $(D)
endif
test:
@for B in `$(OCAMLDEP) -modules _stub/Demo.ml | CFML=$(CFML) $(OCAMLPOST)` ; do echo $(STUB)/$*.cmj: $(STUB)/$${B}.cmj; done
$(STUB)/%.d: $(STUB)/%.ml
# We use ocamldep -modules to find out which modules A depends upon.
# (An advantage of ocamldep -modules is that its output does not
......
......@@ -4,7 +4,7 @@
(* 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. *)
library directory is assumed to be $CFML/local/lib/ocaml. *)
let warning msg =
Printf.fprintf stderr "%s: warning: %s.\n" Sys.argv.(0) msg;
......@@ -39,10 +39,11 @@ let dependencies (line : string) : string list =
[]
let is_stdlib_module (m : string) =
if (m = "Array.cmj" || m = "List.cmj") then true else
let m = String.uncapitalize m in
try
let cfml = Sys.getenv "CFML" in
Sys.file_exists (cfml ^ "/lib/ocaml/" ^ m ^ ".cmj")
Sys.file_exists (cfml ^ "/local/lib/ocaml/" ^ m ^ ".cmj")
with Not_found ->
warning "CFML is undefined";
false
......
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