Commit d89b9e48 authored by charguer's avatar charguer

makeworks

parent 2caa6321
......@@ -10,21 +10,60 @@
# This defines TLC.
include Makefile.tlc
CFML := ./
# ------------------------------------------------------------------------------
PWD := $(shell pwd)
MLI_STDLIB := $(filter-out generator/stdlib/camlinternal% \
%genlex.mli %moreLabels.mli %oo.mli, \
$(wildcard generator/stdlib/*.mli))
MLI_ADDED := lib/ocaml/NullPointers.mli lib/ocaml/StrongPointers.mli
MLI := $(MLI_STDLIB) $(MLI_STDLIB)
MAKECMJ := $(PWD)/generator/makecmj.native
MYOCAMLDEP := $(PWD)/generator/myocamldep.native
ONEOCAMLLIBFILE := lib/ocaml/Array.mli
# ------------------------------------------------------------------------------
all: cfmlgenerator cfmllib
all: gen coqlib
# Compile the generator.
cfmlgenerator:
gen:
make -C generator
# Compile the Coq theory.
cfmllib:
coqlib:
make -C lib/coq -j
ocamllib:
make MAKECMJ=$(MAKECMJ) MYOCAMLDEP=$(MYOCAMLDEP) -C lib/ocaml
clean:
make -C generator $@
make -C lib/coq $@
@cd lib/ocaml && rm -f Makefile $(notdir $(MLI_STDLIB))
@echo "deleted ocamllib mli files"
make MAKECMJ=$(MAKECMJ) MYOCAMLDEP=$(MYOCAMLDEP) -C lib/ocaml $@
#*********arguments above should not be needed
# ------------------------------------------------------------------------------
init: gen
# Install a symlink to TLC, since we know where it is.
ln -f -s $(TLC) lib/tlc
# Copy the executable.
mkdir -p bin
cp generator/main.native bin/cfml
# Copy the OCaml standard library mli files
cp $(MLI_STDLIB) lib/ocaml
make MAKECMJ=$(MAKECMJ) MYOCAMLDEP=$(MYOCAMLDEP) -C lib/ocaml
# Success.
@echo Successfully initialized.
# ------------------------------------------------------------------------------
......@@ -40,14 +79,6 @@ ifndef PREFIX
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.
......@@ -58,9 +89,10 @@ install: all
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.
# *********TODO: compilation should be done by "make all"...
mkdir -p $(PREFIX)/lib/ocaml
cp -r $(MLI) $(PREFIX)/lib/ocaml
cp Makefile.camllib $(PREFIX)/lib/ocaml/Makefile
cp lib/ocaml/Makefile $(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.
......
let f x = x
\ No newline at end of file
val f : int -> int
Require Export CFLib Aux_ml.
Require Import Extra.
Lemma f_spec :
Spec f (x:int) |R>> R [] (fun y => [same x y]).
Proof.
xcf. intros. xret. unfold same. hsimpl~.
Qed.
Hint Extern 1 (RegisterSpec f) => Provide f_spec.
Require Import LibCore LibInt.
Definition same (x y : int) := (x = y).
open Aux (* required for cfml to do the require in Coq, in the current implementation *)
let g x = Aux.f x
\ No newline at end of file
Require Export CFLib Main_ml.
Require Import Aux_ml Aux_proof Extra.
Lemma g_spec :
Spec g (x:int) |R>> R [] (fun y => [same x y]).
Proof.
xcf. intros. xapp. hsimpl~.
Qed.
Hint Extern 1 (RegisterSpec g) => Provide g_spec.
include ../Makefile.example
\ No newline at end of file
EXAMPLE_DIRS=\
BasicDemos
DemoMake
# BasicDemos
# References
......
......@@ -25,11 +25,6 @@ CFML := ../../
-include $(CFML)/settings.sh
STUB := _stub
# TODO: $(STUB) should be passed to the script Makefile.cf.2
##############################################################
# Default target files
......@@ -43,7 +38,7 @@ ifndef ML
endif
ifndef PREFIX
PREFIX := $(CFML)/local
PREFIX := $(CFML)
endif
ifndef TLC
......@@ -63,6 +58,8 @@ OCAMLBUILD_WITH_OPTIONS := $(OCAMLBUILD) -classic-display -use-ocamlfind -cflags
code: $(ML_MAIN).native
##############################################################
# Characteristic formula generation
......@@ -71,46 +68,19 @@ code: $(ML_MAIN).native
# 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
@echo "Characteristic formula files generated"
test:
echo $(ML)
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 $@
#***********TEMP:
#test:
# @make CFML=$(CFML) --no-print-directory -f $(CFML)/lib/make/Makefile.cf.2 -j test
##############################################################
# Verification proof
COQINCLUDE := -R $(PREFIX)/lib/coq CFML -R $(TLC) TLC -I .
COQINCLUDE := -R $(PREFIX)/lib/coq CFML -R $(TLC) TLC -R . EXAMPLE
#include $(CFML)/lib/make/Makefile.coq
......@@ -133,14 +103,18 @@ ifeq ($(findstring $(MAKECMDGOALS),clean),)
-include $(VD)
endif
%.v.d: %.v
@$(COQDEP) $(COQINCLUDE) -I . $< > $@
test:
@echo $(ML)
%.v.d: %.v
$(COQDEP) $(COQINCLUDE) $< > $@
%.vo: %.v
$(COQC) $(COQINCLUDE) -I . $<
$(COQC) $(COQINCLUDE) $<
%.vio: %.v
$(COQC) -quick $(COQINCLUDE) -I . $<
$(COQC) -quick $(COQINCLUDE) $<
##############################################################
......@@ -156,6 +130,6 @@ clean:
rm -rf _build *.native
rm -f *.cmj
rm -rf output *_ml.v
rm -f *.v.d *.vio *.vo *.glob
rm -rf $(STUB)
rm -f *.d *.v.d *.vio *.vo *.glob
......@@ -21,11 +21,11 @@ let outputfile = ref None
(* err_formatter *)
(*#########################################################################*)
let _ =
Clflags.strict_value_restriction := true;
Clflags.no_std_include := true;
Settings.configure();
(*---------------------------------------------------*)
trace "1) parsing of command line";
......
......@@ -13,8 +13,7 @@ let no_mystd_include = ref false
let _ =
Clflags.strict_value_restriction := true;
Clflags.no_std_include := true;
Settings.configure();
(*---------------------------------------------------*)
let files = ref [] in
......
let configure () =
Config.interface_suffix := "____mli_files_are_ignored____";
Clflags.strict_value_restriction := true;
Clflags.no_std_include := true
# We assume that CFML has not necessarily been installed.
# Compile only a subset of the files available here
SRC :=\
Shared \
CFHeaps \
CFSpec \
CFPrint \
CFTactics \
CFPrim \
CFRep \
CFLib \
V := $(SRC:=.v)
-include ../../settings.sh
# Find Makefile.tlc.
......@@ -10,5 +25,6 @@ include $(ROOT)/Makefile.tlc
# Compile.
COQINCLUDE := -R $(TLC) TLC -R . CFML
include $(ROOT)/lib/make/Makefile.coq
......@@ -33,20 +33,19 @@
# ------------------------------------------------------------------------------
PREFIX := $(CFML)/local
ifndef PREFIX
PREFIX := $(CFML)
endif
COQINCLUDE:= -R $(PREFIX)/lib/coq/ CFML -R $(PREFIX)/lib/tlc/ TLC
COQINCLUDE:= -R $(PREFIX)/lib/coq/ CFML -R $(PREFIX)/lib/tlc/ TLC -R . EXAMPLE
# ------------------------------------------------------------------------------
# The CFML generator.
GENERATOR := $(CFML)/local/bin/cfml
# The name of the directory _stub.
STUB := _stub
GENERATOR := $(CFML)/bin/cfml
# Standard tools.
OCAMLDEP := $(COQBIN)ocamldep
OCAMLDEP := ocamldep
COQC := $(COQBIN)coqc
# Extra scripts.
......@@ -56,13 +55,13 @@ OCAMLPOST := $(CFML)/lib/make/ocamldep.post
# ------------------------------------------------------------------------------
# The OCaml source files.
ML := $(shell cd $(STUB) && ls *.ml)
ML := $(wildcard *.ml)
# The Coq files that we produce.
MLV := $(patsubst %.ml,%_ml.v,$(ML))
# The compiled Coq files.
MLVO := $(patsubst %.ml,%_ml.vo,$(ML))
# The dependency files.
D := $(patsubst %.ml,$(STUB)/%.d,$(ML))
D := $(patsubst %.ml,%.d,$(ML))
.PHONY: all clean
......@@ -74,29 +73,23 @@ D := $(patsubst %.ml,$(STUB)/%.d,$(ML))
# The goal is to produce the compiled Coq files.
all: $(MLVO)
echo $(ML) $(ls *.ml)
# Cleaning up.
clean:
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.cmj: B.cmj
# A_ml.vo: B_ml.vo
# whenever module A depends on module B.
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
# depend on the presence or absence of certain .mli files.)
......@@ -104,8 +97,10 @@ $(STUB)/%.d: $(STUB)/%.ml
# out the standard library modules.)
# We use the script $(OCAMLPOST) to post-process the output of ocamldep
# and filter out the standard library modules.
%.d: %.ml
@for B in `$(OCAMLDEP) -modules $< | CFML=$(CFML) $(OCAMLPOST)` ; do \
echo $(STUB)/$*.cmj: $(STUB)/$${B}.cmj ; \
echo $*.cmj: $${B}.cmj ; \
echo $*_ml.vo: $${B}_ml.vo ; \
done > $@
......@@ -113,15 +108,13 @@ $(STUB)/%.d: $(STUB)/%.ml
# The generator produces %_ml.v and %.cmj file out of %.ml.
# Only the %.cmj target is known to "make".
# The target %_ml.v is generated in _stub; we move it up.
%.cmj: %.ml
$(GENERATOR) -I $(STUB) $<
@mv -f $*_ml.v .
$(GENERATOR) -I . $<
# ------------------------------------------------------------------------------
# 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
%_ml.vo: %.cmj
$(COQC) $(COQINCLUDE) $*_ml.v
......@@ -9,7 +9,10 @@ COQC := $(COQBIN)coqc
COQDEP := $(COQBIN)coqdep
COQIDE := $(COQBIN)coqide
V := $(wildcard *.v)
ifndef V
V := $(wildcard *.v)
endif
VO := $(patsubst %.v,%.vo,$(V))
VIO := $(patsubst %.v,%.vio,$(V))
VD := $(patsubst %.v,%.v.d,$(V))
......
......@@ -4,7 +4,8 @@
(* 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/local/lib/ocaml. *)
library directory is assumed to be $CFML/lib/ocaml.
******TODO: generate a list of files in a text file instead of relying on folder *)
let warning msg =
Printf.fprintf stderr "%s: warning: %s.\n" Sys.argv.(0) msg;
......@@ -39,11 +40,12 @@ let dependencies (line : string) : string list =
[]
let is_stdlib_module (m : string) =
(***** TODO: hack because it didn't work *)
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 ^ "/local/lib/ocaml/" ^ m ^ ".cmj")
Sys.file_exists (cfml ^ "/lib/ocaml/" ^ m ^ ".cmj")
with Not_found ->
warning "CFML is undefined";
false
......
# A Makefile which produces .cmj files out of .mli files.
##*********TODO: errors below should not occur if target is "clean".
##*********TODO: error should appear if *.mli files have not been initialized
# We assume MAKECMJ is defined externally.
ifndef MAKECMJ
$(error Please define MAKECMJ)
......@@ -27,3 +30,5 @@ pervasives.cmj: pervasives.mli
.depend: $(MLI)
@$(MYOCAMLDEP) $^ > $@
clean:
rm *.cmj
\ No newline at end of file
......@@ -6,6 +6,17 @@ if [ -f ./settings.sh ]
then
source settings.sh
fi
if [ -f ../settings.sh ]
then
source ../settings.sh
fi
if [ -f ../../settings.sh ]
then
source ../../settings.sh
fi
# TODO: improve with a while loop?
#echo coqbin=${COQBIN}
# todo: generalize to all
......@@ -17,7 +28,7 @@ else
FILE=`find . -name ${FILE}`
fi
${COQBIN}coqide -R ${TLC} TLC -R lib/coq CFML ${FILE}
${COQBIN}coqide -R ${TLC} TLC -R ${CFML}/lib/coq CFML -I . ${FILE}
#-dont-load-proofs -async-proofs-j 1
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