fixed documentation and updated CHANGES

parent 0065ba02
* marks an incompatible change
* calls to prover can now be asynchronous
Driver.prove_task now returns some intermediate value (of type
prover_call), which can be queried in two ways:
- blocking way with Call_provers.wait_on_call
- non-blocking way with Call_provers.query_call
So old code performing "prove_task t () ()" should be translated to
"wait_on_call (prove_task t ()) ()".
o record types in the logic
- introduced with syntax "type t = {| a:int; b:bool |}"
- actually syntactic sugar for "type t = T (a:int) (b:bool)"
......@@ -11,7 +21,7 @@ version 0.64, Feb 16, 2011
o algebraic types: must be well-founded, non-positive constructors
are forbidden, recursive functions and predicates must
structurally terminate
o syntax: /\ renamed into && and \/ into ||
* syntax: /\ renamed into && and \/ into ||
o accept lowercase names for axioms, lemmas, goals, and cases in
inductive predicates
o labels in terms and formulas are not printed by default.
......
......@@ -175,7 +175,7 @@ loaded first.
\begin{verbatim}
(* builds the environment from the [loadpath] *)
let env : Env.env =
Env.create_env (Lexer.retrieve (Whyconf.loadpath main))
Lexer.create_env (Whyconf.loadpath main)
(* loading the Alt-Ergo driver *)
let alt_ergo_driver : Driver.driver =
Driver.load_driver env alt_ergo.Whyconf.driver
......@@ -187,8 +187,9 @@ termination. Here is a simple way to proceed:
\begin{verbatim}
(* calls Alt-Ergo *)
let result1 : Call_provers.prover_result =
Driver.prove_task ~command:alt_ergo.Whyconf.command
alt_ergo_driver task1 () ()
Call_provers.wait_on_call
(Driver.prove_task ~command:alt_ergo.Whyconf.command
alt_ergo_driver task1 ()) ()
(* prints Alt-Ergo answer *)
let () = printf "@[On task 1, alt-ergo answers %a@]@."
Call_provers.print_prover_result result1
......@@ -225,9 +226,10 @@ Here is thus another way of calling the Alt-Ergo prover, on our second
task.
\begin{verbatim}
let result2 : Call_provers.prover_result =
Driver.prove_task ~command:alt_ergo.Whyconf.command
Call_provers.wait_on_call
(Driver.prove_task ~command:alt_ergo.Whyconf.command
~timelimit:10
alt_ergo_driver task2 () ()
alt_ergo_driver task2 ()) ()
let () =
printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
......
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