Commit 8f6a08df authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
parents d2083b32 b206453e
......@@ -5,8 +5,8 @@ This chapter is a tutorial for the users who wants to link their own
OCaml code with the Why3 library. We progressively introduce the way
one can use the library to build terms, formulas, theories, proof
tasks, call external provers on tasks, and apply transformations on
tasks. The complete documentation for API calls is given in
Chapter~\ref{chap:apidoc}.
tasks. The complete documentation for API calls is given
[TODO in Chapter~ref{chap:apidoc}.]
We assume the reader has a fair knowledge of the OCaml
language. Notice also that the Why3 library is installed: see
......
......@@ -55,7 +55,7 @@ Part 2 provides:
\item In Chapter~\ref{chap:manpages}, the technical manual pages for the
tools of the platform. All tool options, and all the configuration
files are described in details there.
\item In Chapter~\ref{chap:apidoc}, the technical documentation of the API.
% \item In Chapter~\ref{chap:apidoc}, the technical documentation of the API.
\end{itemize}
......
......@@ -171,10 +171,9 @@ used to provide other informations :
\item TODO
\end{itemize}
% TODO (pour plus tard)
% \section{The \texttt{why3ml} tool}
[TO BE COMPLETED]
% [TO BE COMPLETED LATER]
\section{The \texttt{why3ide} GUI}
\label{sec:ideref}
......
......@@ -7,6 +7,12 @@
\usepackage[a4paper,pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref}
\usepackage{graphicx}
% \setlrmargins{20mm}{*}{*}
% \setulmargins{1.0in}{*}{*}
% %\setheadfoot{13pt}{26pt}
% %\setheaderspaces{*}{13pt}{*}
% \checkandfixthelayout
%\usepackage[toc,nonumberlist]{glossaries}
%\makeglossaries
......@@ -117,6 +123,24 @@ Report any bug to the Why3 Bug Tracking System:
We gratefully thank the people who contributed to Why3: Simon Cruanes,
Johannes Kanig, St\'ephane Lescuyer, Sim\~ao Melo de Sousa.
\section*{Release notes}
\paragraph{Version 0.10}
Initial release.
\begin{itemize}
\item New syntax for terms and formulas
\item Algebraic data types, pattern-matching
\item Recursive definitions
\item Inductive predicates
\item Declaration encapsulated in theories. Using and cloning theories.
\item Concept of goal transformation
\item Generic communication with provers
\item Ocaml Library with documented API
\item New GUI with session save and restore
\item New syntax for programs, new VC generator, intentionaly left
undocumented, since the syntax is likely to evolve significantly in
the future.
\end{itemize}
\cleardoublepage
\tableofcontents
......
......@@ -498,15 +498,10 @@ module External_proof = struct
in
db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql)
(*
let delete db e =
let id = e.external_proof_id in
assert (id <> 0L);
let sql = "DELETE FROM external_proofs WHERE external_proof_id=?" in
let stmt = bind db sql [ Sqlite3.Data.INT id ] in
ignore(step_fold db stmt (fun _ -> ()));
e.external_proof_id <- 0L
*)
let stmt = bind db sql [ Sqlite3.Data.INT e ] in
ignore(step_fold db stmt (fun _ -> ()))
let add db (g : goal) (p: prover_id) =
transaction db
......@@ -609,6 +604,8 @@ let status_and_time p = External_proof.status_and_time (current()) p
let external_proofs g = External_proof.of_goal (current()) g
let remove_proof_attempt e = External_proof.delete (current()) e
module Goal = struct
let init db =
......
......@@ -152,7 +152,7 @@ val add_proof_attempt : goal -> prover_id -> proof_attempt
@raise AlreadyExist if an attempt for the same prover
is already there *)
(* todo: remove_proof_attempt *)
val remove_proof_attempt : proof_attempt -> unit
val set_obsolete : proof_attempt -> unit
(** marks this proof as obsolete *)
......
......@@ -618,6 +618,15 @@ module Helpers = struct
set_proof_status ~obsolete a status time;
a
let remove_proof_row a =
let (_:bool) = goals_model#remove a.Model.proof_row in
(* let g = a.Model.proof_goal in
remove a from g.Model.external_proofs
and update g.Model.proved
*)
()
let add_goal_row parent name t db_goal =
let parent_row = match parent with
| Theory mth -> mth.theory_row
......@@ -1164,94 +1173,6 @@ let split_selected_goals () =
goals_view#selection#get_selected_rows) ())
(*****************************************************)
(* method: split all unproved goals *)
(*****************************************************)
(*
let split_unproved_goals () =
let transf_id_split = Db.transf_from_name "split_goal" in
List.iter
(fun th ->
List.iter
(fun g ->
if not g.Model.proved then
let row = g.Model.goal_row in
let goal_name = goals_model#get ~row ~column:Model.name_column in
let callback subgoals =
if List.length subgoals >= 2 then
let split_row = goals_model#append ~parent:row () in
goals_model#set ~row:split_row ~column:Model.visible_column
true;
goals_model#set ~row:split_row ~column:Model.name_column
"split";
goals_model#set ~row:split_row ~column:Model.icon_column
!image_transf;
let db_transf =
Db.add_transformation g.Model.goal_db transf_id_split
in
let tr =
{ Model.parent_goal = g;
(*
Model.transf = split_transformation;
*)
Model.transf_row = split_row;
Model.transf_db = db_transf;
subgoals = [];
}
in
goals_model#set ~row:split_row ~column:Model.index_column
(Model.Row_transformation tr);
g.Model.transformations <- tr :: g.Model.transformations;
let goals,_ = List.fold_left
(fun (acc,count) subtask ->
let _id = (Task.task_goal subtask).Decl.pr_name in
let subgoal_name =
goal_name ^ "." ^ (string_of_int count)
in
let subtask_row =
goals_model#append ~parent:split_row ()
in
let sum = task_checksum subtask in
let subtask_db = Db.add_subgoal db_transf
subgoal_name sum in
(* TODO: call add_goal_row *)
let goal = {
Model.goal_name = subgoal_name;
Model.parent = Model.Transf tr;
Model.task = subtask ;
Model.goal_row = subtask_row;
Model.goal_db = subtask_db;
Model.external_proofs = Hashtbl.create 7;
Model.transformations = [];
Model.proved = false;
}
in
goals_model#set ~row:subtask_row
~column:Model.index_column (Model.Row_goal goal);
goals_model#set ~row:subtask_row
~column:Model.visible_column true;
goals_model#set ~row:subtask_row
~column:Model.name_column subgoal_name;
goals_model#set ~row:subtask_row
~column:Model.icon_column !image_file;
(goal :: acc, count+1))
([],1) subgoals
in
tr.Model.subgoals <- List.rev goals;
goals_view#expand_row (goals_model#get_path row)
in
Scheduler.apply_transformation_l ~callback
split_transformation g.Model.task
)
th.Model.goals
)
[] (* !Model.all *)
*)
(*********************************)
(* add a new file in the project *)
(*********************************)
......@@ -1522,8 +1443,10 @@ let () =
let () =
let b = GButton.button ~packing:transf_box#add ~label:"Inline" () in
(*
let i = GMisc.image ~pixbuf:(!image_transf) () in
let () = b#set_image i#coerce in
*)
let (_ : GtkSignal.id) =
b#connect#pressed ~callback:not_implemented
in ()
......@@ -1835,6 +1758,10 @@ let () =
(* removing *)
(*************)
let remove_proof_attempt a =
Db.remove_proof_attempt a.Model.proof_db;
Helpers.remove_proof_row a
let confirm_remove_row r =
let row = filter_model#get_iter r in
match filter_model#get ~row ~column:Model.index_column with
......@@ -1844,17 +1771,14 @@ let confirm_remove_row r =
let (_:bool) = info_window `ERROR "Cannot remove a theory" in ()
| Model.Row_file _file ->
let (_:bool) = info_window `ERROR "Cannot remove a file" in ()
| Model.Row_proof_attempt _a ->
let (_:bool) = info_window `INFO "Proof attempt removal not implemented" in ()
| Model.Row_proof_attempt a ->
let b =
info_window `QUESTION
"Do you really want to remove the selected proof attempt?"
in
if b then remove_proof_attempt a
| Model.Row_transformation _tr ->
let (_:bool) = info_window `INFO "Transformation removal not implemented" in ()
(*
let b =
info_window `QUESTION
"Do you really want to remove the current selection?"
in
if b then remove_selection
*)
let confirm_remove_selection () =
match goals_view#selection#get_selected_rows with
......
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