Commit 0dfe99ac authored by charguer's avatar charguer

cleanup todo

parent a1e04229
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
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