Commit 556f9fd9 authored by charguer's avatar charguer

sep

parents b2f2d1e6 7ba728ec
......@@ -14,9 +14,7 @@ _CoqProject
*.cache
# CFML
*.cmj
lib/tools/cfml_cmj
lib/tools/cfml_dep
lib/tools/cfml_mlv
generator/cfml_config.ml
README.html
lib/coq/README.html
*_ml.v
......
.PHONY: all coqlib tools demos doc clean install
.PHONY: all coqlib generator examples doc clean install uninstall reinstall
CFML := $(shell pwd)
TOOLS := $(CFML)/lib/tools
include Makefile.common
##############################################################################
# Installation destinations.
DEFAULT_PREFIX := $(shell opam config var prefix)
ifeq ($(DEFAULT_PREFIX),)
DEFAULT_PREFIX := /usr/local
endif
PREFIX ?= $(DEFAULT_PREFIX)
BINDIR ?= $(PREFIX)/bin
LIBDIR ?= $(PREFIX)/lib/cfml
##############################################################################
# Targets.
all: coqlib tools
$(MAKE) -C lib/stdlib
all: coqlib generator
$(MAKE) CFMLC=$(CFML)/generator/main.native -C lib/stdlib
coqlib:
$(MAKE) -C lib/coq proof
tools:
generator:
rm -f generator/cfml_config.ml
sed -e 's|@@PREFIX@@|$(PREFIX)|' \
-e 's|@@BINDIR@@|$(BINDIR)|' \
-e 's|@@LIBDIR@@|$(LIBDIR)|' \
generator/cfml_config.ml.in > generator/cfml_config.ml
$(MAKE) -C generator
ln -sf $(CFML)/generator/main.native $(TOOLS)/cfml_mlv
ln -sf $(CFML)/generator/makecmj.native $(TOOLS)/cfml_cmj
ln -sf $(CFML)/generator/myocamldep.native $(TOOLS)/cfml_dep
demos: all
examples: all
$(MAKE) -C examples
##############################################################################
......@@ -40,7 +51,7 @@ clean:
$(MAKE) -C lib/coq $@
$(MAKE) -C lib/stdlib $@
$(MAKE) -C generator $@
rm -rf $(TOOLS)/cfml_mlv $(TOOLS)/cfml_cmj $(TOOLS)/cfml_dep
rm -f generator/cfml_config.ml
rm -f $(DOC)
##############################################################################
......@@ -50,9 +61,46 @@ clean:
# directory to this directory (cfml). Otherwise, perform a copy.
# TEMPORARY, this is TODO
WHERE := $(shell $(COQBIN)coqc -where)
CONTRIB := $(WHERE)/user-contrib
COQ_WHERE := $(shell $(COQBIN)coqc -where)
COQ_CONTRIB := $(COQ_WHERE)/user-contrib
# As install depends on all, the file generator/cfml_config.ml is regenerated
# when `make install` is run; this ensures LIBDIR cannot be inconsistent.
install: all
# Install the generator binary
install -m755 $(CFML)/generator/_build/main.native $(BINDIR)/cfmlc
# install -m755 $(CFML)/generator/_build/makecmj.native $(BINDIR)/cfml_cmj
# Cleanup LIBDIR
rm -rf $(LIBDIR)
# Install the stdlib .cmj files
mkdir -p $(LIBDIR)/stdlib
install $(CFML)/lib/stdlib/*.cmj $(LIBDIR)/stdlib
# Install the auxiliary makefiles
mkdir -p $(LIBDIR)/make
install $(CFML)/lib/make/Makefile.cfml $(LIBDIR)/make
install -m755 $(CFML)/lib/make/ocamldep.post $(LIBDIR)/make
# Cleanup COQ_CONTRIB/CFML
rm -rf $(COQ_CONTRIB)/CFML
# Install the CFML core coq library
mkdir -p $(COQ_CONTRIB)/CFML
install $(CFML)/lib/coq/*.vo $(COQ_CONTRIB)/CFML
# Install the CFML stdlib coq library
mkdir -p $(COQ_CONTRIB)/CFML/Stdlib
install $(CFML)/lib/stdlib/*.vo $(COQ_CONTRIB)/CFML/Stdlib
uninstall:
rm -f $(BINDIR)/cfmlc
# rm -f $(BINDIR)/cfml_cmj
rm -rf $(LIBDIR)
rm -rf $(DOCDIR)
rm -rf $(COQ_CONTRIB)/CFML
install:
mkdir -p $(CONTRIB)
ln -s `pwd` $(CONTRIB)/CFML
reinstall: uninstall
@ $(MAKE) install
......@@ -5,20 +5,10 @@
# trailing slash), e.g. COQBIN=/var/tmp/coq/bin/.
# If COQBIN is undefined, then "coqc" is used.
# To request installation via a symbolic link, as opposed to
# installation via a copy, define ARTHUR.
# To request creation of .vio files, as opposed to creation of .vo
# files, define SERIOUS=0.
# This assumes that $(CFML) points to the CFML root directory.
SERIOUS := 1
-include $(CFML)/settings.sh
export SERIOUS
############################################################################
# We assume that TLC has been installed.
# (Note: this definition can be overriden from outside.)
......
lib/stdlib should have make quick target
----------
-- lib/stdlib should have make quick target
-- while loop invariant : when b is false, should not prove decrease
......@@ -43,57 +39,48 @@ lib/stdlib should have make quick target
-- Array.iter forall l, Array xs \c I l
-- renommer Array.of_list
-- utiliser "of_list []" à la place de make_empty
-- régler le "==>"
-- utiliser "of_list []" à la place de make_empty
-- avoir un flag pour _output
-- external sur une constante, passe pas le typeur
-- ajouter
- documenter la faiblesse de Array.make
- remettre les vrais noms des external
- todo: test xif new variants
-- documenter la faiblesse de Array.make
-- remettre les vrais noms des external
-- todo: test xif new variants
(* TODO / FIX
Open Scope set_scope.
Notation "\aset{ x : A | P }" := (@set_st A (fun x => P))
(at level 0, x ident, A at level 0, P at level 200) : set_scope.
*)
-- todo: test xand
-- xclose with args for the change.
-- xsimpl on I X ==> I Y produces X = Y.
-- xapp_rm
-- generate inhab instance for algebraic
-- hint spec based on type args
-- xchanges
-- implement xpush.
- implement xpush.
(* TODO / FIX
Open Scope set_scope.
Notation "\aset{ x : A | P }" := (@set_st A (fun x => P))
(at level 0, x ident, A at level 0, P at level 200) : set_scope.
*)
----
MAJOR TODAY
----
MAJOR NEXT
- record with imperative
......@@ -124,7 +111,7 @@ MAJOR NEXT
with : match r with T_intro x1 .. xN => T_intro x1 .. yI .. xN
=> requires the order of labels to be fixed as in the definition.
----
MAJOR NEXT NEXT
- xlet_keep
......@@ -143,7 +130,10 @@ MAJOR NEXT NEXT
- see if we can get rid of make_cmj, using -only-cmj
=> make_cmj seems to already be never used.
-- xwhile: error reporting when arguments don't have the right types.
----
MAJOR POSTPONED
- support char, string, float
......@@ -224,65 +214,9 @@ MAKEFILE BEAUTIFY
##################################################################
# COQ BUG remaining
--------------
coq 8.6:
> coqc -v
The Coq Proof Assistant, version trunk (July 2016)
--------------
omega requires Z.sub to be transparent, but this is an issue for simpl.
--------------
~/shared/formalmetacoq/tuto$
coqc -R . TUTO -R ~/tlc/src TLC Coind.v -quick
Crashes if "Print foo" command remains in script.
--------------
semantics of config.keys with modifiers by group...
--------------
Warning: Notation _ * _ was already used in scope type_scope
[notation-overridden,parsing]
=> s'affiche à chaque include !
---------------
Coqide internal error: Source ID 1252 was not found when attempting to remove it
Handshake failed: End_of_file
Thread 122 killed on uncaught exception Sys.Break
=> don't know how
---------------
disable highlighting in feeback window
##############################################
I successfully migrated all my scripts to Coq 8.6, without pain.
I've reported a couple of bugs in the bugtracker. Most interesting ones:
- coqide is even slower than it used to, and is up to 4.5x slower than coqc (#4935).
- coqide interrupt button no longer works, it only kills the parser thread (#4700),
- forcing to use "Arguments" vs "Implicit Arguments" is problematic imo,
because "Arguments" requires too much redundant information (#4936).
Regarding compilation speeed, I confirm that v8.6 is a little bit
faster than v8.5, typically around 10% faster for my scripts,
and sometimes up to 25%, depending on the file. Details follow.
......@@ -356,166 +290,11 @@ v8.6:
##############################################
---------------
CFML/lib/CFHeaps.v
v8.5
time coqc CFHeaps.vo
real 0m12.192s
coqide
~ 14s
v8.6
time coqc CFHeaps.vo
real 0m8.782s
coqide
~ 19s
---------------
To reproduce, use the following branch that compiles both in 8.5 and 8.6:
git clone -b coq-v8.6 https://gforge.inria.fr/git/tlc/tlc.git
Run "make" (to produce vio), or "export SERIOUS=1; make" (to produce vo).
---------------
TLC/LibList.v
v8.5
time coqc
real 0m8.202s
coqide
~ 20s
v8.6
time coqc
real 0m7.787s
coqide
~ 32s
---------------
To reproduce, use the following branch that compiles both in 8.5 and 8.6:
git clone -b coq-v8.6 https://gforge.inria.fr/git/tlc/tlc.git
Enter folder "tlc/src".
Run "export SERIOUS=1; make LibList.vo" to produce the necessary vo files.
Then "time coqc -R . TLC LibList.v".
And "coqide -R . TLC LibList.v", then request compilation to the last line.
---------------
Error: To rename arguments the "rename" flag must be specified.
Argument y renamed to x.
---------------
Axiom eq_trans : forall (A:Type) (y x z:A),
x = y -> y = z -> x = z.
BEFORE
Implicit Arguments eq_trans [A].
AFTER
Arguments eq_trans [A] y x z _ _.
---------------
This command is just asserting the number and names of arguments of
eq_dep_nd. If this is what you want add ': assert' to silence the warning. If
you want to clear implicit arguments add ': clear implicits'. If you want to
clear notation scopes add ': clear scopes'
[arguments-assert,vernacular]
=> no comment
----------------
pb coexist vio & vo
----------------
In nested Ltac calls to "inverts", "libtac_invert_noregen", "go" (bound to
fun tt =>
match goal with
| |- libtac_mark -> _ => intros _
| |- ?x = ?y -> _ =>
let H := fresh "TEMP" in
intro H; (first [ subst x | subst y ]); go tt
| |- existT ?P ?p ?x = existT ?P ?p ?y -> _ =>
let H := fresh in
intro H; generalize (inj_pair2 H); clear H; go tt
| |- _ -> _ =>
intro;
(let H := libtac_get_last_introduced_hyp tt in
libtac_mark_to_generalize H; go tt)
end), "go" (bound to
fun tt =>
match goal with
| |- libtac_mark -> _ => intros _
| |- ?x = ?y -> _ =>
let H := fresh "TEMP" in
intro H; (first [ subst x | subst y ]); go tt
| |- existT ?P ?p ?x = existT ?P ?p ?y -> _ =>
let H := fresh in
intro H; generalize (inj_pair2 H); clear H; go tt
| |- _ -> _ =>
intro;
(let H := libtac_get_last_introduced_hyp tt in
libtac_mark_to_generalize H; go tt)
end), "go" (bound to
fun tt =>
match goal with
| |- libtac_mark -> _ => intros _
| |- ?x = ?y -> _ =>
let H := fresh "TEMP" in
intro H; (first [ subst x | subst y ]); go tt
| |- existT ?P ?p ?x = existT ?P ?p ?y -> _ =>
let H := fresh in
intro H; generalize (inj_pair2 H); clear H; go tt
| |- _ -> _ =>
intro;
(let H := libtac_get_last_introduced_hyp tt in
libtac_mark_to_generalize H; go tt)
end) and "go" (bound to
fun tt =>
match goal with
| |- libtac_mark -> _ => intros _
| |- ?x = ?y -> _ =>
let H := fresh "TEMP" in
intro H; (first [ subst x | subst y ]); go tt
| |- existT ?P ?p ?x = existT ?P ?p ?y -> _ =>
let H := fresh in
intro H; generalize (inj_pair2 H); clear H; go tt
| |- _ -> _ =>
intro;
(let H := libtac_get_last_introduced_hyp tt in
libtac_mark_to_generalize H; go tt)
end), last call failed.
Error: No matching clauses for match.
-----------------
-async-proofs off
-async-proofs-j n
for coqide is not documented
Set Implicit Arguments.
Require Import CFLib CFLibCredits.
Require Import CFML.CFLib CFML.CFLibCredits.
(* Require Import RandomAccessListSig_ml. *)
Require Import BinaryRandomAccessList_ml.
Require Import LibListZ.
Require Import TLC.LibListZ.
Module BinaryRandomAccessListSpec (* <: RandomAccessListSigSpec *).
......@@ -149,7 +149,7 @@ Qed.
Lemma inv_ts_len : forall A ts p (L:list A),
inv p ts L ->
ts <> nil ->
ts <> nil ->
2 ^ (p + (length ts) - 1) <= length L.
Proof.
induction ts as [|d ts].
......@@ -208,8 +208,8 @@ Qed.
(** verification *)
(* todo move *)
(* TODO: lemma to rewrite ÷ with / under assumption that args > 0
(* todo move *)
(* TODO: lemma to rewrite ÷ with / under assumption that args > 0
and tactic rew_div pour optimiser. *)
Lemma pow2_succ_div : forall p, p >= 0 -> 2 ^ (p+1) ÷ 2 = 2 ^ p.
......@@ -301,7 +301,7 @@ Proof. xcf. xapp~. Qed.
Hint Extern 1 (RegisterSpec cons) => Provide cons_spec.
Lemma uncons_tree_spec : forall A (ts: rlist_ A) p L,
inv p ts L ->
inv p ts L ->
ts <> nil ->
app uncons_tree [ts]
PRE \[]
......@@ -359,7 +359,7 @@ Qed.
Hint Extern 1 (RegisterSpec tail) => Provide tail_spec.
Require Import LibInt.
Require Import TLC.LibInt.
Lemma lookup_tree_spec :
forall a i (t: tree_ a) p L,
......@@ -382,7 +382,7 @@ Qed.
Hint Extern 1 (RegisterSpec lookup_tree) => Provide lookup_tree_spec.
Lemma update_tree_spec :
Lemma update_tree_spec :
forall a i (x: a) (t: tree_ a) p L,
btree p t L ->
ZInbound i L ->
......@@ -405,7 +405,7 @@ Qed.
Hint Extern 1 (RegisterSpec update_tree) => Provide update_tree_spec.
Ltac xapp_xapply_no_simpl K ::=
xapply_core K ltac:(fun _ => idtac) ltac:(fun _ => idtac).
xapply_core K ltac:(fun _ => idtac) ltac:(fun _ => idtac).
Lemma lookup_spec_ind :
......@@ -421,7 +421,7 @@ Proof.
- { xmatch. xapps~. unpack. subst.
forwards~: length_correct. forwards~: btree_size_correct.
xapps~. xif.
xapp_no_simpl~. (* xapp~ T. *)
xapp_no_simpl~. (* xapp~ T. *)
- apply~ ZInbound_app_l_inv.
- hsimpl. apply~ ZNth_app_l.
- xgo~. apply~ ZInbound_app_r_inv. apply~ ZNth_app_r. }
......@@ -444,30 +444,30 @@ Proof.
- { xmatch. xapps~. unpack. subst.
forwards~: length_correct. forwards~: btree_size_correct.
xapps~. xif.
xapp_no_simpl~. (* xapp~ T. *)
xapp_no_simpl~. (* xapp~ T. *)
- apply~ ZInbound_app_l_inv.
- hsimpl. apply~ ZNth_app_l.
- xgo~. apply~ ZInbound_app_r_inv. apply~ ZNth_app_r. }
(*
-- strategy 2.
-- strategy 2.
introv. unfold Rlist. generalize 0 as p. revert i L.
induction ts; introv I Bi; inverts I; xcf.
- xgo. apply~ ZInbound_nil_inv.
- { xmatch. xapps~. unpack. subst.
forwards~: length_correct. forwards~: btree_size_correct.
xapps~. xif.
xapp_no_simpl~. (* xapp~ T. *)
xapp_no_simpl~. (* xapp~ T. *)
- apply~ ZInbound_app_l_inv.
- hsimpl. apply~ ZNth_app_l.
- xgo~. apply~ ZInbound_app_r_inv. apply~ ZNth_app_r. }
-- strategy 3.
-- strategy 3.
assert ( de toute la spec )
-- strategy 4
lemme séparée
-- strategy 4
lemme séparée
*)
Qed.
(* OLD
......
This diff is collapsed.
# CFML := ../../..
# include $(CFML)/Makefile.common
#
# ML := Demo.ml TestDepend_AuxCode.ml TestDepend_MainCode.ml
# PWD := $(shell pwd)
# V := $(wildcard $(PWD)/*.v)
#
# V_AUX := \
# $(wildcard $(TLC)/*.v) \
# $(wildcard $(CFML)/lib/coq/*.v) \
# $(wildcard $(CFML)/lib/stdlib/*.v) \
#
# CFML_FLAGS := -debug
# ML := TestDepend_AuxCode.ml TestDepend_MainCode.ml
# For tests, use:
# ML := Test.ml
# V := $(PWD)/Test_ml.v $(PWD)/Test_proof.v
# To exclude some files:
# V := $(filter-out $(PWD)/Demo_proof.v $(PWD)/Demo_ml.v $(PWD)/Test_proof.v $(PWD)/Test_ml.v, $(wildcard $(PWD)/*.v))
# To include some files:
# V := $(addprefix $(PWD)/, TestDepend_OnlyCoq.v TestDepend_MainCode_proof.v TestDepend_AuxCode_proof.v)
include ../Makefile.example
EXAMPLE_DIRS = \
Demos \
Tuto \
BinaryRandomAccessList \
BinaryRandomAccessList \
# TO FIX:
# BatchedQueue => OCaml complains about ungeneralized type variable (!?)
......
##############################################################################
#
# 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,47 +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
ifeq ($(findstring $(MAKECMDGOALS),clean),)
include $(CFML)/lib/make/Makefile.tools
endif
TLC := $(shell $(COQBIN)coqc -where)/user-contrib/TLC
##############################################################################