Commit 2c38a456 authored by MARCHE Claude's avatar MARCHE Claude

prepare for release 0.86

parent 792bc1a4
......@@ -27,17 +27,17 @@ provers
http://www.lix.polytechnique.fr/~lengrand/Psyche/)
o preliminary support for upcoming CVC4 1.5 (steps feature)
bug fixes:
o bug in interpreter in presence of nested mutable fields
o IDE: proofs in progress should never be "cleaned"
o IDE: display warnings after reload
IDE:
o config file not automatically saved anymore at exit. Configuration
is saved on disk for future sessions if, and only if, preferences
window is exited by hitting the "Save&Close" button
o right part of main window organized in tabs.
bug fixes:
o bug in interpreter in presence of nested mutable fields
o IDE: proofs in progress should never be "cleaned"
o IDE: display warnings after reload
version 0.85, September 17, 2014
================================
......
......@@ -159,17 +159,19 @@ Release Notes (details in file CHANGES):
== TODO ==
* plusieurs drivers acceptés sur la ligne de commande (AP)
* clean up the support for SMTLIB bitvectors: there are 2 theories in the stdlib: thoeries/bv.why and modules/bitvectors.mlw
-> not anymore, but more cleaning can be done: no need to separate all theories in drivers for Z3 and CVC4, since the same theory can be put several times in a driver (or imported sub-drivers)
* decide if GUI with tabs is convenient enough
-> onglets dans why3 ide : est-ce apprécié ? OUI
mais enlever l'onglet "Counterexamples" avant la release
* for next release: complete realization of bitvector library
== DONE ==
* clean up the support for SMTLIB bitvectors: there are 2 theories in the stdlib: thoeries/bv.why and modules/bitvectors.mlw
-> not anymore, but more cleaning can be done: no need to separate all theories in drivers for Z3 and CVC4, since the same theory can be put several times in a driver (or imported sub-drivers)
* DONE plusieurs drivers acceptés sur la ligne de commande (AP)
* solve issues with metitarski
. DONE theory PowerReal
. DONE crashes when applied on a WP (see examples/my_cosine.mlw)
......
......@@ -342,10 +342,12 @@ let output_page,output_tab =
3, GPack.vbox ~homogeneous:false ~packing:
(fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
(*
let counterexample_page,counterexample_tab =
let label = GMisc.label ~text:"Counter-example" () in
4, GPack.vbox ~homogeneous:false ~packing:
(fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
*)
let (_ : GPack.box) =
GPack.hbox ~packing:(source_tab#pack ~expand:false ?from:None ?fill:None
......@@ -400,6 +402,7 @@ let output_view =
~packing:scrolled_output_view#add
()
(*
let scrolled_counterexample_view =
GBin.scrolled_window
~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
......@@ -411,11 +414,15 @@ let counterexample_view =
~show_line_numbers:true
~packing:scrolled_counterexample_view#add
()
*)
let modifiable_sans_font_views = ref [goals_view#misc]
let modifiable_mono_font_views =
ref [task_view#misc;edited_view#misc;output_view#misc;
counterexample_view#misc]
(*
counterexample_view#misc
*)
]
let () = task_view#source_buffer#set_language why_lang
let () = task_view#set_highlight_current_line true
......@@ -647,6 +654,7 @@ let update_tabs a =
(Pp.string_of (Pp.hov 2 print) m.S.metas_added)
| _ -> ""
in
(*
let counterexample_text =
match a with
| S.Proof_attempt a ->
......@@ -658,13 +666,16 @@ let update_tabs a =
end
| _ -> ""
in
*)
task_view#source_buffer#set_text task_text;
task_view#scroll_to_mark `INSERT;
edited_view#source_buffer#set_text edited_text;
edited_view#scroll_to_mark `INSERT;
output_view#source_buffer#set_text output_text;
counterexample_view#source_buffer#set_text counterexample_text
(*
counterexample_view#source_buffer#set_text counterexample_text;
*)
()
......
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