Commit d781a155 authored by MARCHE Claude's avatar MARCHE Claude

IDE: removed detection of provers

because it is incompatible with the session system
parent 56f88378
* marks an incompatible change
o [IDE] interactive detection of provers disabled because incompatible
with session. Detection must be done with why3config --detect-provers
o WhyML with mutable record fields and type models
o why3replayer
* "parameter" keyword renamed to "val"
......
......@@ -2,34 +2,47 @@
=== Long-term Roadmap (see below for roadmap to next release) ===========
* Logic language
** support for higher-order logic
** rename andb, orb, xorb and notb into and, or, xor and not
* more libraries (theories and modules)
* WhyML
** regions : strong update
** clone module
** ghost code
** extraction of Ocaml code
** logic symbols used in programs
* Jessie3
* traceability: Partially done
(Claude)
TODO: traceability des hyp comme path dans le prog (depuis
Frama-C en particulier)
afficher les explications dans les outils en ligne de
commande why3 et why3bench + le path
* Coq plugin
* Coq realization of theories
(Andrei)
* more libraries (theories and modules)
* IDE: edition, navigation
(partially done)
* HOL
* IDE: reimplement "hide proved goals" feature
** suggested solution: replace model + filter_model by a custom model
* 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)
* Add as many examples as possible in the regression tests
* Add more examples in the regression tests and in the proval gallery
* Papers to write
......@@ -44,16 +57,11 @@
* system description (e.g. at CAD, TACAS)
* rapports recherche ?
* Why3ide: saving session
* add a "cancel" choice
* add "ctrl-S" to save the session explicitly
* choisir un logo
* choose a logo -> done ?
* complete doc/api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
* rename andb, orb, xorb and notb into and, or, xor and not
=== Roadmap for third release 0.70, july 2011 ========================
......@@ -70,8 +78,6 @@
- threads problem in IDE solved (by not using threads anymore)
** as soon as possible: update why3 output of Why2, release Why 2.30
* doc: citer l'article Boogie 2011 quelque part
* increment the magic number in config (A)
* distribute bench files (A + F)
......@@ -87,6 +93,8 @@
* (done) update doc for why3replayer
- not done: parler des examples distribues ci dessus
* DONE doc: citer l'article Boogie 2011 quelque part
* DONE deplacer le bouton "Cancel" dans le menu "tools",
le renommer en "make obsolete"
......
@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -c '$key="ayad10ijcar" or $key="CoqArt" or $key="conchon08smt" or $key="paskevich09rr" or $key="z3" or $key="ergo" or $key="simplify05" or $key="DM06" or $key="BarTin-CAV-07" or $key="melquiond08rnc" or $key="filliatre07cav" or 1=2' /home/cmarche/biblio/abbrevs.bib /home/cmarche/biblio/demons.bib /home/cmarche/biblio/demons2.bib /home/cmarche/biblio/demons3.bib /home/cmarche/biblio/team.bib /home/cmarche/biblio/crossrefs.bib /home/cmarche/biblio/crossrefs2.bib}}
@comment{{Command line: /usr/bin/bib2bib -c '$key="schulz04ijcar" or $key="ayad10ijcar" or $key="CoqArt" or $key="conchon08smt" or $key="paskevich09rr" or $key="z3" or $key="ergo" or $key="simplify05" or $key="DM06" or $key="BarTin-CAV-07" or $key="vstte10comp" or $key="melquiond08rnc" or $key="filliatre07cav" or $key="okasaki98" or $key="boogie11why3" or 1=2' /home/cmarche/biblio/abbrevs.bib /home/cmarche/biblio/demons.bib /home/cmarche/biblio/demons2.bib /home/cmarche/biblio/demons3.bib /home/cmarche/biblio/team.bib /home/cmarche/biblio/crossrefs.bib /home/cmarche/biblio/crossrefs2.bib}}
@string{sv = {Springer}}
......@@ -58,6 +58,35 @@
note = {\url{http://research.microsoft.com/projects/z3/}}
}
@inproceedings{schulz04ijcar,
author = {S. Schulz},
title = {{System Description: E~0.81}},
booktitle = {Proc.\ of the 2nd IJCAR, Cork, Ireland},
editor = {D. Basin and M. Rusinowitch},
volume = 3097,
series = {LNAI},
year = 2004,
publisher = {Springer},
pages = {223--228}
}
@misc{vstte10comp,
author = {Natarajan Shankar and Peter Mueller},
title = {{Verified Software: Theories, Tools and Experiments
(VSTTE'10). Software Verification Competition}},
month = {August},
year = 2010,
address = {Edinburgh, Scotland},
note = {\url{http://www.macs.hw.ac.uk/vstte10/Competition.html}}
}
@book{okasaki98,
author = {Chris Okasaki},
title = {{Purely Functional Data Structures}},
publisher = {Cambridge University Press},
year = 1998
}
@inproceedings{conchon08smt,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean
and St\'ephane Lescuyer},
......@@ -87,7 +116,8 @@
author = {Sylvain Conchon and \'Evelyne Contejean},
title = {The {Alt-Ergo} automatic Theorem Prover},
url = {http://alt-ergo.lri.fr/},
note = {\url{http://alt-ergo.lri.fr/}},
howpublished = {\url{http://alt-ergo.lri.fr/}},
note = {APP deposit under the number IDDN FR 001 110026 000 S P 2010 000 1000},
topics = {team,lri},
year = 2008,
x-equipes = {demons PROVAL},
......@@ -119,8 +149,6 @@
address = {Santiago de Compostela, Spain},
year = {2008},
pages = {93--102},
note = {\url{http://gappa.gforge.inria.fr/}},
url = {http://gappa.gforge.inria.fr/},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
......@@ -129,7 +157,7 @@
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-pdf = {http://www.msr-inria.inria.fr/~gmelquio/doc/08-rnc8-article.pdf}
x-pdf = {http://www.lri.fr/~melquion/doc/08-rnc8-article.pdf}
}
@techreport{paskevich09rr,
......@@ -140,7 +168,7 @@
topics = {team},
hal = {http://hal.inria.fr/inria-00439232/en/},
note = {\url{http://hal.inria.fr/inria-00439232/en/}},
number = {RR-7128}
number = 7128
}
@inproceedings{ayad10ijcar,
......@@ -148,8 +176,37 @@
title = {Multi-Prover Verification of Floating-Point Programs},
crossref = {ijcar10},
url = {http://www.lri.fr/~marche/ayad10ijcar.pdf},
x-equipes = {demons PROVAL EXT},
topics = {team},
type_publi = {icolcomlec}
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes},
x-cle-support = {IJCAR},
x-type = {article},
x-editorial-board = {yes}
}
@inproceedings{boogie11why3,
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Andrei Paskevich},
title = {Why3: Shepherd Your Herd of Provers},
topics = {team},
booktitle = {Boogie 2011: First International Workshop on Intermediate Verification Languages},
year = 2011,
address = {Wroc\l{}aw, Poland},
month = {August},
url = {http://proval.lri.fr/submissions/boogie11.pdf},
abstract = {Why3 is the next generation of the
Why software verification platform.
Why3 clearly separates the purely logical
specification part from generation of verification conditions for programs.
This article focuses on the former part.
Why3 comes with a new enhanced language of
logical specification. It features a rich library of
proof task transformations that can be chained to produce a suitable
input for a large set of theorem provers, including SMT solvers,
TPTP provers, as well as interactive proof assistants.}
}
@proceedings{ijcar10,
......@@ -175,30 +232,3 @@
year = {2007}
}
@InProceedings{schulz04ijcar,
author = {S. Schulz},
title = {{System Description: E~0.81}},
booktitle = {Proc.\ of the 2nd IJCAR, Cork, Ireland},
editor = {D. Basin and M. Rusinowitch},
volume = 3097,
series = {LNAI},
year = 2004,
publisher = {Springer},
pages = {223--228},
}
@Misc{vstte10comp,
author = {Natarajan Shankar and Peter Mueller},
title = {{Verified Software: Theories, Tools and Experiments
(VSTTE'10). Software Verification Competition}},
month = {August},
year = 2010,
address = {Edinburgh, Scotland},
note = {\url{http://www.macs.hw.ac.uk/vstte10/Competition.html}}}
@BOOK{okasaki98,
author = {Chris Okasaki},
title = {{Purely Functional Data Structures}},
publisher = {Cambridge University Press},
year = 1998
}
......@@ -94,15 +94,14 @@ $^2$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893
\chapter*{Foreword}
This is the manual for the Why platform version 3, or \why for
short. \why is a complete reimplementation of the former Why
platform~\cite{filliatre07cav} for program verification. Among
the new features are: numerous extensions to the input language,
a new architecture for calling external provers, and a
well-designed API, allowing to use \why as a software library.
An important emphasis is put on modularity and genericity,
giving the end user a possibility to easily reuse \why
formalizations or to add support for a new external
prover if wanted.
short. \why is a complete reimplementation~\cite{boogie11why3} of the former Why
platform~\cite{filliatre07cav} for program
verification. Among the new features are: numerous
extensions to the input language, a new architecture for calling
external provers, and a well-designed API, allowing to use \why as a
software library. An important emphasis is put on modularity and
genericity, giving the end user a possibility to easily reuse \why
formalizations or to add support for a new external prover if wanted.
\subsection*{Availability}
......
......@@ -4,43 +4,10 @@
<file name="../hello_proof.why" verified="false" expanded="true">
<theory name="HelloProof" verified="false" expanded="true">
<goal name="G1" sum="da0794d2f4de035d230d26e93d3e1afe" proved="false" expanded="true">
<proof prover="simplify" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G2" sum="07e54d9a25fa3174d5d5bf7ce71a13dc" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="true">
<result status="unknown" time="0.02"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="true">
<result status="unknown" time="0.01"/>
</proof>
<transf name="split_goal" proved="false" expanded="true">
<goal name="G2.1" sum="f7915ef009bdd949e4af326643583051" proved="false" expanded="true">
<proof prover="coq" timelimit="10" edited="" obsolete="true">
<result status="unknown" time="0.46"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="true">
<result status="unknown" time="0.02"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="true">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal name="G2.2" sum="c53f58872dc3cb71805234ace78f1c2d" proved="false" expanded="true">
<proof prover="simplify" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
<goal name="G3" sum="8813554ea4313f64f3efc3330036b5e9" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.01"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="true">
<result status="unknown" time="0.01"/>
</proof>
</goal>
</theory>
</file>
......
......@@ -479,6 +479,7 @@ let preferences c =
save_config ();
dialog#destroy ()
(*
let run_auto_detection gconfig =
let config = Autodetection.run_auto_detection gconfig.config in
gconfig.config <- config;
......@@ -487,6 +488,7 @@ let run_auto_detection gconfig =
gconfig.provers <- Mstr.fold (Session.get_prover_data gconfig.env) provers Mstr.empty
*)
()
*)
let () = eprintf "[Info] end of configuration initialization@."
......
......@@ -32,9 +32,6 @@ type t =
mutable mem_limit : int;
mutable verbose : int;
mutable max_running_processes : int;
(*
mutable provers : prover_data Util.Mstr.t;
*)
mutable default_editor : string;
mutable show_labels : bool;
mutable saving_policy : int;
......@@ -95,7 +92,9 @@ val show_legend_window : unit -> unit
val show_about_window : unit -> unit
val preferences : t -> unit
(* buggy
val run_auto_detection : t -> unit
*)
(*
Local Variables:
......
......@@ -530,21 +530,6 @@ let () =
end
let () =
try
eprintf "[Info] Opening session...@\n@[<v 2> ";
M.open_session ~env:gconfig.env
(* ~provers:gconfig.provers *)
~config:gconfig.Gconfig.config
~init ~notify project_dir;
M.maximum_running_proofs := gconfig.max_running_processes;
eprintf "@]@\n[Info] Opening session: done@."
with e ->
eprintf "@[Error while opening session:@ %a@.@]"
Exn_printer.exn_printer e;
exit 1
let info_window ?(callback=(fun () -> ())) mt s =
let buttons = match mt with
| `INFO -> GWindow.Buttons.close
......@@ -556,16 +541,42 @@ let info_window ?(callback=(fun () -> ())) mt s =
~message:s
~message_type:mt
~buttons
~title:"Why3 info or error"
~title:"Why3IDE"
~modal:true
~show:true ()
in
let (_ : GtkSignal.id) =
d#connect#response
~callback:(function x -> d#destroy ();
if x = `OK then callback ())
~callback:(function x ->
d#destroy ();
if mt <> `QUESTION || x = `OK then callback ())
in ()
(* check if provers are present *)
let () =
if Util.Mstr.is_empty (Whyconf.get_provers gconfig.Gconfig.config) then
begin
info_window `ERROR "No prover configured.\nPlease run 'why3config --detect-provers' first"
~callback:GMain.quit;
GMain.main ();
exit 2;
end
let () =
try
eprintf "[Info] Opening session...@\n@[<v 2> ";
M.open_session ~env:gconfig.env
(* ~provers:gconfig.provers *)
~config:gconfig.Gconfig.config
~init ~notify project_dir;
M.maximum_running_proofs := gconfig.max_running_processes;
eprintf "@]@\n[Info] Opening session: done@."
with e ->
eprintf "@[Error while opening session:@ %a@.@]"
Exn_printer.exn_printer e;
exit 1
(**********************************)
(* add new file from command line *)
......@@ -717,14 +728,17 @@ let (_ : GMenu.image_menu_item) =
let refresh_provers = ref (fun () -> ())
let add_refresh_provers f =
let add_refresh_provers f msg =
eprintf "[Info] recording '%s' for refresh provers@." msg;
let rp = !refresh_provers in
refresh_provers := (fun () -> rp (); f ())
(*
let (_ : GMenu.image_menu_item) =
file_factory#add_image_item ~label:"_Detect provers" ~callback:
(fun () -> Gconfig.run_auto_detection gconfig; !refresh_provers () )
()
*)
let save_session () =
eprintf "[Info] saving session@.";
......@@ -917,12 +931,14 @@ let (_ : GMenu.check_menu_item) = view_factory#add_check_item
let () = add_refresh_provers (fun () ->
List.iter (fun item -> item#destroy ()) provers_box#all_children)
"remove from provers box"
let tools_menu = factory#add_submenu "_Tools"
let tools_factory = new GMenu.factory tools_menu ~accel_group
let () = add_refresh_provers (fun () ->
List.iter (fun item -> item#destroy ()) tools_menu#all_children)
"remove from tools menu"
let () =
let add_item_provers () =
......@@ -948,7 +964,7 @@ let () =
in ())
(M.get_provers ())
in
add_refresh_provers add_item_provers;
add_refresh_provers add_item_provers "Add in tools menu and provers box";
add_item_provers ()
let split_selected_goals () =
......@@ -971,9 +987,9 @@ let () =
~label:"Inline in selection"
~callback:inline_selected_goals
() : GMenu.image_menu_item) in
add_refresh_provers add_separator;
add_refresh_provers add_item_split;
add_refresh_provers add_item_inline;
add_refresh_provers add_separator "add separator in tools menu";
add_refresh_provers add_item_split "add split in tools menu";
add_refresh_provers add_item_inline "add inline in tools menu";
add_separator ();
add_item_split ();
add_item_inline ()
......@@ -1287,10 +1303,10 @@ let () =
~label:"Mark as obsolete"
~callback:cancel_proofs
() : GMenu.image_menu_item) in
add_refresh_provers add_separator;
add_refresh_provers add_item_edit;
add_refresh_provers add_item_replay;
add_refresh_provers add_item_cancel;
add_refresh_provers add_separator "add sep in tools menu";
add_refresh_provers add_item_edit "add edit in tools menu";
add_refresh_provers add_item_replay "add replay in tools menu";
add_refresh_provers add_item_cancel "add cancel in tools menu";
add_separator ();
add_item_edit ();
add_item_replay ();
......@@ -1391,9 +1407,9 @@ let () =
~label:"Clean selection"
~callback:clean_selection
() : GMenu.image_menu_item) in
add_refresh_provers add_separator;
add_refresh_provers add_item_remove;
add_refresh_provers add_item_clean;
add_refresh_provers add_separator "add sep in tools menu";
add_refresh_provers add_item_remove "add remove in tools menu";
add_refresh_provers add_item_clean "add clean in tools menu";
add_separator ();
add_item_remove ();
add_item_clean ()
......
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