v4.4.0-rc1

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 and lean using the leanOptions config field. Setting either of these fields instead of moreServerArgs ensures that viewing files from a dependency uses the options for that dependency. Additionally, moreServerArgs is being deprecated in favor of the moreGlobalServerArgs 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⟩]

• Rename request handler.

• Import auto-completion.

• pp.beta to apply beta reduction when pretty printing.

• Embed and check githash in .olean.

• Guess lexicographic order for well-founded recursion.

• Allow trailing comma in tuples, lists, and tactics.

Bug fixes for #2628, #2883,
#2810, #2925, and #2914.

Lake:

• lake init . and a bare lake init and will now use the current directory as the package name. #2890
• lake new and lake init will now produce errors on invalid package names such as .., foo/bar, Init, Lean, Lake, and Main. 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 named bar.* rather than Bar.*). See issue #2567 and PR #2889.
• Lean and Lake now properly support non-identifier library names (e.g., lake new 123-hello and import «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 via elab 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 parses target 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 named foo-bar and lake new foo.bar exe properly creates foo/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 in ite docstring by @AdrienChampion in #2924
• fix: eq_refl tactic’s name is eqRefl 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