Commit 9ea5cab3 authored by MARCHE Claude's avatar MARCHE Claude

new files for distrib

parent 33503e93
Installation instructions
Shortly, installation is done by
./configure
make
make install (as root)
To install also the Ocaml library do
make byte
make install-lib (as root)
For detailed instructions and required dependencies, please see
the manual (doc/manual.pdf), Chapter 7.
\ No newline at end of file
......@@ -229,8 +229,6 @@ install_no_local::
mkdir -p $(DATADIR)/why3/theories
mkdir -p $(DATADIR)/why3/theories/transform
mkdir -p $(DATADIR)/why3/drivers
mkdir -p $(OCAMLLIB)/why3
cp -f src/why.cmi src/why.cma src/why.cmxa $(OCAMLLIB)/why3
cp -f theories/*.why $(DATADIR)/why3/theories
cp -f theories/transform/*.why $(DATADIR)/why3/theories/transform
cp -f drivers/*.drv $(DATADIR)/why3/drivers
......@@ -239,14 +237,22 @@ install_no_local::
cp -f share/emacs/why.el $(DATADIR)/why3/emacs/why.el
cp -f share/lang/why.lang $(DATADIR)/why3/lang/why.lang
install_no_local_lib::
mkdir -p $(OCAMLLIB)/why3
cp -f src/why.cm* $(OCAMLLIB)/why3
if test -f src/why.a; then cp -f src/why.a $(OCAMLLIB)/why3; fi
ifeq ("@ENABLE_LOCAL@","no")
install: install_no_local
install-lib: install_no_local_lib
else
install:
install install-lib:
@echo "You use a local configuration you can't install with it."
@echo "Run ./configure without --enable-local"
endif
install-all: install install-lib
##################
# Why binary
......@@ -740,74 +746,6 @@ clean::
rm -f $(PLUGGENERATED)
rm -f .depend.plug
## install: install-binary install-lib install-man
##
## BINARYFILES = $(BINARY) bin/whyide.$(OCAMLBEST)
##
## # install-binary should not depend on $(BINARYFILES); otherwise it
## # enforces the compilation of whyide, even when lablgtk2 is not installed
## install-binary:
## mkdir -p $(BINDIR)
## cp -f $(BINARY) $(BINDIR)/why$(EXE)
## if test -f bin/whyide.$(OCAMLBEST); then \
## cp -f bin/whyide.$(OCAMLBEST) $(BINDIR)/whyide-bin$(EXE); \
## fi
##
## install-lib:
## mkdir -p $(LIBDIR)/why/why
##
## install-man:
## mkdir -p $(MANDIR)/man1
## cp -f doc/*.1 $(MANDIR)/man1
##
## install-coq-no:
## install-coq-yes: install-coq-@COQVER@
## install-coq-v7:
## mkdir -p $(LIBDIR)/why/coq7
## cp -f $(V7FILES) $(LIBDIR)/why/coq7
## cp -f $(VO7) $(LIBDIR)/why/coq7
## install-coq-v8 install-coq-v8.1:
## if test -w $(COQLIB) ; then \
## mkdir -p $(COQLIB)/user-contrib ; \
## cp -f $(V8FILES) $(COQLIB)/user-contrib ; \
## cp -f $(VO8) $(COQLIB)/user-contrib ; \
## else \
## echo "Cannot copy to Coq standard library. Add $(LIBDIR)/why/coq to Coq include path." ;\
## mkdir -p $(LIBDIR)/why/coq ;\
## cp -f $(VO8) $(V8FILES) $(LIBDIR)/why/coq ;\
## fi
##
## install-pvs-no:
## install-pvs-yes: $(PVSFILES)
## mkdir -p $(PVSLIB)/why
## cp $(PVSFILES) $(PVSFILES:.pvs=.prf) $(PVSLIB)/why
## cp lib/pvs/top.pvs lib/pvs/pvscontext.el $(PVSLIB)/why
## @echo "====== Compiling PVS theories, this may take some time ======"
## (cd $(PVSLIB)/why ; @PVSC@ -batch -l pvscontext.el -q -v 2 > top.out)
## @echo "====== Done compiling PVS theories ======"
##
## install-mizar-no:
## install-mizar-yes:
## mkdir -p @MIZARLIB@/mml/dict
## cp lib/mizar/why.miz @MIZARLIB@/mml
## cp lib/mizar/dict/why.voc @MIZARLIB@/mml/dict
##
## local-install: $(BINARY) $(WHYCONFIG) $(JESSIE) bin/whyide.$(OCAMLBEST) byte bin/whyide.byte
## cp $(BINARY) $$HOME/bin/why
## cp $(WHYCONFIG) $$HOME/bin/why
## cp $(JESSIE) $$HOME/bin/jessie
## if test -f bin/whyide.$(OCAMLBEST); then \
## cp -f bin/whyide.$(OCAMLBEST) $$HOME/bin/whyide; \
## fi
##
## local: install
##
## win: why.nsi
## "/cygdrive/c/Program Files (x86)/NSIS/makensis" /DVERSION=$(VERSION) why.nsi
##
## zip:
## zip -A -r why-$(VERSION).zip c:/why/bin c:/why/lib c:/coq/lib/contrib/why c:/coq/lib/contrib7/why
################
# documentation
################
......
TODO: Andrei
\ No newline at end of file
......@@ -4,6 +4,11 @@ Why3 is a tool for automated and interactive proving in first-order
polymorphic logic. It provides a collection of command-line tools, a
graphical interface and an Objective Caml library.
PROJECT HOME
============
https://gforge.inria.fr/projects/why3
DOCUMENTATION
=============
......@@ -32,4 +37,4 @@ xx (see file OCAML-LICENSE).
INSTALLATION
============
See the enclosed file INSTALL.
See the file INSTALL.
......@@ -4,7 +4,7 @@
== Documentation ==
* API: Andrei + Francois
* tools: WhyML (JC), IDE (Claude)
* tools: IDE (Claude)
* semantics:
* tutorial for API:
** build a task
......@@ -22,11 +22,17 @@
== Misc ==
* README (done)
* INSTALL (done)
* LICENSE (done)
* OCAML-LICENSE (TODO: Andrei)
* Builtin arrays in provers (Francois)
(done) make install
(done) debug "make -j"
* META for ocamlfind
* headers
* make install (done)
* make export (TODO: JCF)
* "make -j" (done)
* META for ocamlfind (TODO: ?)
* headers (TODO: ?)
......@@ -34,6 +40,7 @@
= Roadmap for 2011 =
* WhyML (JC)
* Jessie3
* traceability
* Coq plugin
......
......@@ -82,7 +82,7 @@ We gratefully thank all the people who contributed to this document:
\input{library.tex}
\input{whyml.tex}
% \input{whyml.tex}
\input{api.tex}
......
This diff is collapsed.
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Why
(** {1 Proof manager database} *)
(** {2 Current proof state} *)
(** prover data *)
type prover
(** abstract type for the set of provers of the database *)
val prover_name : prover -> string
(** name of a prover *)
val get_prover : string -> prover
(** retrieves prover from its unique name. creates a new prover if
needed. *)
(** status of an external proof attempt *)
type proof_attempt_status =
| Scheduled (** external proof attempt is scheduled *)
| Running (** external proof attempt is in progress *)
| Success (** external proof attempt succeeded *)
| Timeout (** external proof attempt was interrupted *)
| Unknown (** external prover answered ``don't know'' or equivalent *)
| HighFailure (** external prover call failed *)
val print_status : Format.formatter -> proof_attempt_status -> unit
type external_proof
(** abstract type for a proof attempt with an external prover *)
val prover : external_proof -> prover
(** the prover used for this attempt *)
val timelimit : external_proof -> int
(** the time limit chosen for this attempt *)
val memlimit : external_proof -> int
(** the memory limit chosen for this attempt *)
val status : external_proof -> proof_attempt_status
(** the current status for this attempt *)
val result_time : external_proof -> float
(** the time taken for this attempt. Only meaningfull for attempts
that are not Scheduled or Running. *)
val trace : external_proof -> string
(** a trace of execution of this attempt. Not used yet. *)
val proof_obsolete : external_proof -> bool
(** this attempt became obsolete because goal has changed. *)
type goal
(** abstract type for goals *)
(** module Goal to allow use of goals in Hashtables or Map or Set *)
module Goal : sig
type t = goal
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
end
type transf_data =
{ transf_name : string;
transf_action : Task.task Trans.tlist
}
type transf
(** goal accessors *)
val goal_name : goal -> string
(** returns a goal's name, if any *)
(*
val parent : goal -> transf option
*)
val goal_task : goal -> Task.task
val goal_task_checksum: goal -> string
val external_proofs : goal -> external_proof list
(** returns the set of external proof attempt for that goal *)
val transformations : goal -> transf list
val goal_proved : goal -> bool
(** tells if the goal is proved valid or not.
It returns true iff either
{ul {li exists proof p in [external_proofs g] s.t.
proof_obsolete p == false and status p = Valid}}
or
{ul {li exists transf t in [transformations g] s.t.
transf_obsolete t == false and
forall g in [subgoals t], [goal_proved g]}}
*)
(** transf accessors *)
val transf_data : transf -> transf_data
val transf_obsolete : transf -> bool
val subgoals : transf -> goal list
(** {2 The persistent database} *)
val init_base : string -> unit
(** opens or creates the current database, from given file name *)
val root_goals : unit -> goal list
(** returns the current set of root goals *)
(** {2 attempts to solve goals} *)
exception AlreadyAttempted
val try_prover :
async:((unit->unit)->unit) ->
debug:bool -> timelimit:int -> memlimit:int -> prover:prover ->
command:string -> driver:Driver.driver -> goal ->
(unit -> proof_attempt_status)
(** attempts to prove goal with the given prover. This function
prepares the goal for that prover, adds it as an new
external_proof attempt, setting its current status to Scheduled,
and returns immmediately a function. When called, this function
actually sets the status to running, launches the prover, and
waits for its termination. Upon termination of the external
process, the prover's answer is retrieved and database is
updated, that is the [proved] field of the database is updated,
and also these of any goal affected, according to invariant
above. The prover result is also returned.
Although goal preparation is not re-entrant, the function
returned initially is re-entrant, thus is suitable for being executed
in a thread, in contexts where background execution of provers is wanted.
@param timelimit CPU time limit given for that attempt, in
seconds, must be positive. (unlimited attempts are not allowed
with this function)
@param memlimit memory limit given for that attempt, must be
positive. If not given, does not limit memory consumption
@raise AlreadyAttempted if there already exists a non-obsolete
external proof attempt with the same prover and time limit, or
with a lower or equal time limit and a result different from Timeout
*)
val add_transformation: goal -> transf -> unit
(** adds a transformation on the goal. This function adds a new
corresponding attempt for that goal, computes the subgoals and
and them in the database. In the case where no subgoal is
genereated, the [proved] field is updated, and those of parent
goals.
if this transformation has already been attempted but is markes
as obsolete, it is retried, and the new lists of goals is
carefully matched with the older subgoals, so that if some
subgoals are identical to older ones, then the proof is kept.
Notice that no old proof attempts should be lost in this
process, e.g if the old trans formation produced 3 subgoals
A,B,C, C was proved interactively, and the new transformations
produces only 2 goals, the interactive proof of C is keep in an
extra dummy goal "true"
@raise AlreadyAttempted if this transformation has already been attempted
and is not obsolete
*)
(** TODO: removal of attempts *)
(* {2 goal updates} *)
val add_or_replace_task: tname:string -> name:string -> Task.task -> goal
(** updates the database with the new goal called [name] in the
theory called [tname]. If a goal with the same [(tname,name)]
already exists, it is checked whether the task to prove is
different or not. If it is the same, proof attempts are
preserved. If not the same, former proof attempts are marked as
obsolete.
WARNING: the current implementation always adds a new task,
without checking if it already exists
IMPORTANT: this kills every running prover tasks
*)
(** TODO: full update, removing goals that are not pertinent anymore *)
This diff is collapsed.
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
#load "printer_utils.cmo"
#load "sql_orm_header.cmo"
#load "sql_orm.cmo"
open Sql_orm
open Schema
let boolean = integer
let all_tables = make
[
(* table of locs *)
("loc",
[ text "file";
integer "line";
integer "start";
integer "stop";
],
[], default_opts);
(* external proofs *)
("external_proof",
[ text "prover"; (* prover identifier *)
integer "timelimit"; (* CPU limit given in seconds *)
integer "memlimit"; (* VM limit given in megabytes *)
integer "status"; (* enum{proof_attempt_status}; the current state *)
real "result_time"; (* CPU time for that run in seconds *)
text "trace"; (* any kind of trace returned by an automatic prover,
or any kind of proof script for an interactive prover *)
boolean "obsolete";
],
[], default_opts);
(* goal *)
("goal",
[ text "task_checksum";
foreign "transf" "parent"; (* parent transf if any *)
text "name"; (* qualified proposition name *)
foreign "loc" "pos";
foreign_many "external_proof" "external_proofs";
foreign_many "transf" "transformations";
boolean "proved";
],
[], default_opts);
(* transformations *)
("transf",
[ text "name"; (* transformation name *)
boolean "obsolete";
foreign_many "goal" "subgoals";
],
[], default_opts);
]
let () = generate ~debug:false all_tables "src/manager/db"
(* queue of pending proof attempts
protected by a lock
*)
let queue_lock = Mutex.create ()
let attempts = Queue.create ()
let running_proofs = ref 0
let maximum_running_proofs = ref 2
let schedule_proof_attempt ~async ~debug ~timelimit ~memlimit ~prover
~command ~driver ~callback
goal =
let prepare_goal =
try
Db.try_prover ~async ~debug ~timelimit ~memlimit ~prover ~command ~driver goal;
with Db.AlreadyAttempted ->
raise Exit
in
let _thread_id =
Thread.create
begin
fun () ->
try
(* BEGIN LOCKED SECTION *)
(* lock and store the attempt into the queue *)
Mutex.lock queue_lock;
Queue.push (prepare_goal,callback) attempts;
callback Db.Scheduled;
(* try to run attempt if resource available *)
while !running_proofs < !maximum_running_proofs do
let call,callback = Queue.pop attempts in
incr running_proofs;
callback Db.Running;
Mutex.unlock queue_lock;
(* END LOCKED SECTION *)
let res = call () in
(* BEGIN LOCKED SECTION *)
Mutex.lock queue_lock;
callback res;
decr running_proofs;
done;
Mutex.unlock queue_lock
(* END LOCKED SECTION *)
with
| Queue.Empty ->
(* Queue was Empty *)
Mutex.unlock queue_lock
(* END LOCKED SECTION *)
| e ->
(* any other exception should be propagated
after unlocking the lock *)
Mutex.unlock queue_lock;
(* END LOCKED SECTION *)
raise e
end
()
in ()
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/gwhy.byte"
End:
*)
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Why
val schedule_proof_attempt :
async:((unit->unit)->unit) ->
debug:bool -> timelimit:int -> memlimit:int -> prover:Db.prover ->
command:string -> driver:Driver.driver ->
callback:(Db.proof_attempt_status -> unit) -> Db.goal -> unit
(** schedules an attempt to prove goal with the given prover. This
function just prepares the goal for the proof attempt, and puts
it in the queue of waiting proof attempts, associated with its
callback.
The callback is called each time the status of that proves
changes, typically from Scheduled, then Running, then Success or
Timeout or Failure.
@param timelimit CPU time limit given for that attempt, in
seconds, must be positive. (unlimited attempts are not allowed
with this function)
@param memlimit memory limit given for that attempt, must be
positive. If not given, does not limit memory consumption
@raise AlreadyAttempted if there already exists a non-obsolete
external proof attempt with the same prover and time limit, or
with a lower or equal time limit and a result different from Timeout
*)
(*
Local Variables:
compile-command: "make -C ../.. bin/manager.byte"
End:
*)
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(** {1 Proof manager database} *)
(** {2 proof attempts and transformations} *)
(** status of an external proof attempt *)
type proof_attempt_status =
| Running (** external proof attempt is in progress *)
| Success (** external proof attempt succeeded *)
| Timeout (** external proof attempt was interrupted *)
| Unknown (** external prover answered ``don't know'' or equivalent *)
| HighFailure (** external prover call failed *)
(** a proof attempt by some external provers *)
type external_proof =
{ prover : Driver.driver; (** prover driver *)
timelimit : int; (** CPU limit given in seconds *)
status : proof_attempt_status; (** the current state *)
result_time : float ; (** CPU time for that run *)
trace : string;
(** any kind of trace returned by the prover.
when redoing the same attempt, the former trace is sent again *)
obsolete : bool;
(** when true, goal as changed after that proof attempt *)
}
type transf = Task.task Register.tlist_reg
(** an proof attempt is either an external proof or a transformation
into subtasks *)
type attempt =
| External of external_proof
| Transf of transf
(** {2 proof goals in a proof project} *)
type loc
type explain
type identifier
type goal_origin =
| Goal of Decl.prsymbol
| VCfun of loc * explain * identifier
| Subgoal of goal
and goal =
{
task : Task.task;
task_checksum: string;
origin : goal_origin;
mutable attempts : attempt list;
mutable proved : bool;
(** invariant: g.proved == true iff
exists attempts a in g.attempts, a.obsolete == false and
(a = External e and e.result == Valid or
a = Transf(gl) and forall g in gl, g.proved)
*)
mutable observers: (bool -> unit) list;
(** observers that wants to be notified by any changes of the proved status *)
}
(** {2 database for a proof project} *)
type loc_record_in_db =
{ file : string;
line : int;
cbegin : int;
cend : int;
}
type goal_record_in_db =
{
task_checksum : string;
parent : transf_in_db option;
name : string; (* qualified proposition name *)
origin : loc_record_in_db option;
external_proofs : external_proof_in_db list;
transformations : transf_in_db list;
proved : bool;
}
and external_proof_in_db =
{
prover : string; (** prover identifier *)
timelimit : int; (** CPU limit given in seconds *)
memlimit : int; (** VM limit given in megabytes *)
status : int; (** enum{proof_attempt_status}; the current state *)
result_time : float ; (** CPU time for that run in seconds *)
trace : string option;
(** any kind of trace returned by an automatic prover,
or any kind of proof script for an interactive prover *)
obsolete : bool;
}
and transf_in_db =
{
name : string; (** transformation name *)
obsolete : bool;
}
val read_db_from_file : unit -> goal list
(** returns the set of root goals *)