v4.4.0-rc1
Pre-release
Pre-release
github-actions
released this
30 Nov 04:01
·
2264 commits
to master
since this release
Changes since v4.3.0 (from RELEASES.md):
-
Lake and the language server now support per-package server options using the
moreServerOptions
config field, as well as options that apply to both the language server andlean
using theleanOptions
config field. Setting either of these fields instead ofmoreServerArgs
ensures that viewing files from a dependency uses the options for that dependency. Additionally,moreServerArgs
is being deprecated in favor of themoreGlobalServerArgs
field. See PR #2858.A Lakefile with the following deprecated package declaration:
def moreServerArgs := #[ "-Dpp.unicode.fun=true" ] def moreLeanArgs := moreServerArgs package SomePackage where moreServerArgs := moreServerArgs moreLeanArgs := moreLeanArgs
... can be updated to the following package declaration to use per-package options:
package SomePackage where leanOptions := #[⟨`pp.unicode.fun, true⟩]
Bug fixes for #2628, #2883,
#2810, #2925, and #2914.
Lake:
lake init .
and a barelake init
and will now use the current directory as the package name. #2890lake new
andlake init
will now produce errors on invalid package names such as..
,foo/bar
,Init
,Lean
,Lake
, andMain
. See issue #2637 and PR #2890.lean_lib
no longer converts its name to upper camel case (e.g.,lean_lib bar
will include modules namedbar.*
rather thanBar.*
). See issue #2567 and PR #2889.- Lean and Lake now properly support non-identifier library names (e.g.,
lake new 123-hello
andimport «123Hello»
now work correctly). See issue #2865 and PR #2889. - Lake now filters the environment extensions loaded from a compiled configuration (
lakefile.olean
) to include only those relevant to Lake's workspace loading process. This resolves segmentation faults caused by environment extension type mismatches (e.g., when defining custom elaborators viaelab
in configurations). See issue #2632 and PR #2896. - Cloud releases will now properly be re-unpacked if the build directory is removed. See PR #2928.
- Lake's
math
template has been simplified. See PR #2930. lake exe <target>
now parsestarget
like a build target (as the help text states it should) rather than as a basic name. For example,lake exe @mathlib/runLinter
should now work. See PR #2932.lake new foo.bar [std]
now generates executables namedfoo-bar
andlake new foo.bar exe
properly createsfoo/bar.lean
. See PR #2932.- Later packages and libraries in the dependency tree are now preferred over earlier ones. That is, the later ones "shadow" the earlier ones. Such an ordering is more consistent with how declarations generally work in programming languages. This will break any package that relied on the previous ordering. See issue #2548 and PR #2937.
- Executable roots are no longer mistakenly treated as importable. They will no longer be picked up by
findModule?
. See PR #2937.
Pull requests merged:
- chore: update release notes after v4.3.0-rc2 by @semorrison in #2891
- chore: Issue template: Suggest
#eval Lean.versionString
by @nomeata in #2884 - fix: support non-identifier library names by @tydeu in #2888
- refactor: lake: use plain lib name for root and native name by @tydeu in #2889
- feat: bare
lake init
& validated pkg names by @tydeu in #2890 - Allow trailing comma in tuples, lists, and tactics by @vleni in #2643
- chore: syntax documentation for
universe
,open
,export
,variable
by @AdrienChampion in #2645 - fix: lake: whitelist loaded config olean env exts by @tydeu in #2896
- chore: ignore forgotten Lake test artifacts by @tydeu in #2886
- doc: fix typos by @marcusrossel in #2915
- fix: DecidableEq deriving handler could not handle fields whose types start with an implicit argument by @kmill in #2918
- doc: release notes for recent lake fixes by @tydeu in #2906
- fix: PackMutual: Deal with extra arguments by @nomeata in #2892
- feat:
Lean.MVarId.cleanup
configuration by @kmill in #2919 - feat: helpful error message about supportInterpreter by @semorrison in #2912
- doc: Adjust contributor's docs to squash merging by @nomeata in #2927
- feat: rename request handler by @digama0 in #2462
- doc: mention
dite
inite
docstring by @AdrienChampion in #2924 - fix:
eq_refl
tactic’s name iseqRefl
by @nomeata in #2911 - refactor: WF.Fix: Pass all remaining goals to
Term.reportUnsolvedGoals
by @nomeata in #2922 - chore: run CI on merge_group by @semorrison in #2948
- fix: most-recently-nightly-tag does not assume a 'nightly' remote by @semorrison in #2947
- fix: Use whnf for mutual recursion with types hiding
→
by @nomeata in #2926 - chore: CI: pin macos-11 to work around 12.7.1 breakage by @Kha in #2946
- fix: Float RecApp out of applications by @nomeata in #2818
- fix:
PackMutual
: Eta-Expand as needed by @nomeata in #2902 - chore: script/most-recent-nightly-tag uses https rather than ssh repo URL by @semorrison in #2951
- chore: Run CI on all PRs, even base ≠ master by @nomeata in #2955
- doc: Markdown fixes in Lean.Expr by @nomeata in #2956
- feat: import auto-completion by @mhuisi in #2904
- chore: remove unused MonadBacktrack instance for SimpM by @semorrison in #2943
- feat:
pp.beta
to apply beta reduction when pretty printing by @kmill in #2864 - feat: per-package server options by @mhuisi in #2858
- fix: ignore errors on
IO.FS.Handle
finalization by @Kha in #2935 - feat: embed and check githash in .olean by @Kha in #2766
- fix: missing withContext in simp trace by @digama0 in #2053
- feat: Add MatcherApp. and CasesOnApp.refineThrough by @nomeata in #2882
- fix: untar cloud release if no build dir by @tydeu in #2928
- fix: lake: proper exe targets & pkg generation by @tydeu in #2932
- refactor: reverse pkg/lib search & no exe roots in import by @tydeu in #2937
- feat: Guess lexicographic order for well-founded recursion by @nomeata in #2874
- refactor: lake: simplify math template & test it by @tydeu in #2930
- doc: release notes for recent lake changes by @tydeu in #2938
- feat: WF.GuessLex: If there is only one plausible measure, use it by @nomeata in #2954
- fix: remove unnecessary step in pr-release.yml by @semorrison in #2976
- chore: Check PR title, not commit, for commit convention by @nomeata in #2978
- chore: CI: Create an all-builds-ok job by @nomeata in #2983
- chore: remove supportInterpreter from lake template by @semorrison in #2984
New Contributors
- @vleni made their first contribution in #2643
Full Changelog: v4.3.0...v4.4.0-rc1