Commit ceea10c2 authored by MARCHE Claude's avatar MARCHE Claude

logo Why in IDE

parent a7214380
* marks an incompatible change * marks an incompatible change
o [Session] during reload, new method for pairing old and new subgoals
based on goal shapes, stored in database.
o [Session] prover versions are stored in database. A proof is o [Session] prover versions are stored in database. A proof is
marked obsolete if it was made by a prover with another version marked obsolete if it was made by a prover with another version
than the current. than the current.
......
...@@ -24,34 +24,8 @@ ...@@ -24,34 +24,8 @@
afficher les explications dans les outils en ligne de afficher les explications dans les outils en ligne de
commande why3 et why3bench + le path commande why3 et why3bench + le path
* Coq plugin
* Coq realization of theories
(Andrei)
* IDE:
** edition, navigation (partially done)
** restore provers detection in the middle of a session.
+ todo: run detection immediately at start up if conf file absent or
outdated
** reimplement "hide proved goals" feature
+ suggested solution: replace model + filter_model by a custom model
(JC + ?)
** saving session
* add a "cancel" choice in the "ask" window
* add "ctrl-S" to save the session explicitly
(partially done, but no shortcut)
* reload: improve matching of new and old goals by use a kind a distance
between some notion of shape of a goal
* Add more examples in the regression tests and in the proval gallery * Add more examples in the regression tests and in the proval gallery
* prover support
** avoid bug of CVC3, e.g in examples/my_cosine.why
** test/debug TPTP output, make Vampire work
** understand bug reports 12792-12794 and 12907
* Papers to write * Papers to write
* DONE Encodings and transformations (Andrei+Francois) * DONE Encodings and transformations (Andrei+Francois)
...@@ -72,6 +46,37 @@ ...@@ -72,6 +46,37 @@
transformations, write new functions on terms (A) transformations, write new functions on terms (A)
** complete manpages.tex: section "Drivers of external provers" (A+F) ** complete manpages.tex: section "Drivers of external provers" (A+F)
=== Roadmap for fourth release ========================
* Coq plugin
* Coq realization of theories
(Andrei)
* prover support
** avoid bug of CVC3, e.g in examples/my_cosine.why
** test/debug TPTP output, make Vampire work
** understand bug reports 12792-12794 and 12907
* IDE:
** edition, navigation (partially done)
** restore provers detection in the middle of a session.
+ todo: run detection immediately at start up if conf file absent or
outdated
** reimplement "hide proved goals" feature
+ suggested solution: replace model + filter_model by a custom model
(JC + ?)
** saving session
* add a "cancel" choice in the "ask" window
* add "ctrl-S" to save the session explicitly
(partially done, but no shortcut)
* replayer: don't replay a goal that has changed, just display as an
unsuccessful replay
* DONE reload: improve matching of new and old goals by use a kind a distance
between some notion of shape of a goal
=== Roadmap for third release 0.70, july 2011 ======================== === Roadmap for third release 0.70, july 2011 ========================
* Final preparation: put on the web page * Final preparation: put on the web page
......
...@@ -24,10 +24,6 @@ open Rc ...@@ -24,10 +24,6 @@ open Rc
open Whyconf open Whyconf
(*
type prover_data = Session.prover_data
*)
type t = type t =
{ mutable window_width : int; { mutable window_width : int;
mutable window_height : int; mutable window_height : int;
...@@ -37,9 +33,6 @@ type t = ...@@ -37,9 +33,6 @@ type t =
mutable mem_limit : int; mutable mem_limit : int;
mutable verbose : int; mutable verbose : int;
mutable max_running_processes : int; mutable max_running_processes : int;
(*
mutable provers : prover_data Util.Mstr.t;
*)
mutable default_editor : string; mutable default_editor : string;
mutable show_labels : bool; mutable show_labels : bool;
mutable saving_policy : int; mutable saving_policy : int;
...@@ -92,12 +85,6 @@ let load_config config = ...@@ -92,12 +85,6 @@ let load_config config =
let ide = match get_section config "ide" with let ide = match get_section config "ide" with
| None -> default_ide | None -> default_ide
| Some s -> load_ide s in | Some s -> load_ide s in
(*
let provers = get_provers config in
*)
(*
let env = Lexer.create_env main.loadpath in
*)
(* temporary sets env to empty *) (* temporary sets env to empty *)
let env = Env.create_env_of_loadpath [] in let env = Env.create_env_of_loadpath [] in
{ window_height = ide.ide_window_height; { window_height = ide.ide_window_height;
...@@ -109,9 +96,6 @@ let load_config config = ...@@ -109,9 +96,6 @@ let load_config config =
verbose = ide.ide_verbose; verbose = ide.ide_verbose;
saving_policy = ide.ide_saving_policy ; saving_policy = ide.ide_saving_policy ;
max_running_processes = Whyconf.running_provers_max main; max_running_processes = Whyconf.running_provers_max main;
(*
provers = Mstr.empty;
*)
default_editor = ide.ide_default_editor; default_editor = ide.ide_default_editor;
show_labels = false; show_labels = false;
config = config; config = config;
...@@ -169,7 +153,7 @@ let get_main () = (get_main config.config) ...@@ -169,7 +153,7 @@ let get_main () = (get_main config.config)
(* (*
boomy icons images, icons
*) *)
...@@ -237,6 +221,8 @@ let image_reload = ref !image_default ...@@ -237,6 +221,8 @@ let image_reload = ref !image_default
let image_remove = ref !image_default let image_remove = ref !image_default
let image_cleaning = ref !image_default let image_cleaning = ref !image_default
let why_icon = ref !image_default
let resize_images size = let resize_images size =
image_default := image ~size iconname_default; image_default := image ~size iconname_default;
image_undone := image ~size iconname_undone; image_undone := image ~size iconname_undone;
...@@ -268,6 +254,7 @@ let resize_images size = ...@@ -268,6 +254,7 @@ let resize_images size =
let () = let () =
eprintf "[Info] reading icons...@?"; eprintf "[Info] reading icons...@?";
why_icon := image "logo-why";
resize_images 20; resize_images 20;
eprintf " done.@." eprintf " done.@."
......
...@@ -19,10 +19,6 @@ ...@@ -19,10 +19,6 @@
open Why3 open Why3
(*
type prover_data = Session.prover_data
*)
type t = type t =
{ mutable window_width : int; { mutable window_width : int;
mutable window_height : int; mutable window_height : int;
...@@ -39,21 +35,17 @@ type t = ...@@ -39,21 +35,17 @@ type t =
mutable config : Whyconf.config; mutable config : Whyconf.config;
} }
(*
val get_prover_data : Why3.Env.env -> string ->
Why3.Whyconf.config_prover ->
prover_data Why3.Util.Mstr.t -> prover_data Why3.Util.Mstr.t
*)
val save_config : unit -> unit val save_config : unit -> unit
val config : t val config : t
val get_main : unit -> Whyconf.main val get_main : unit -> Whyconf.main
(***************) (*****************)
(* boomy icons *) (* images, icons *)
(***************) (*****************)
val why_icon : GdkPixbuf.pixbuf ref
val image_yes : GdkPixbuf.pixbuf ref val image_yes : GdkPixbuf.pixbuf ref
...@@ -92,10 +84,6 @@ val show_legend_window : unit -> unit ...@@ -92,10 +84,6 @@ val show_legend_window : unit -> unit
val show_about_window : unit -> unit val show_about_window : unit -> unit
val preferences : t -> unit val preferences : t -> unit
(* buggy
val run_auto_detection : t -> unit
*)
(* (*
Local Variables: Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3ide.byte" compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
......
...@@ -133,6 +133,9 @@ let w = GWindow.window ...@@ -133,6 +133,9 @@ let w = GWindow.window
~height:gconfig.window_height ~height:gconfig.window_height
~title:"Why3 Interactive Proof Session" () ~title:"Why3 Interactive Proof Session" ()
let () =
w#set_icon (Some !Gconfig.why_icon)
let (_ : GtkSignal.id) = let (_ : GtkSignal.id) =
w#misc#connect#size_allocate w#misc#connect#size_allocate
~callback: ~callback:
......
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