CHANGES 3.36 KB
Newer Older
1
* marks an incompatible change
2

3
  o [WhyML] programs labels with new syntax 'L: (instead of label L:)
MARCHE Claude's avatar
MARCHE Claude committed
4
  o [Coq output] fixed bug 12934: type def with several type params
5 6
  o [IDE] interactive detection of provers disabled because incompatible
    with session. Detection must be done with why3config --detect-provers
7
  o [WhyML] mutable record fields and type models
8
  o why3replayer
MARCHE Claude's avatar
MARCHE Claude committed
9
  * "parameter" keyword renamed to "val"
10
  * new syntax for conjunction (/\) and disjunction (\/)
MARCHE Claude's avatar
MARCHE Claude committed
11 12
    ("and" and "or" do not exist anymore)
  * "logic" is not a keyword anymore, use "function" and "predicate"
13
  * functions to create an environment are now exported from Env
MARCHE Claude's avatar
MARCHE Claude committed
14
  o [IDE] bug 12244 resolved by using Task.task_equal
15
  o fixed Alt-ergo output: no triggers for "exists" quantifier
MARCHE Claude's avatar
MARCHE Claude committed
16 17 18 19
  o [IDE] tool "Replay" works
  o [IDE] does not use Threads anymore, thanks to Call_provers.query_call
  o VC gen produces explanations in a suitable form for IDE
  o [IDE] displays explanations using labels of the form "expl:..."
20
  o fixed Coq output for polymorphic inductive predicates
21
  o [IDE] dropped dependence on Sqlite
22
  * calls to prover can now be asynchronous
23 24 25 26 27 28
    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 ()) ()".
29
  o record types
30
    - introduced with syntax "type t = {| a:int; b:bool |}"
31
      actually syntactic sugar for "type t = `mk t' (a:int) (b:bool)"
32
      i.e. an algebraic with one constructor and projection functions
33
    - a record expression is written {| a = 1; b = True |}
34

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
35 36 37
version 0.64, Feb 16, 2011
==========================

38
  o configure: if possible, use ocamlfind to find lablgtk2 and sqlite3
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
39
  o algebraic types: must be well-founded, non-positive constructors
MARCHE Claude's avatar
MARCHE Claude committed
40
    are forbidden, recursive functions and predicates must
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
41
    structurally terminate
42
  * syntax: /\ renamed into && and \/ into ||
MARCHE Claude's avatar
MARCHE Claude committed
43 44
  o accept lowercase names for axioms, lemmas, goals, and cases in
    inductive predicates
45
  o labels in terms and formulas are not printed by default.
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
46 47 48 49 50 51 52 53 54 55 56
  o transformation split-goal does not split under disjunction anymore
  o fixed --enable-local
  o why.conf is no more looked for in the current directory; use -C or
    WHY3CONFIG instead
  o why.conf: when changed, a backup up copy is made in why.conf.bak
  o why.conf now contains a magic number; configuration must be
    rebuilt with why3config if the magic number has changed
  o why3config: --autodetect-provers renamed to --detect-provers
                --autodetect-plugins renamed to --detect-plugins
     new option --detect to perform both detections
  o why3config: --conf_file is replaced by -C and --config
MARCHE Claude's avatar
MARCHE Claude committed
57
  o TPTP: encoding by explicit polymorphism is not anymore the
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
58
    default encoding for TPTP provers. It is now forbidden to use this
MARCHE Claude's avatar
MARCHE Claude committed
59
    encoding in presence of finite types.
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
60
  o IDE: source file names are stored in database with paths relative
61 62 63
    to the database, so that databases are now easier to move from a
    machine to another (e.g when they are stored in source control
    repositories)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
64
  o better Gappa output: support for sqrt, for negative constants
65 66 67 68 69

version 0.63, Dec 21, 2010
==========================

  o first public release. See release notes in manual