v4.20.0-rc3

fix: make sure all kernel constants are persisted eventually (#8238)

This PR avoids an issue where, through other potential bugs, constants
that are tracked by `Kernel.Environment` but not `Environment` are not
persisted.

(cherry picked from commit af51e3e4b1c655df43476972c4d9aeae76e49046)

v4.20.0-rc2

fix: cadical distribution on Linux (#8201)

Compile it with the same flags as other executables

v4.20.0-rc1

chore: set release flag

chore: set release flag

v4.19.0

chore: lake: backport dynlib fixes (#8187)

This PR backports fixes to dynamic library linking and loading in Lake
to `v4.19.0`.

Includes changes from #7809, #8026, #8152, and #8190.

v4.19.0-rc3

fix: cancellation of synchronous part of previous elaboration (#7882)

This PR fixes a regression where elaboration of a previous document
version is not cancelled on changes to the document.

Done by removing the default from `SnapshotTask.cancelTk?` and
consistently passing the current thread's token for synchronous
elaboration steps.

(cherry picked from commit 1421b6145e6be03e0f69ab2ad8de4fb1387b8049)

v4.19.0-rc2

For this release, 414 changes landed. In addition to the 164 feature additions and 74 fixes listed below there were 13 refactoring changes, 29 documentation improvements, 31 performance improvements, 9 improvements to the test suite and 92 other changes.

Language

• #5182 makes functions defined by well-founded recursion use an
  opaque well-founded proof by default. This reliably prevents kernel
  reduction of such definitions and proofs, which tends to be
  prohibitively slow (fixes #2171), and which regularly causes
  hard-to-debug kernel type-checking failures. This changes renders
  unseal ineffective for such definitions. To avoid the opaque proof,
  annotate the function definition with @[semireducible].

• #5998 lets omega always abstract its own proofs into an auxiliary
  definition. The size of the olean of Vector.Extract goes down from 20MB
  to 5MB with this, overall stdlib olean size and build instruction count
  go down 5%.

• #6325 ensures that environments can be loaded, repeatedly, without
  executing arbitrary code

• #7075 ensures that names suggested by tactics like simp? are not
  shadowed by auxiliary declarations in the local context and that names
  of let rec and where declarations are correctly resolved in tactic
  blocks.

• #7084 enables the elaboration of theorem bodies, i.e. proofs, to
  happen in parallel to each other as well as to other elaboration tasks.

• #7166 extends the notion of “fixed parameter” of a recursive function
  also to parameters that come after varying function. The main benefit is
  that we get nicer induction principles.

• #7247 makes generation of match equations and splitters compatible
  with parallelism.

• #7256 introduces the assert! variant debug_assert! that is
  activated when compiled with buildType debug.

• #7261 ensures all equation, unfold, induction, and partial fixpoint
  theorem generators in core are compatible with parallelism.

• #7298 adds rewrites to bv_decide's preprocessing that concern
  combinations of if-then-else and operation such as multiplication or
  negation.

• #7302 changes how fields are elaborated in the structure/class
  commands and also makes default values respect the structure resolution
  order when there is diamond inheritance. Before, the details of
  subobjects were exposed during elaboration, and in the local context any
  fields that came from a subobject were defined to be projections of the
  subobject field. Now, every field is represented as a local variable.
  All parents (not just subobject parents) are now represented in the
  local context, and they are now local variables defined to be parent
  constructors applied to field variables (inverting the previous
  relationship). Other notes:

  • The entire collection of parents is processed, and all parent
    projection names are checked for consistency. Every parent appears in
    the local context now.
  • For classes, every parent now contributes an instance, not just the
    parents represented as subobjects.
  • Default values are now processed according to the parent resolution
    order. Default value definition/override auxiliary definitions are
    stored at StructName.fieldName._default, and inherited values are
    stored at StructName.fieldName._inherited_default. Metaprograms no
    longer need to look at parents when doing calculations on default
    values.
  • Default value omission for structure instance notation pretty printing
    has been updated in consideration of this.
  • Now the elaborator generates a _flat_ctor constructor that will be
    used for structure instance elaboration. All types in this constructor
    are put in "field normal form" (projections of parent constructors are
    reduced, and parent constructors are eta reduced), and all fields with
    autoParams are annotated as such. This is not meant for users, but it
    may be useful for metaprogramming.
  • While elaborating fields, any metavariables whose type is one of the
    parents is assigned to that parent. The hypothesis is that, for the
    purpose of elaborating structure fields, parents are fixed: there is
    only one instance of any given parent under consideration. See the
    Magma test for an example of this being necessary. The hypothesis may
    not be true when there are recursive structures, since different values
    of the structure might not agree on parent fields.

• #7304 fixes an issue where nested let rec declarations within
  match expressions or tactic blocks failed to compile if they were
  nested within, and recursively called, a let rec that referenced a
  variable bound by a containing declaration.

• #7309 fixes a bug where bv_decide's new structure support would
  sometimes not case split on all available structure fvars as their type
  was an mvar.

• #7312 implements proof term generation for cooper_dvd_left and its
  variants in the cutsat procedure for linear integer arithmetic.

• #7314 changes elaboration of structure parents so that each must be
  fully elaborated before the next one is processed.

• #7315 implements the Cooper conflict resolution in cutsat. We still
  need to implement the backtracking and disequality case.

• #7324 changes the internal construction of well-founded recursion, to
  not change the type of fix’s induction hypothesis in non-defeq ways.

• #7329 adds support to bv_decide for simple pattern matching on enum
  inductives. By simple we mean non dependent match statements with all
  arms written out.

• #7333 allows aux decls (like generated by match) to be generated by
  decreasing_by tactics.

• #7335 modifies elabTerminationByHints in a way that the type of the
  recursive function used for elaboration of the termination measure is
  striped of from optional parameters. It prevents introducing
  dependencies between the default values for arguments, that can cause
  the termination checker to fail.

• #7339 implements cooper conflict resolution in the cutsat procedure.
  It also fixes several bugs in the proof term construction. We still need
  to add more tests, but we can already solve the following example that
  omega fails to solve:

  example (x y : Int) :
      27 ≤ 11*x + 13*y →
      11*x + 13*y ≤ 45 →
      -10 ≤ 7*x - 9*y →
      7*x - 9*y ≤ 4 → False := by
    grind

• #7347 upgrades the CaDiCal we ship and use for bv_decide to version
  2.1.2. Additionally it enables binary LRAT proofs on windows by default
  as arminbiere/cadical#112 has been fixed.

• #7348 ensures all equation and unfold theorem generators in core are
  compatible with parallelism.

• #7351 ensures cutsat does not have to perform case analysis in the
  univariate polynomial case. That it, it can close a goal whenever there
  is no solution for a divisibility constraint in an interval. Example of
  theorem that is now proved in a single step by cutsat:

  example (x : Int) : 100 ≤ x → x ≤ 10000 → 20000 ∣ 3*x → False := by
    grind

• #7353 changes abstractNestedProofs so that it also visits the
  subterms in the head of an application.

• #7355 fixes a bug in the markNestedProofs preprocessor used in the
  grind tactic.

• #7357 adds support for / and % to the cutsat procedure.

• #7362 allows simp dischargers to add aux decls to the environment.
  This enables tactics like native_decide to be used here, and unblocks
  improvements to omega in #5998.

• #7369 uses let-declarations for each polynomial occurring in a proof
  term generated by the cutsat procedure.

• #7370 simplifies the proof term due to the Cooper's conflict
  resolution in cutsat.

• #7373 implements the last missing case for the cutsat procedure and
  fixes a bug. During model construction, we may encounter a bounded
  interval containing integer solutions that satisfy the divisibility
  constraint but fail to satisfy known disequalities.

• #7381 refactors the AIG datastructures that underly bv_decide in order
  to allow a better tracking of negations in the circuit. This refactor
  has two effects, for one adding full constant folding to the AIG
  framework and secondly enabling us to add further simplifications from
  the Brummayer Biere paper...

v4.19.0-rc1

chore: normalize URLs to the language reference in test results

update tests

syntax

sigh

fix regex

allow rcs

v4.18.0

This is the v4.18.0 release of Lean.

v4.18.0-rc1

v4.18.0-rc1

For this release, 339 changes landed. In addition to the 166 feature additions and 37 fixes listed below there were 13 refactoring changes, 10 documentation improvements, 3 performance improvements, 4 improvements to the test suite and 105 other changes.

Language

• #6634 adds support for changing the binder annotations of existing
  variables to and from strict-implicit and instance-implicit using the
  variable command.

• #6741 implements two rules for bv_decide's preprocessor, lowering
  ||| to &&& in order to enable more term sharing + application of
  rules about &&& as well as rewrites of the form (a &&& b == -1#w) = (a == -1#w && b == -1#w) in order to preserve rewriting behavior that
  already existed before this lowering.

• #6744 extend the preprocessing of well-founded recursive definitions
  to bring assumptions like h✝ : x ∈ xs into scope automatically.

• #6770 enables code generation to proceed in parallel to further
  elaboration.

• #6823 adds a builtin tactic and a builtin attribute that are required
  for the tree map. The tactic, as_aux_lemma, can generally be used to
  wrap the proof term generated by a tactic sequence into a separate
  auxiliary lemma in order to keep the proof term small. This can, in rare
  cases, be necessary if the proof term will appear multiple times in the
  encompassing term. The new attribute, Std.Internal.tree_tac, is
  internal and should not be used outside of Std.

• #6853 adds support for anonymous equality proofs in match
  expressions of the form match _ : e with ....

• #6869 adds a recommended_spelling command, which can be used for
  recording the recommended spelling of a notation (for example, that the
  recommended spelling of ∧ in identifiers is and). This information
  is then appended to the relevant docstrings for easy lookup.

• #6891 modifies rewrite/rw to abort rewriting if the elaborated
  lemma has any immediate elaboration errors (detected by presence of
  synthetic sorries). Rewriting still proceeds if there are elaboration
  issues arising from pending synthetic metavariables, like instance
  synthesis failures. The purpose of the change is to avoid obscure
  "tactic 'rewrite' failed, equality or iff proof expected ?m.5" errors
  when for example a lemma does not exist.

• #6893 adds support for plugins to the frontend and server.

• #6902 ensures simp diagnostic information in included in the grind
  diagnostic message.

• #6924 adds the EQUAL_ITE rules from Bitwuzla to the preprocessor of
  bv_decide.

• #6926 adds the BV_EQUAL_CONST_NOT rules from Bitwuzla to the
  preprocessor of bv_decide.

• #6935 adds the tactic expose_names. It creates a new goal whose
  local context has been "exposed" so that every local declaration has a
  clear, accessible name. If no local declarations require renaming, the
  original goal is returned unchanged.

• #6936 fixes the #discr_tree_simp_key command, because it displays
  the keys for just lhs in lhs ≠ rhs, but it should be lhs = rhs,
  since that is what simp indexes.

• #6937 improves grind error and trace messages by cleaning up local
  declaration names.

• #6939 adds error messages for inductive declarations with
  conflicting constructor names and mutual declarations with conflicting
  names.

• #6940 improves how the grind tactic performs case splits on p <-> q.

• #6946 implements basic support for handling of enum inductives in
  bv_decide. It now supports equality on enum inductive variables (or
  other uninterpreted atoms) and constants.

• #6947 adds the binderNameHint gadget. It can be used in rewrite and
  simp rules to preserve a user-provided name where possible.

• #6951 adds line breaks and indentations to simp's trace messages to
  make them easier to read (IMHO).

• #6961 adds the auxiliary tactic evalAndSuggest. It will be used to
  refactor try?.

• #6964 adds a convenience command #info_trees in, which prints the
  info trees generated by the following command. It is useful for
  debugging or learning about InfoTree.

• #6965 re-implements the try? tactic using the new evalAndSuggest
  infrastructure.

• #6967 ensures try? can suggest tactics that need to reference
  inaccessible local names.
  Example:

  /--
  info: Try these:
  • · expose_names; induction as, bs_1 using app.induct <;> grind [= app]
  • · expose_names; induction as, bs_1 using app.induct <;> grind only [app]
  -/
  #guard_msgs (info) in
  example : app (app as bs) cs = app as (app bs cs) := by
    have bs := 20 -- shadows `bs` in the target
    try?

• #6979 adds support for more complex suggestions in try?. Example:

  example (as : List α) (a : α) : concat as a = as ++ [a] := by
    try?

  suggestion

  Try this: · induction as, a using concat.induct
    · rfl
    · simp_all
  

• #6980 improves the try? tactic runtime validation and error
  messages. It also simplifies the implementation, and removes unnecessary
  code.

• #6981 adds new configuration options to try?.

  • try? -only omits simp only and grind only suggestions
  • try? +missing enables partial solutions where some subgoals are
    "solved" using sorry, and must be manually proved by the user.
  • try? (max:=<num>) sets the maximum number of suggestions produced
    (default is 8).

• #6988 ensures interrupting the kernel does not lead to wrong, sticky
  error messages in the editor

• #6991 improves how suggestions for the <;> combinator are generated.

• #6994 adds the Try.Config.merge flag (true by default) to the
  try? tactic. When set to true, try? compresses suggestions such
  as:

  · induction xs, ys using bla.induct
      · grind only [List.length_reverse]
      · grind only [bla]

  into:

  induction xs, ys using bla.induct <;> grind only [List.length_reverse, bla]

• #6995 implements support for exact? in the try? tactic.

• #7000 adds helper theorems for justifying the linear integer
  normalizer.

• #7002 implements the normalizer for linear integer arithmetic
  expressions. It is not connect to simp +arith yet because of some
  spurious [simp] attributes.

• #7009 ensures users get an error message saying which module to import
  when they try to use bv_decide.

• #7011 adds simp +arith for integers. It uses the new grind
  normalizer for linear integer arithmetic. We still need to implement
  support for dividing the coefficients by their GCD. It also fixes
  several bugs in the normalizer.

• #7015 makes sure simp +arith normalizes coefficients in linear
  integer polynomials. There is still one todo: tightening the bound of
  inequalities.

• #7019 properly spells out the trace nodes in bv_decide so they are
  visible with just trace.Meta.Tactic.bv and trace.Meta.Tactic.sat
  instead of always having to enable the profiler.

• #7021 adds theorems for interactions of extractLsb with &&&, ^^^,
  ~~~ and bif to bv_decide's preprocessor.

• #7029 adds simprocs to bv_decide's preprocessor that rewrite
  multiplication with powers of two to constant shifts.

• #7030 adds completes the linear integer inequality normalizer for
  grind. The missing normalization step replaces a linear inequality of
  the form a_1*x_1 + ... + a_n*x_n + b <= 0 with a_1/k * x_1 + ... + a_n/k * x_n + ceil(b/k) <= 0 where k = gcd(a_1, ..., a_n).
  ceil(b/k) is implemented using the helper cdiv b k.

• #7033 improves presentation of counter examples for UIntX and enum
  inductives in bv_decide.

• #7039 improves the well-founded definition preprocessing to propagate
  wfParam through let expressions.
  ...

v4.17.0

v4.17.0

For this release, 319 changes landed. In addition to the 168 feature additions and 57 fixes listed below there were 12 refactoring changes, 13 documentation improvements and 56 chores.

Highlights

The Lean v4.17 release brings a range of new features, performance improvements,
and bug fixes. Notable user-visible updates include:

• #6368 implements executing kernel checking in parallel to elaboration,
  which is a prerequisite for parallelizing elaboration itself.

• #6711 adds support for UIntX and USize in bv_decide by adding a
  preprocessor that turns them into BitVec of their corresponding size.

• #6505 implements a basic async framework as well as asynchronously
  running timers using libuv.

• improvements to documentation with docgen, which now links dot notations (#6703), coerced functions (#6729), and tokens (#6730).

• extensive library development, in particular, expanding verification APIs of BitVec,
  making APIs of List / Array / Vector consistent, and adding lemmas describing the behavior of UInt.

• #6597 fixes the indentation of nested traces nodes in the info view.

New Language Features

• Partial Fixpoint

  #6355 adds the ability to define possibly non-terminating functions
  and still be able to reason about them equationally, as long as they are
  tail-recursive, or operate within certain monads such as Option

  Typical examples:

  def ack : (n m : Nat) → Option Nat
    | 0,   y   => some (y+1)
    | x+1, 0   => ack x 1
    | x+1, y+1 => do ack x (← ack (x+1) y)
  partial_fixpoint
  
  def whileSome (f : α → Option α) (x : α) : α :=
    match f x with
    | none => x
    | some x' => whileSome f x'
  partial_fixpoint
  
  def computeLfp {α : Type u} [DecidableEq α] (f : α → α) (x : α) : α :=
    let next := f x
    if x ≠ next then
      computeLfp f next
    else
      x
  partial_fixpoint

  See the reference manual
  for more details.

• #6905 adds a first draft of the try?
  interactive tactic, which tries various tactics, including induction:

  @[simp] def revAppend : List Nat → List Nat → List Nat
  | [],    ys => ys
  | x::xs, ys => revAppend xs (x::ys)
  
  example : (revAppend xs ys).length = xs.length + ys.length := by
    try?
    /-
    Try these:
    • · induction xs, ys using revAppend.induct
        · simp
        · simp +arith [*]
    • · induction xs, ys using revAppend.induct
        · simp only [revAppend, List.length_nil, Nat.zero_add]
        · simp +arith only [revAppend, List.length_cons, *]
    -/

• induction with zero alternatives

  #6486 modifies the induction/cases syntax so that the with
  clause does not need to be followed by any alternatives. This improves
  friendliness of these tactics, since this lets them surface the names of
  the missing alternatives:

  example (n : Nat) : True := by
    induction n with
  /-            ~~~~
  alternative 'zero' has not been provided
  alternative 'succ' has not been provided
  -/

• simp? and dsimp? tactics in conversion mode

  #6593 adds support for the simp? and dsimp? tactics in conversion
  mode.

• fun_cases

  #6261 adds foo.fun_cases, an automatically generated theorem that
  splits the goal according to the branching structure of foo, much like
  the Functional Induction Principle, but for all functions (not just
  recursive ones), and without providing inductive hypotheses.

New CLI Features

• #6427 adds the Lean CLI option --src-deps which parallels --deps.
  It parses the Lean code's header and prints out the paths to the
  (transitively) imported modules' source files (deduced from
  LEAN_SRC_PATH).

• #6323 adds a new Lake CLI command, lake query, that both builds
  targets and outputs their results. It can produce raw text or JSON
  -formatted output (with --json / -J).

Breaking Changes

• #6602 allows the dot ident notation to resolve to the current
  definition, or to any of the other definitions in the same mutual block.
  Existing code that uses dot ident notation may need to have nonrec
  added if the ident has the same name as the definition.

• Introduction of the zetaUnused simp and reduction option (#6755)
  is a breaking change in rare cases: the split tactic no longer removes unused let and have expressions as a side-effect.
  dsimp only can be used to remove unused have and let expressions.

This highlights section was contributed by Violetta Sim.

Language

• #5145 splits the environment used by the kernel from that used by the
  elaborator, providing the foundation for tracking of asynchronously
  elaborated declarations, which will exist as a concept only in the
  latter.

• #6261 adds foo.fun_cases, an automatically generated theorem that
  splits the goal according to the branching structure of foo, much like
  the Functional Induction Principle, but for all functions (not just
  recursive ones), and without providing inductive hypotheses.

• #6355 adds the ability to define possibly non-terminating functions
  and still be able to reason about them equationally, as long as they are
  tail-recursive or monadic.

• #6368 implements executing kernel checking in parallel to elaboration,
  which is a prerequisite for parallelizing elaboration itself.

• #6427 adds the Lean CLI option --src-deps which parallels --deps.
  It parses the Lean code's header and prints out the paths to the
  (transitively) imported modules' source files (deduced from
  LEAN_SRC_PATH).

• #6486 modifies the induction/cases syntax so that the with
  clause does not need to be followed by any alternatives. This improves
  friendliness of these tactics, since this lets them surface the names of
  the missing alternatives:

  example (n : Nat) : True := by
    induction n with
  /-            ~~~~
  alternative 'zero' has not been provided
  alternative 'succ' has not been provided
  -/

• #6505 implements a basic async framework as well as asynchronously
  running timers using libuv.

• #6516 enhances the cases tactic used in the grind tactic and
  ensures that it can be applied to arbitrary expressions.

• #6521 adds support for activating relevant match-equations as
  E-matching theorems. It uses the match-equation lhs as the pattern.

• #6528 adds a missing propagation rule to the (WIP) grind tactic.

• #6529 adds support for let-declarations to the (WIP) grind tactic.

• #6530 fixes nondeterministic failures in the (WIP) grind tactic.

• #6531 fixes the support for let_fun in grind.

• #6533 adds support to E-matching offset patterns. For example, we want
  to be able to E-match the pattern f (#0 + 1) with term f (a + 2).

• #6534 ensures that users can utilize projections in E-matching
  patterns within the grind tactic.

• #6536 fixes different thresholds for controlling E-matching in the
  grind tactic.

• #6538 ensures patterns provided by users are normalized. See new test
  to understand why this is needed.

• #6539 introduces the [grind_eq] attribute, designed to annotate
  equational theorems and functions for heuristic instantiations in the
  grind tactic.
  When applied to an equational theorem, the [grind_eq] attribute
  instructs the grind tactic to automatically use the annotated theorem
  to instantiate patterns during proof search. If applied to a function,
  it marks all equational theorems associated with that function.

• #6543 adds additional tests for grind, demonstrating that we can
  automate some manual proofs from Mathlib's basic category theory
  library, with less reliance on Mathlib's @[reassoc] trick.

• #6545 introduces the parametric attribute [grind] for annotating
  theorems and definitions. It also replaces [grind_eq] with [grind =]. For definitions, [grind] is equivalent to [grind =].

• #6556 adds propagators for implic...