Skip to content

v4.5.0
Compare
Choose a tag to compare
@github-actions github-actions released this 01 Feb 03:02
· 2048 commits to master since this release
v4.5.0
1a3021f

Changes since v4.4.0 (from RELEASES.md)

  • Modify the lexical syntax of string literals to have string gaps, which are escape sequences of the form "\" newline whitespace*.
    These have the interpetation of an empty string and allow a string to flow across multiple lines without introducing additional whitespace.
    The following is equivalent to "this is a string".

    "this is \
   a string"

    PR #2821 and RFC #2838.

  • Add raw string literal syntax. For example, r"\n" is equivalent to "\\n", with no escape processing.
    To include double quote characters in a raw string one can add sufficiently many # characters before and after
    the bounding "s, as in r#"the "the" is in quotes"# for "the \"the\" is in quotes".
    PR #2929 and issue #1422.

  • The low-level termination_by' clause is no longer supported.

    Migration guide: Use termination_by instead, e.g.:

    -termination_by' measure (fun ⟨i, _⟩ => as.size - i)
+termination_by i _ => as.size - i

    If the well-founded relation you want to use is not the one that the
    WellFoundedRelation type class would infer for your termination argument,
    you can use WellFounded.wrap from the std libarary to explicitly give one:

    -termination_by' ⟨r, hwf⟩
+termination_by x => hwf.wrap x

  • Support snippet edits in LSP TextEdits. See Lean.Lsp.SnippetString for more details.

  • Deprecations and changes in the widget API.

    • Widget.UserWidgetDefinition is deprecated in favour of Widget.Module. The annotation @[widget] is deprecated in favour of @[widget_module]. To migrate a definition of type UserWidgetDefinition, remove the name field and replace the type with Widget.Module. Removing the name results in a title bar no longer being drawn above your panel widget. To add it back, draw it as part of the component using <details open=true><summary class='mv2 pointer'>{name}</summary>{rest_of_widget}</details>. See an example migration here.
    • The new command show_panel_widgets allows displaying always-on and locally-on panel widgets.
    • RpcEncodable widget props can now be stored in the infotree.
    • See RFC 2963 for more details and motivation.

  • If no usable lexicographic order can be found automatically for a termination proof, explain why.
    See feat: GuessLex: if no measure is found, explain why.

  • Option to print inferred termination argument.
    With set_option showInferredTerminationBy true you will get messages like

    Inferred termination argument:
termination_by
ackermann n m => (sizeOf n, sizeOf m)

    for automatically generated termination_by clauses.

  • More detailed error messages for invalid mutual blocks.

  • Multiple improvements to the output of simp? and simp_all?.

  • Tactics with withLocation * no longer fail if they close the main goal.

  • Implementation of a test_extern command for writing tests for @[extern] and @[implemented_by] functions.
    Usage is

    import Lean.Util.TestExtern

test_extern Nat.add 17 37

    The head symbol must be the constant with the @[extern] or @[implemented_by] attribute. The return type must have a DecidableEq instance.

Bug fixes for
#2853, #2953, #2966,
#2971, #2990, #3094.

Bug fix for eager evaluation of default value in Option.getD.
Avoid panic in leanPosToLspPos when file source is unavailable.
Improve short-circuiting behavior for List.all and List.any.

Several Lake bug fixes: #3036, #3064, #3069.

What's Changed

  • doc: Improve docstrings around Array.mk,.data,.toList by @nomeata in #2771
  • chore: make PR title check work as a merge_group check by @nomeata in #2987
  • chore: trim CI set by default by @nomeata in #2986
  • chore: update stage0 by @mhuisi in #2992
  • test: termination checking and duplicated terms by @nomeata in #2993
  • refactor: CasesOnApp.refineThrough can return a lambda, not an open term by @nomeata in #2974
  • chore: begin development cycle for v4.5.0 by @semorrison in #2995
  • doc: VS Code dev setup by @Kha in #2961
  • doc: fix typos by @marcusrossel in #2996
  • fix: find macOS system libraries in leanc by @Kha in #2997
  • chore: CI: in quick mode, only Nix build runs the tests by @nomeata in #2998
  • chore: CI: update github-script by @Kha in #3002
  • chore: run CI on new labels by @nomeata in #3003
  • chore: fix CPP warnings about static_assert by @nomeata in #3005
  • chore: improve tests/lean/copy-produced by @nomeata in #3006
  • fix: missing whnf in mkBelowBinder and mkMotiveBinder by @arthur-adjedj in #2991
  • doc: fix recent issue links in RELEASES.md by @tydeu in #3000
  • test: expand tests/lean/issue2981.lean a bit by @nomeata in #3007
  • chore: run tests with full-ci by @nomeata in #3009
  • refactor: rewrite TerminationHint elaborators by @nomeata in #2958
  • chore: Nix CI: update setup by @Kha in #3015
  • doc: In testing doc, suggest make to pick up new tests by @nomeata in #2815
  • chore: add vscode cmake configuration by @eric-wieser in #3008
  • doc: typo Runnign by @nomeata in #3018
  • refactor: WF.Fix: gather subgoals by @nomeata in #3017
  • feat: GuessLex: if no measure is found, explain why by @nomeata in #2960
  • feat: GuessLex: print inferred termination argument by @nomeata in #3012
  • doc: add migration guide for per-package server options by @mhuisi in #3025
  • feat: detail error message about invalid mutual blocks by @odanoburu in #2949
  • doc: fix MetavarContext markdown by @nomeata in #3026
  • chore: set warningAsError in CI only by @Kha in #3030
  • fix: WF.Fix: deduplicate subsumed goals before running tactic by @nomeata in #3024
  • feat: string gaps for continuing string literals across multiple lines by @kmill in #2821
  • fix: GuessLex: deduplicate recursive calls by @nomeata in #3004
  • doc: document constructors of TransparencyMode by @eric-wieser in #3037
  • chore: update stage0 by @nomeata in #3041
  • chore: remove obsolete comment in test by @nomeata in #3044
  • doc: explain how to use custom lexers in the latest minted by @eric-wieser in #3047
  • chore: stage0 autoupdater action by @nomeata in #3042
  • fix: Option.getD eagerly evaluates dflt by @digama0 in #3043
  • feat: drop support for termination_by' by @nomeata in #3033
  • chore: make List.all and List.any short-circuit by @semorrison in #2972
  • chore: fix superfluous lemmas in simp.trace by @semorrison in #2923
  • fix: omit fvars from simp_all? theorem list by @JLimperg in #2969
  • chore: refactor pr release workflow by @nomeata in #3020
  • chore: withLocation * should not fail if it closes the main goal by @semorrison in #2917
  • fix: move Lean.List.toSMap to List.toSMap by @digama0 in #3035
  • fix: run_task/deactivate_task race condition on m_imp->m_closure by @Kha in #2959
  • doc: update quickstart guide to reference vs code setup guide by @mhuisi in #2968
  • chore: robustify PR release workflow by @nomeata in #3051
  • chore: do not use actions-ecosystem/action-add-labels by @nomeata in #3055
  • feat: test_extern command by @semorrison in #2970
  • fix: lake: re-elab if config olean is missing by @tydeu in #3036
  • chore: pr-release.yaml: remove hardcoded date by @nomeata in #3061
  • fix: lake: leave run options for script by @tydeu in #3064
  • chore: pr-release.yml: use API to get pull request number by @nomeata in #3066
  • chore: refactor pr-release.yml to avoid 'await' by @semorrison in #3070
  • chore: add the lean4 extension to the vscode workspace by @eric-wieser in #3059
  • doc: mention x:h@e variant in docstring of x@e by @eric-wieser in #3073
  • chore: allow updating stage0 via workflow_dispatch by @nomeata in #3052
  • chore: pr-release: revert to originally used action to get PR number by @nomeata in #3072
  • fix: don't panic in leanPosToLspPos by @semorrison in #3071
  • fix: reference implementation ByteArray.copySlice by @semorrison in #2967
  • doc: fix typos/indentation by @marcusrossel in #3085
  • doc: Bold "Diaconescu's theorem" by @hmonroe in #3086
  • feat: encode let_fun using a letFun function by @kmill in #2973
  • refactor: generalize some simp methods by @leodemoura in #3088
  • refactor: move unpackArg etc. to WF.PackDomain/WF.PackMutual by @nomeata in #3077
  • chore: refine PR template by @nomeata in #3074
  • perf: improve avoidance of repeated Expr visits in unused variables linter by @Kha in #3076
  • feat: add quot_precheck for expression tree elaborators (binop%, etc.) by @kmill in #3078
  • fix: fixing path of the generated binary in documentation by @lu-bulhoes in #3093
  • fix: lake: save config trace before elab by @tydeu in #3069
  • feat: snippet extension by @Vtec234 in #3054
  • chore: pr-release: Also work with older tags by @nomeata in #3097
  • feat: Rust-style raw string literals by @kmill in #2929
  • feat: bundle of widget improvements by @Vtec234 in #2964
  • chore: default compiler.enableNew to false until development restarts by @Kha in #3034
  • doc: avoid universe issue in example type class code by @nomeata in #3098

New Contributors

Full Changelog: v4.4.0...v4.5.0

Contributors

Kha, nomeata, and 14 other contributors
Assets 16
Loading