Skip to content

v4.2.0
Compare
Choose a tag to compare
@github-actions github-actions released this 31 Oct 03:20
· 2452 commits to master since this release
v4.2.0
0d70514

v4.2.0

  • isDefEq cache for terms not containing metavariables..
  • Make Environment.mk and Environment.add private, and add replay as a safer alternative.
  • IO.Process.output no longer inherits the standard input of the caller.
  • Do not inhibit caching of default-level match reduction.
  • List the valid case tags when the user writes an invalid one.
  • The derive handler for DecidableEq now handles mutual inductive types.
  • Show path of failed import in Lake.
  • Fix linker warnings on macOS.
  • Lake: Add postUpdate? package configuration option. Used by a package to specify some code which should be run after a successful lake update of the package or one of its downstream dependencies. (lake#185)
  • Improvements to Lake startup time (#2572, #2573)
  • refine e now replaces the main goal with metavariables which were created during elaboration of e and no longer captures pre-existing metavariables that occur in e (#2502).
    • This is accomplished via changes to withCollectingNewGoalsFrom, which also affects elabTermWithHoles, refine', calc (tactic), and specialize. Likewise, all of these now only include newly-created metavariables in their output.
    • Previously, both newly-created and pre-existing metavariables occurring in e were returned inconsistently in different edge cases, causing duplicated goals in the infoview (issue #2495), erroneously closed goals (issue #2434), and unintuitive behavior due to refine e capturing previously-created goals appearing unexpectedly in e (no issue; see PR).

Merged PRs

  • Add new issue templates by @mhuisi in #2519
  • chore: begin development cycle for 4.2.0 by @semorrison in #2545
  • chore: do not generate PR releases from forks by @semorrison in #2550
  • chore: when bumping Mathlib testing branches, bump to latest nightly-testing by @semorrison in #2553
  • fix: uninterpolated error message in registerRpcProcedure by @thorimur in #2547
  • Enforce linebreak between calc steps by @Kha in #2532
  • fix: rename parameter of withImportModules to match doc string by @dwrensha in #2530
  • perf: reduce allocations in unused variable linter by @hargoniX in #2491
  • fix: set MACOSX_DEPLOYMENT_TARGET in CI only by @Kha in #2556
  • CI: label stale PRs by @Kha in #2561
  • chore: disambiguate whnf system category by @Kha in #2560
  • fix: use MoveFileEx for rename on win by @digama0 in #2546
  • fix: set ref in getCalcFirstStep by @PatrickMassot in #2563
  • perf: Use flat ByteArrays in Trie by @nomeata in #2529
  • chore: update domain by @Kha in #2566
  • feat: lake: add name to manifest by @tydeu in #2565
  • fix: only return new mvars from refine, elabTermWithHoles, and withCollectingNewGoalsFrom by @thorimur in #2502
  • fix: don't try to generate below for nested predicates. by @arthur-adjedj in #2390
  • perf: do not detect lean's toolchain by @tydeu in #2570
  • test: add lake benchmarks by @tydeu in #2457
  • perf: lake: build lakefile environments incrementally by @Kha in #2573
  • perf: lake: no lean --githash when collocated by @tydeu in #2572
  • test: lake: add env & dep cfg benchmarks + cleanup by @tydeu in #2574
  • perf: lake: lazily acquire repo URL/tag in :release by @tydeu in #2583
  • doc: add token error change to RELEASES.md by @Kha in #2579
  • chore: begin development cycle for v4.3.0 by @semorrison in #2585
  • fix: hover term/tactic confusion by @digama0 in #2586
  • doc: fix doc comment syntax in declModifiers doc comment by @nomeata in #2590
  • chore: add release note about lake startup time by @semorrison in #2597
  • chore: Remove unused variables from kernel by @nomeata in #2576
  • Fix typos by @DenisGorbachev in #2605
  • docs: update RELEASES.md for #2502 by @thorimur in #2606
  • [Backport releases/v4.2.0] docs: update RELEASES.md for #2502 by @github-actions in #2613
  • refactor: remove redundant let by @DenisGorbachev in #2614
  • Fix linker warnings on macOS by @Kha in #2598
  • feat : derive DecidableEq for mutual inductives by @arthur-adjedj in #2591
  • fix: withLocation should use withMainContext for target by @alexjbest in #2607
  • fix: XML parsing bugs by @kuruczgy in #2601
  • feat: Web Assembly Build by @abentkamp in #2599
  • feat: make Environment.mk private by @digama0 in #2604
  • doc: fix the link to contribution guidelines by @DenisGorbachev in #2623
  • feat: show path of failed import by @bollu in #2616
  • doc: add missing character in testing.md by @david-christiansen in #2630
  • Tag names by @david-christiansen in #2629
  • fix: eliminate widestring uses by @Kha in #2633
  • chore: fix typos in comments by @int-y1 in #2636
  • chore: fix more typos in comments by @int-y1 in #2638
  • perf: do not inhibit caching of default-level match reduction by @Kha in #2612
  • chore: add missing if statements to pr-release.yml workflow by @semorrison in #2639
  • chore: fix MVarId.getType' by @semorrison in #2595
  • chore: add axiom for tracing use of reduceBool / reduceNat by @semorrison in #2654
  • feat: replay constants into an Environment by @semorrison in #2617
  • chore: remove unnecessary partial in ForEachExpr.visit by @digama0 in #2657
  • chore: change trustCompiler axiom to True by @semorrison in #2662
  • Add development process docs by @david-christiansen in #2650
  • fix: treat pretty-printed names as strings by @Vtec234 in #2652
  • feat: ToMessageData (α × β) instance by @digama0 in #2658
  • fix: implementation of Array.anyMUnsafe by @semorrison in #2641
  • perf: use quick_is_def_eq first by @digama0 in #2671
  • chore: make Environment.add private by @semorrison in #2642
  • fix: quot reduction bug by @digama0 in #2673
  • fix: stdin := .null in IO.Process.output by @tydeu in #2544
  • test: lake: show module with failed import by @tydeu in #2677
  • feat: lake: postUpdate? + test by @tydeu in #2603
  • Cancel outstanding tasks on document edit in the language server by @Kha in #2648
  • feat: lake: --no-build option to exit before a build by @tydeu in #2651
  • Machinery for opt-in builds in language server by @Kha in #2665
  • fix : make mk_no_confusion_type handle delta-reduction when generating telescope by @arthur-adjedj in #2501
  • isDefEq cache for terms not containing metavariables. by @leodemoura in #2644
  • chore: simp tracing reports ← by @semorrison in #2621
  • feat: use nat_gcd in the kernel by @semorrison in #2533
  • chore: add items to RELEASES.md by @semorrison in #2687
  • fix: pp projection indices starting at 1 by @digama0 in #2691
  • chore: update RELEASES.md to reflect v4.2.0-rc2 by @semorrison in #2692
  • refactor: env extensions can only modify .extensions by @digama0 in #2661
  • chore: add an explicit branch name to leanlaketest_clone by @david-christiansen in #2693
  • chore: lake: test fixes by @tydeu in #2653
  • Fix typos in specialize.cpp by @sadikkuzu in #2702
  • Revert "Cancel outstanding tasks on document edit in the language server" by @semorrison in #2703

Contributors

% git log v4.1.0..v4.2.0 --pretty="%an" | sort | uniq -c | sort -rn
  26 Sebastian Ullrich
  23 Scott Morrison
  20 Mac Malone
   9 Mario Carneiro
   7 Marc Huisinga
   6 Leonardo de Moura
   4 David Christiansen
   3 Thomas Murrills
   3 Joachim Breitner
   3 Denis Gorbachev
   3 Arthur Adjedj
   2 int-y1
   2 David Thrane Christiansen
   1 kuruczgy
   1 Wojciech Nawrocki
   1 Siddharth
   1 Sadik Kuzu
   1 Patrick Massot
   1 Mac Malone
   1 Henrik
   1 David Renshaw
   1 Alexander Bentkamp
   1 Alex J Best

New Contributors

Full Changelog: v4.1.0...v4.2.0

Contributors

Kha, david-christiansen, and 19 other contributors
Assets 12
Loading