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

3
  o [prover] support for Z3 4.3.*
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6 7
  o [prover] fixed Coq 8.4 support for theory real.Trigonometry
  o [prover] support for CVC4
  o [prover] support for mathematica
  o [prover] support for MathSAT5
8

9
version 0.80, Oct 31, 2012
MARCHE Claude's avatar
MARCHE Claude committed
10
==========================
11 12 13 14
  * [whyml] modified syntax for mlw programs; a summary of changes is
    given in Appendix A of the manual
  o [whyml] support for type invariants and ghost code
  o [api] Ocaml interfaces for constructing program modules
15 16
  o [transformation] experimental support for induction on integers
    and on algebraic types
17
  o [interface] new system of warnings, that includes:
MARCHE Claude's avatar
MARCHE Claude committed
18 19 20
     - form "exists x, P -> Q", likely an error
     - unused bound logic variables in "forall", "exists" and "let"
  o [replayer] new option -q, for running quietly
21 22 23 24
  * [session] improved output of "why3session latex"; LaTeX macros have
    more arguments
  o [prover] support for Coq 8.4
  * [prover] dropped support for Coq 8.2
25
  o [prover] support for forthcoming PVS 6.0, including realizations
26
  o [prover] support for iProver and Zenon
27 28
  o [prover] new output scheme for Coq using type classes, to ensures
    types are inhabited
29 30 31 32
  * [driver] theory realizations now use meta "realized_theory" instead
    of "realized"
  * [config] modifiers in --extra-config are now called [prover_modifier]
    instead of just [prover]
33

34 35
version 0.73, Jul 19, 2012
==========================
36
  o [IDE] "Clean" was cleaning too much
37
  * no more executable why3ml (why3 now handles WhyML files)
38
  o [Provers] support for Z3 4.0
MARCHE Claude's avatar
MARCHE Claude committed
39 40
  o [Sessions] a small change in the format. Why3 is still able to
    read session files in the old format.
MARCHE Claude's avatar
MARCHE Claude committed
41 42 43 44 45
  o completed support for the "Out Of Memory" prover result
  o [Why3ml] new construct "abstract e { q }"
  o [Coq output] quotes in identifiers remain quotes in Coq
  o [Coq output] default tactic is now "intros ..." with a pattern
    that matches the structure of the goal
46
  o [why3replayer] option -obsolete-only
MARCHE Claude's avatar
MARCHE Claude committed
47 48
  o workaround for a bug about modulo operator in Alt-Ergo 0.94
  o fixed a consistency issue with set.Fset theory
MARCHE Claude's avatar
MARCHE Claude committed
49
  o co-inductive predicates
50 51 52
  o new option -e for "why3session latex" allows to specify when to
    split tables in parts

53 54 55 56 57 58 59 60 61 62 63 64
version 0.72, May 11, 2012
==========================
  o [Coq] new tactic "why3" to call external provers as oracles
  o [Coq output] new feature: theory realizations (see manual, chapter 9)
  o new tool why3session (see manual, section 6.7)
  o new tool why3doc (see manual, section 6.8)
  o support for multiple versions of the same prover (see manual, section 5.5)
  o [why3ide] new features, including prover upgrade, alternate editors
  o complete support for limiting provers' memory usage
  o improved support on Microsoft Windows
  o fix BTS 14221
  o fix BTS 14190
65
  o fix BTS 12457
MARCHE Claude's avatar
MARCHE Claude committed
66 67
  o fix BTS 13854
  o fix BTS 13849
68 69
  o [syntax] new syntax "constant x:ty" and "constant x:ty = e" to
    introduce constants, as an alternative to "function"
Andrei Paskevich's avatar
Andrei Paskevich committed
70 71 72 73 74 75 76 77
  o [TPTP] new parser for TPTP files with support for the newest
    TFA1 format (TPTP with polymorphic types and arithmetic)
  o [API] Dtype declaration kind is split into two: Dtype for
    declarations of a single abstract type or type alias, and
    Ddata for a list of (mutually recursive) algebraic types.
    Similarly, Dlogic declaration kind is split into Dparam for
    a single abstract function/predicate symbol and Dlogic for
    a list of (mutually recursive) defined symbols.
78

79
version 0.71, October 13, 2011
MARCHE Claude's avatar
MARCHE Claude committed
80 81 82 83 84
==============================

  o [examples] a lot of new program examples in directory examples/programs
  o [Why3replayer] new option -latex to output a proof session in LaTeX format
  o [WhyML] significant improvement of the efficiency of the WP calculus
85
  o [WhyIDE] better coloring and source positioning including from front-ends
MARCHE Claude's avatar
MARCHE Claude committed
86 87
    such as Krakatoa and Jessie plugin of Frama-C
  o [WhyML] fixed labels and source locations in WPs
MARCHE Claude's avatar
MARCHE Claude committed
88 89
  o [Session] during reload, new method for pairing old and new subgoals
    based on goal shapes, stored in database.
MARCHE Claude's avatar
MARCHE Claude committed
90 91 92 93
  o [Session] prover versions are stored in database. A proof is
    marked obsolete if it was made by a prover with another version
    than the current.

94 95 96 97 98 99 100 101 102 103 104
version 0.70, July 6, 2011
==========================

  New features

  o [WhyML] language and VC generator
  o [syntax] record types
    - introduced with syntax "type t = {| a:int; b:bool |}"
      actually syntactic sugar for "type t = `mk t' (a:int) (b:bool)"
      i.e. an algebraic with one constructor and projection functions
    - a record expression is written {| a = 1; b = True |}
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
105 106 107
    - access to field a with syntax x.a
    - update with syntax {| x with b = False |}
    - record patterns
108
  o new tool why3replayer: batch replay of a Why3 session created in IDE
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
109
  o [Alt-Ergo/Z3/CVC3/Yices output] support for built-in theory of arrays
110 111 112 113 114 115

  Fixes and other changes

  * [syntax] new syntax for conjunction (/\) and disjunction (\/)
    ("and" and "or" do not exist anymore)
  * [syntax] "logic" is not a keyword anymore, use "function" and "predicate"
116 117
  o [IDE] interactive detection of provers disabled because incompatible
    with session. Detection must be done with why3config --detect-provers
MARCHE Claude's avatar
MARCHE Claude committed
118
  o [IDE] bug 12244 resolved by using Task.task_equal
MARCHE Claude's avatar
MARCHE Claude committed
119
  o [IDE] tool "Replay" works
MARCHE Claude's avatar
MARCHE Claude committed
120
  o [IDE] tool "Reload" reloads the file from disk. No need to exit IDE anymore
MARCHE Claude's avatar
MARCHE Claude committed
121 122
  o [IDE] does not use Threads anymore, thanks to Call_provers.query_call
  o [IDE] displays explanations using labels of the form "expl:..."
MARCHE Claude's avatar
MARCHE Claude committed
123
  o [IDE] dropped dependence on Sqlite3
124 125 126 127 128 129 130
  o [Alt-Ergo output] bugfix: no triggers for "exists" quantifier
  o [Coq output] bugfix: polymorphic inductive predicates
  o [Coq output] fixed bug 12934: type def with several type params
  * [API] functions to create an environment are now exported from Env
  * [API] 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:
131 132 133 134
    - 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 ()) ()".
135

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
136 137 138
version 0.64, Feb 16, 2011
==========================

139
  o configure: if possible, use ocamlfind to find lablgtk2 and sqlite3
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
140
  o algebraic types: must be well-founded, non-positive constructors
MARCHE Claude's avatar
MARCHE Claude committed
141
    are forbidden, recursive functions and predicates must
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
142
    structurally terminate
143
  * syntax: /\ renamed into && and \/ into ||
MARCHE Claude's avatar
MARCHE Claude committed
144 145
  o accept lowercase names for axioms, lemmas, goals, and cases in
    inductive predicates
146
  o labels in terms and formulas are not printed by default.
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
147 148 149 150 151 152 153 154 155 156 157
  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
158
  o TPTP: encoding by explicit polymorphism is not anymore the
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
159
    default encoding for TPTP provers. It is now forbidden to use this
MARCHE Claude's avatar
MARCHE Claude committed
160
    encoding in presence of finite types.
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
161
  o IDE: source file names are stored in database with paths relative
162 163 164
    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
165
  o better Gappa output: support for sqrt, for negative constants
166 167 168 169 170

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

  o first public release. See release notes in manual
MARCHE Claude's avatar
MARCHE Claude committed
171 172 173 174 175

# Emacs parameters
Local Variables:
mode: text
End: