src/HOL/Tools/Nitpick/HISTORY
author blanchet
Tue Nov 24 16:11:50 2009 +0100 (2009-11-24)
changeset 33888 4e0da333f75b
parent 33886 cde73f8dbe4e
child 33892 3937da7e13ea
permissions -rw-r--r--
use correct Isabelle version name in README file
blanchet@33888
     1
Version 2009-1
blanchet@33197
     2
blanchet@33197
     3
  * Moved into Isabelle/HOL "Main"
blanchet@33197
     4
  * Renamed "nitpick_const_def" to "nitpick_def", "nitpick_const_simp" to
blanchet@33197
     5
    "nitpick_simp", "nitpick_const_psimp" to "nitpick_psimp", and
blanchet@33197
     6
    "nitpick_ind_intro" to "nitpick_intro"
blanchet@33197
     7
  * Replaced "special_depth" and "skolemize_depth" options by "specialize"
blanchet@33197
     8
    and "skolemize"
blanchet@33556
     9
  * Renamed "coalesce_type_vars" to "merge_type_vars"
blanchet@33558
    10
  * Optimized Kodkod encoding of datatypes whose constructors don't appear in
blanchet@33558
    11
    the formula to falsify
blanchet@33581
    12
  * Added support for codatatype view of datatypes
blanchet@33876
    13
  * Fixed soundness bugs related to sets, sets of sets, (co)inductive
blanchet@33886
    14
    predicates, typedefs, "finite", "rel_comp", and negative literals
blanchet@33197
    15
  * Fixed monotonicity check
blanchet@33853
    16
  * Fixed error when processing definitions
blanchet@33853
    17
  * Fixed error in "star_linear_preds" optimization
blanchet@33744
    18
  * Fixed error in Kodkod encoding of "The" and "Eps"
blanchet@33565
    19
  * Fixed error in display of uncurried constants
blanchet@33581
    20
  * Speeded up scope enumeration
blanchet@33197
    21
blanchet@33197
    22
Version 1.2.2 (16 Oct 2009)
blanchet@33197
    23
blanchet@33197
    24
  * Added and implemented "star_linear_preds" option
blanchet@33197
    25
  * Added and implemented "format" option
blanchet@33197
    26
  * Added and implemented "coalesce_type_vars" option
blanchet@33197
    27
  * Added and implemented "max_genuine" option
blanchet@33197
    28
  * Fixed soundness issues related to "set", "distinct", "image", "Sigma",
blanchet@33197
    29
    "-1::nat", subset, constructors, sort axioms, and partially applied
blanchet@33197
    30
    interpreted constants
blanchet@33197
    31
  * Fixed error in "show_consts" for boxed specialized constants
blanchet@33197
    32
  * Fixed errors in Kodkod encoding of "The", "Eps", and "ind"
blanchet@33197
    33
  * Fixed display of Skolem constants
blanchet@33197
    34
  * Fixed error in "check_potential" and "check_genuine"
blanchet@33197
    35
  * Added boxing support for higher-order constructor parameters
blanchet@33197
    36
  * Changed notation used for coinductive datatypes
blanchet@33197
    37
  * Optimized Kodkod encoding of "If", "card", and "setsum"
blanchet@33197
    38
  * Improved the monotonicity check
blanchet@33197
    39
blanchet@33197
    40
Version 1.2.1 (25 Sep 2009)
blanchet@33197
    41
blanchet@33197
    42
  * Added explicit support for coinductive datatypes
blanchet@33197
    43
  * Added and implemented "box" option
blanchet@33197
    44
  * Added and implemented "fast_descrs" option
blanchet@33197
    45
  * Added and implemented "uncurry" option
blanchet@33197
    46
  * Renamed and generalized "sync_cards" and "inductive_mood" to "mono" and "wf"
blanchet@33197
    47
  * Fixed soundness issue related to nullary constructors
blanchet@33197
    48
  * Fixed soundness issue related to higher-order quantifiers
blanchet@33197
    49
  * Fixed soundness issue related to the "destroy_constrs" optimization
blanchet@33197
    50
  * Fixed soundness issues related to the "special_depth" optimization
blanchet@33197
    51
  * Added support for PicoSAT and incorporated it with the Nitpick package
blanchet@33197
    52
  * Added automatic detection of installed SAT solvers based on naming
blanchet@33197
    53
    convention
blanchet@33197
    54
  * Optimized handling of quantifiers by moving them inward whenever possible
blanchet@33197
    55
  * Optimized and improved precision of "wf" and "wfrec"
blanchet@33197
    56
  * Improved handling of definitions made in locales
blanchet@33197
    57
  * Fixed checked scope count in message shown upon interruption and timeout
blanchet@33197
    58
  * Added minimalistic Nitpick-like tool called Minipick
blanchet@33197
    59
blanchet@33197
    60
Version 1.2.0 (27 Jul 2009)
blanchet@33197
    61
blanchet@33197
    62
  * Optimized Kodkod encoding of datatypes and records
blanchet@33197
    63
  * Optimized coinductive definitions
blanchet@33197
    64
  * Fixed soundness issues related to pairs of functions
blanchet@33197
    65
  * Fixed soundness issue in the peephole optimizer
blanchet@33197
    66
  * Improved precision of non-well-founded predicates occurring positively in
blanchet@33197
    67
    the formula to falsify
blanchet@33197
    68
  * Added and implemented "destroy_constrs" option
blanchet@33197
    69
  * Changed semantics of "inductive_mood" option to ensure soundness
blanchet@33197
    70
  * Fixed semantics of "lockstep" option (broken in 1.1.1) and renamed it
blanchet@33197
    71
    "sync_cards"
blanchet@33197
    72
  * Improved precision of "trancl" and "rtrancl"
blanchet@33197
    73
  * Optimized Kodkod encoding of "tranclp" and "rtranclp"
blanchet@33197
    74
  * Made detection of inconsistent scope specifications more robust
blanchet@33853
    75
  * Fixed a few Kodkod generation bugs
blanchet@33197
    76
blanchet@33197
    77
Version 1.1.1 (24 Jun 2009)
blanchet@33197
    78
blanchet@33197
    79
  * Added "show_all" option
blanchet@33197
    80
  * Fixed soundness issues related to type classes
blanchet@33197
    81
  * Improved precision of some set constructs
blanchet@33197
    82
  * Fiddled with the automatic monotonicity check
blanchet@33197
    83
  * Fixed performance issues related to scope enumeration
blanchet@33853
    84
  * Fixed a few Kodkod generation bugs
blanchet@33197
    85
blanchet@33197
    86
Version 1.1.0 (16 Jun 2009)
blanchet@33197
    87
blanchet@33197
    88
  * Redesigned handling of datatypes to provide an interface baded on "card" and
blanchet@33197
    89
    "max", obsoleting "mult"
blanchet@33197
    90
  * Redesigned handling of typedefs, "rat", and "real"
blanchet@33197
    91
  * Made "lockstep" option a three-state option and added an automatic
blanchet@33197
    92
    monotonicity check
blanchet@33197
    93
  * Made "batch_size" a (n + 1)-state option whose default depends on whether
blanchet@33197
    94
    "debug" is enabled
blanchet@33197
    95
  * Made "debug" automatically enable "verbose"
blanchet@33197
    96
  * Added "destroy_equals" option
blanchet@33197
    97
  * Added "no_assms" option
blanchet@33197
    98
  * Fixed bug in computation of ground type 
blanchet@33197
    99
  * Fixed performance issue related to datatype acyclicity constraint generation
blanchet@33197
   100
  * Fixed performance issue related to axiom selection
blanchet@33197
   101
  * Improved precision of some well-founded inductive predicates
blanchet@33197
   102
  * Added more checks to guard against very large cardinalities
blanchet@33197
   103
  * Improved hit rate of potential counterexamples
blanchet@33197
   104
  * Fixed several soundness issues
blanchet@33197
   105
  * Optimized the Kodkod encoding to benefit more from symmetry breaking
blanchet@33197
   106
  * Optimized relational composition, cartesian product, and converse
blanchet@33197
   107
  * Added support for HaifaSat
blanchet@33197
   108
blanchet@33197
   109
Version 1.0.3 (17 Mar 2009)
blanchet@33197
   110
blanchet@33197
   111
  * Added "HOL-Nominal-Nitpick" as a target in addition to "HOL-Nitpick"
blanchet@33197
   112
  * Added "overlord" option to assist debugging
blanchet@33197
   113
  * Increased default value of "special_depth" option
blanchet@33197
   114
  * Fixed a bug that effectively disabled the "nitpick_const_def" attribute
blanchet@33197
   115
  * Ensured that no scopes are skipped when multithreading is enabled
blanchet@33197
   116
  * Fixed soundness issue in handling of "The", "Eps", and partial functions
blanchet@33197
   117
    defined using Isabelle's function package
blanchet@33197
   118
  * Fixed soundness issue in handling of non-definitional axioms
blanchet@33197
   119
  * Fixed soundness issue in handling of "Abs_" and "Rep_" functions for "unit",
blanchet@33197
   120
    "nat", "int", and "*"
blanchet@33853
   121
  * Fixed a few Kodkod generation bugs
blanchet@33197
   122
  * Optimized "div", "mod", and "dvd" on "nat" and "int"
blanchet@33197
   123
blanchet@33197
   124
Version 1.0.2 (12 Mar 2009)
blanchet@33197
   125
blanchet@33197
   126
  * Added support for non-definitional axioms
blanchet@33197
   127
  * Improved Isar integration
blanchet@33197
   128
  * Added support for multiplicities of 0
blanchet@33197
   129
  * Added "max_threads" option and support for multithreaded Kodkodi
blanchet@33197
   130
  * Added "blocking" option to control whether Nitpick should be run
blanchet@33197
   131
    synchronously or asynchronously
blanchet@33197
   132
  * Merged "auto_timeout" and "wellfounded_timeout" into "tac_timeout"
blanchet@33197
   133
  * Added "auto" option to run Nitpick automatically (like Auto Quickcheck)
blanchet@33197
   134
  * Introduced "auto_timeout" to specify Auto Nitpick's time limit
blanchet@33197
   135
  * Renamed the possible values for the "expect" option
blanchet@33197
   136
  * Renamed the "peephole" option to "peephole_optim"
blanchet@33197
   137
  * Added negative versions of all Boolean options and made "= true" optional
blanchet@33197
   138
  * Altered order of automatic SAT solver selection
blanchet@33197
   139
blanchet@33197
   140
Version 1.0.1 (6 Mar 2009)
blanchet@33197
   141
blanchet@33197
   142
  * Eliminated the need to import "Nitpick" to use "nitpick"
blanchet@33197
   143
  * Added "debug" option
blanchet@33197
   144
  * Replaced "specialize_funs" with the more general "special_depth" option
blanchet@33197
   145
  * Renamed "watch" option to "eval"
blanchet@33197
   146
  * Improved parsing of "card", "mult", and "iter" options
blanchet@33197
   147
  * Fixed a soundness bug in the "specialize_funs" optimization
blanchet@33197
   148
  * Increased the scope of the "specialize_funs" optimization
blanchet@33197
   149
  * Fixed a soundness bug in the treatment of "<" and "<=" on type "int"
blanchet@33197
   150
  * Fixed a soundness bug in the "subterm property" optimization for types of
blanchet@33197
   151
    cardinality 1
blanchet@33197
   152
  * Improved the axiom selection for overloaded constants, which led to an
blanchet@33197
   153
    infinite loop for "Nominal.perm"
blanchet@33197
   154
  * Added support for multiple instantiations of non-well-founded inductive
blanchet@33197
   155
    predicates, which previously raised an exception
blanchet@33853
   156
  * Fixed a Kodkod generation bug
blanchet@33197
   157
  * Altered order of scope enumeration and automatic SAT solver selection
blanchet@33197
   158
  * Optimized "Eps", "nat_case", and "list_case"
blanchet@33197
   159
  * Improved output formatting
blanchet@33197
   160
  * Added checks to prevent infinite loops in axiom selector and constant
blanchet@33197
   161
    unfolding
blanchet@33197
   162
blanchet@33197
   163
Version 1.0.0 (27 Feb 2009)
blanchet@33197
   164
blanchet@33197
   165
  * First release