X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdist%2FChangeLog;h=a0a1c51a9dc6442819675d44ed7ea103c5f726c5;hb=732ffd3b5cb77cbacb60b95c1d52d3b63bd56c3b;hp=f6f973f031700b38c9c579c7373689692114f7ea;hpb=05482479b8f4cf4c86ff91e43a913b47aa270cc6;p=helm.git diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog index f6f973f03..a0a1c51a9 100644 --- a/helm/software/matita/dist/ChangeLog +++ b/helm/software/matita/dist/ChangeLog @@ -1,10 +1,150 @@ -0.5.1 - -/5/2008 - minor bug fix release +0.5.8 - 02/12/2009 - toward the 1.x series + * Complete rewriting of paramodulation code (thanks to Maxime Denes), + that is abstract over the data type embedded in the fisrt order + theory the procedure is able to handle. + Can be used as a stand-alone prover, and partecipated + to the CASC22 beating many older systems ;-) + * new (compact) kernel: + * toplevel fixpoints + * height (inter object dependency) driven conversion + * compact metavariable representation + * experimental irrelevant arguments handling in convesion + (in the spirit of proof irrelevance) + * explicit predicative universes + * new refiner: + * bi-directional type inference + * unification hints + * implicit vector (expands to the right number of implicits) + * new basic tactics: + * new type for tactics, with a global view on the ongoing proof + * heavily based on the refiner + * work with terms labelled with their contexts + * new auto (prolog like) proof search tactic: + * works on a set of goals + * non uniform context support: + * arbitrary tactics can be called to attack a goal (hardcoded + at the OCaml level), for now just apply and intro + * new installation: + * the standard library (now we have two of them) is not + distributed pre-compiled + * standard library .ma files can be included from everywhere since + they are in a standard path + * including a file of the standard library triggers its compilation + in the user's space + * gtksourceview2 based text widget (lablgtk >= 2.14) + +0.5.7 - 15/02/2009 - Pàdoa release + * are_convertible bug solved, arguments of application where + compared allowing cumulativity. This allowed to prove Type0=Type1. + * cases tactic speedup in the simplest case of an inductive type + hose right parameters have all to be abstracted when the outtype is + built + * maction support added to output notation (adopted for "=" that + expands to "= \sub T" to show the equality type) + * generation of derived lemmas rewritten to be based on hooks that + are triggered every definition + * composition of coercions fixed, more composite are generated + * undo mechanism for coercions remade, should work better + * new command "prefer coercion foo" to reorder coercions. + * UTF-8 eq classes and virtuals described in the manual and + consistently printed in the TeX/UTF-8 table + * added a memory system for UTF-8 equivalence classes, so that + last choice is remembered and attempted first next time the same + eq class is walked trough + * some core notation fixed to allow a better setoid-path + representation (foo ^-1 changed precedence) + * matita manual updated with a section regarding the usage of + the liveCD with the VirtualBox emulator + * liveCD fixed to allow to easily mount/unmount real host folders + with VirtualBox + * ttf-freefont package added to the liveCD together with gucharmap + * coercions from convertible types are not inserted for real, they + just behave as hints for the unification algorithm + * virtuals (eq classes) fixed w.r.t. greek letters + * some virtuals added to ease the writing of diamond (<>), box ([]) + and upper bar (_). + * code that generates eliminators fixed to use whd ~delta set to true + when counting products, this allows to used definitions as inductive + type ariety. + * match ... with rendering fixed to break the box containing + constructors arguments if needed (i.e. record projections + are now almost readable) + * fixed pattern matching over ast terms, Ast.Case construct can be + matched correctly. Look the o-algebra example if you are + intereseted. + * Mpadded MathML tag can be used in notation, it allows to overlap + symbols reducing the bounding box size + +0.5.6 - 1/12/2008 - bugfix release + * more abstract disambiguation algorithm, simpler instantiation + to a different CIC/refiner + * natural deduction support improved in the first order case + * natural deduction lem rule does now support lemmas + with (up to) 3 premises (multicut rule, displayed as + a collapsed tree) + +0.5.5 - 17/11/2008 - bugfix release with students in mind + * by ... we proved fixed to use only the specified lemmas but + using full unification inside auto. + * new apply rule tactic, that exploits the goal type to + disambiguate the input term. + * new didactic/ library directory, with support for natural deduction + treese. + +0.5.4 - 19/10/2008 - bugfix release + * When a file is opened, the cursor is placed at the begin of the + buffer and not atthe end as before + * New macro eval + * More code in the direction of a fully functional matita status, that + improved undo reliability in the parser/notation modules + * matitac was seldom compiling up-to-date files, fixed + * Memory consumption durin proof construction cut down using Lazy.t + proof terms + * mstyle support in notation for text color, font size + * AutoGui now scales fonts to the correct user-requested size + * Non linear pattern matching from the level of terms to the + one of content in interpretation command (if the same variable name + is used, the two captured terms must be alpha equivalent to match) + +0.5.3 - 23/7/2008 - bugfix release + * many fixes concerning the CProp hiearchy + * coercion database simplified + * coercion hiding now works properly for coercions to funclass + * triangular pullback works better with coercions to the function space + * notation for lists fixed to add a break point after the separator + * notation for the existential is now user definable + * \infrule layout added, allows to display readable fractions + * better window for terms grammar and TeX/Unicode + * fixed a bug in the positivity check not considering some subterms + * fixed some GUI glitches thanks to glade-3 + +0.5.2 - 2/7/2008 - better-usability-for-the-working-constructivist release + * refinement of match fixed to prevent useless unfolding, + head_beta_reduce is used instead of whd ~delta:true + * CProp hierarchy, interleaved with type (used to be a single universe) + * Notation now allows to set the precedence level of subterms, avoiding + unnecessary parenthese + * UTF-8 / TeX conversion table is now available in the Help menu + * Notation subsystem described in the manual + * EBNF term grammar is now available in the View menu (and is in sync with + the currently loaded notation) + * Rewrite tactic (in hypothesis) now computes the right sort and + uses the right equality elimination principle + * URI free interpretation and coercion statements (scripts are almost + relocatable now) + * elim and cases tactic now support a pattern to specify hypotheses that + are generalized before the elimination. + +0.5.1 - 29/5/2008 - minor bug fix release + * visualization of inductive types reports the number of fixed parameters * a wrong context was used to refine fixpoints arguments when trying to optimize out the letin (grep for `AvoidLetIn): (let rec f x = Fix... in f t ---> Fix... t) * auto fixed to prefer goals with metavariables to closed ones, added new syntax to specify the universe "auto by t1, t2, ...", updated documentation describing all auto parameters + * declarative language syntax and documentation ported to the new + auto parameters 0.5.0 - 9/5/2008 - bugfix release * first release not considered experimental