v4.8.0-rc1 discussion

Stream: general

[Floris van Doorn]

Let's discuss the new release here

[Floris van Doorn]

This is a great new release!
Even the new def-eq changes that I've seen look good. I looked through a few failing and succeeding def-eq traces, and there seems to be room for speedups. I don't have time to find another minimal example in the next 2 weeks, but after that I'll see if I can see if I can minimize some other non-optimal behavior.

Non-minimal example

Here is an example where the trace seems to show the elaborator do a few very similar tasks, each taking a few seconds each to fail. Probably I'm recording this mostly for myself, to look at this again in a few weeks.

import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace

open Set ChartedSpace SmoothManifoldWithCorners
open scoped Topology Manifold
variable {𝕜 : Type*}
  [NontriviallyNormedField 𝕜]
    -- declare a smooth manifold `M` over the pair `(E, H)`.
  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
  {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
  [SmoothManifoldWithCorners I M]
    -- declare a smooth manifold `M'` over the pair `(E', H')`.
  {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
  [SmoothManifoldWithCorners I' M']
    -- declare a smooth manifold `N` over the pair `(F, G)`.
  {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type*} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G}
  {N : Type*} [TopologicalSpace N] [ChartedSpace G N]
  [SmoothManifoldWithCorners J N]
    -- declare a smooth manifold `N'` over the pair `(F', G')`.
  {F' : Type*} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type*} [TopologicalSpace G']
  {J' : ModelWithCorners 𝕜 F' G'} {N' : Type*} [TopologicalSpace N'] [ChartedSpace G' N']
  [SmoothManifoldWithCorners J' N']
    -- F₁, F₂, F₃, F₄ are normed spaces
  {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type*} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂]
  {F₃ : Type*} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {F₄ : Type*} [NormedAddCommGroup F₄]
  [NormedSpace 𝕜 F₄]
    -- declare functions, sets, points and smoothness indices
  {f f₁ : M → M'} {s t : Set M} {x : M} {m n : ℕ∞}

set_option profiler true
set_option trace.profiler true
count_heartbeats in
theorem ContMDiffWithinAt.cle_arrowCongr' {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄}
    {s : Set M} {x : M}
    (hf : ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n (fun x ↦ ((f x).symm : F₂ →L[𝕜] F₁)) s x)
    (hg : ContMDiffWithinAt I 𝓘(𝕜, F₃ →L[𝕜] F₄) n (fun x ↦ (g x : F₃ →L[𝕜] F₄)) s x) :
    ContMDiffWithinAt I 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄)) n
      (fun y ↦ (f y).arrowCongr (g y) : M → (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄)) s x :=
  show ContMDiffWithinAt I 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄)) n
    (fun y ↦ (((f y).symm : F₂ →L[𝕜] F₁).precomp F₄).comp ((g y : F₃ →L[𝕜] F₄).postcomp F₁)) s x
  from hf.clm_precomp.clm_comp hg.clm_postcomp

/- the following has an intentional mistake, and is even slower before it fails. -/
count_heartbeats in
theorem ContMDiffWithinAt.cle_arrowCongr'' {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄}
    {s : Set M} {x : M}
    (hf : ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n (fun x ↦ ((f x).symm : F₂ →L[𝕜] F₁)) s x)
    (hg : ContMDiffWithinAt I 𝓘(𝕜, F₃ →L[𝕜] F₄) n (fun x ↦ (g x : F₃ →L[𝕜] F₄)) s x) :
    ContMDiffWithinAt I 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄)) n
      (fun y ↦ (f y).arrowCongr (g y) : M → (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄)) s x :=
  show ContMDiffWithinAt I 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄)) n
    (fun y ↦ (((f y).symm : F₂ →L[𝕜] F₁).precomp F₃).comp ((g y : F₃ →L[𝕜] F₄).postcomp F₁)) s x
  from hf.clm_precomp.clm_comp hg.clm_postcomp

[Ruben Van de Velde]

Has docgen been updated yet?

[Patrick Stevens]

(For those like me who didn't know what "functional induction" was, the first PR for this feature seems to be https://github.com/leanprover/lean4/pull/3432 which has a nice example of when to use it.)

[Kyle Miller]

The pretty printer now uses dot notation by default, so no need for @[pp_dot] anymore in mathlib (#12609 deprecates it)

[François G. Dorais]

The lake update lean4#3835 is very big! Looks like some major improvements! It will take a while to digest...

Quick question: how do you properly use download in a lake script now?

Old script snippet:

for file in ["UnicodeData.txt", "PropList.txt"] do
     let url := "https://www.unicode.org/Public/UCD/latest/ucd/" ++ file
     IO.println s!"Downloading UCD/{file}"
     let _ ← LogIO.captureLog <| download file url (dataDir/file)

It looks like download lost the first argument and it also looks like I no longer need to drop the log. But LogIO.captureLog seems to have disappeared. Maybe this is an old x with a new and improved y?

[François G. Dorais]

^^^ cc @Mac Malone

[Mac Malone]

@François G. Dorais You are correct that the first argument has been removed. I am not quite sure why you were dropping the log originally, so I am not sure exactly what you should do now. captureLog still exists. It is just not part of theLogIO namespace. The following should work:

let _ <- download url (dateDir/file) |>.captureLog

[François G. Dorais]

That was very quick! Your patch works fine. I found where captureLog went now. This is old code, I'm not sure why I was dropping the log. It's on my todo list to review that but now I can update my repo. Thanks Mac!

[François G. Dorais]

PS: I haven't done any serious testing, but it feels like solid performance improvements for lake too! Thanks Mac! I'm loving this update!

[François G. Dorais]

This is a strange one! Both of these alias declarations make lean crash:

import Std
alias foo := And.left
alias bar := And.right

So far, this seems to be localized to And.left and And.right. No issues with Or.left, Prod.fst, And.intro, nor anything else I tried.

[Christian Merten]

The new rfl tactic error message is great! It seems to override the default "no goals to be solved" message though:

example : 3 = 3 := by
  rfl
  rfl
  -- The rfl tactic failed. Possible reasons ...

[Yaël Dillies]

A few comments about the new build progress:

• I used to be able to see all build errors resurface during the linting step in mathlib CI. Now they are drowned in 4.5k lines of "Building ..." and all I get is a list of "Some build steps logged failures:" without actually telling me what the errors are, meaning that I can't start thinking about how to solve them while cache is downloading. Could the full errors resurface, rather than just their location?
• Building doesn't seem to stop once all files depending only on non-erroring files have been built, meaning that I have no clear indicator of eg how far in mathlib I have pushed a refactor. Could we recover the indicator of how many files were successfully built?

[Joachim Breitner]

Christian Merten said:

The new rfl tactic error message is great! It seems to override the default "no goals to be solved" message though:

example : 3 = 3 := by
  rfl
  rfl
  -- The rfl tactic failed. Possible reasons ...

Thanks for the feedback, glad you like it! Can you open an issue?

[Christian Merten]

Joachim Breitner said:

Can you open an issue?

lean4#4063

[François G. Dorais]

The alias command issue I mentioned above appears to be due to malformed constant info for And.left and And.right. I filed an issue: lean4#4064

[Kim Morrison]

Yaël Dillies said:

A few comments about the new build progress:

• I used to be able to see all build errors resurface during the linting step in mathlib CI. Now they are drowned in 4.5k lines of "Building ..." and all I get is a list of "Some build steps logged failures:" without actually telling me what the errors are, meaning that I can't start thinking about how to solve them while cache is downloading. Could the full errors resurface, rather than just their location?
• Building doesn't seem to stop once all files depending only on non-erroring files have been built, meaning that I have no clear indicator of eg how far in mathlib I have pushed a refactor. Could we recover the indicator of how many files were successfully built?

@Yaël Dillies, could you please open (separate) issues about these requests? In the first one, please explain carefully what you want in the first case without assuming that the current mathlib CI steps are known to all. :-)

[Eric Wieser]

Relating to mathlib CI, it seems that the problem matcher is no longer annotating the diff with build failures

[Eric Wieser]

I think this is probably because the messages are of the form error: ././././Mathlib/Algebra/MvPolynomial/Basic.lean:721:23-721:35, and nothing understands the - notation (VSCode also no longer lets you click the message to jump to the error)

[Kim Morrison]

Hmm, I've been successfully jumping to errors locally?

[Eric Wieser]

When I click on an error message, vscode gives me this behavior:

image.png

[Eric Wieser]

Removing the trailing -$line:$col fixes it

[Eric Wieser]

Maybe this is a gitpod quirk

[Kim Morrison]

Seem reasonable to open an issue for this one. Other tools are likely to get confused by the : in a way they wouldn't if it were just a space.

[Sebastian Ullrich]

I think support for the colon(s?) is pretty standard but the dash may not be

[Mario Carneiro]

I was discussing this with @Mac Malone . Apparently l:c-l.c works but it's a bit weird. Doing some quick comparative analysis, most other tools just show the initial l:c (including 4.7.0), which I think is fine since when you get there the line will be highlighted anyway

[Eric Wieser]

Yes, the problem is the dash not the colon

[Eric Wieser]

Though it looks like this can be fixed with extra configuration

[Eric Wieser]

Certainly problem-matchers support carrying this data, just not the parsers that vs code / our CI uses

[Somo S.]

tiny issue ..
image.png
Instead of being maked "latest", isn't an rc release supposed to be marked as "pre-release" like so
image.png
?

[Kim Morrison]

Fixed.

[Kim Morrison]

Re: lakefile.toml, I would like to see projects switch if possible / helpful! I'm hoping the toml file is useful, and that projects will try using it and come back with bug reports and feature requests. While we're unlikely to drop support for lakefile.lean anytime soon (perhaps ever), I hope that life is going to be simpler if most projects are using non-interpreted configuration files.

[Kim Morrison]

I've switched importGraph (see #12690 verifying that Mathlib is still happy). I think it should be no problem to switch std/batteries, but will wait to do so until after the rename.

[Kim Morrison]

We won't update Qq for now, as we prefer to leave that on the oldest compatible toolchain.

[Kim Morrison]

Similarly Cli? @Marc Huisinga?

[Kim Morrison]

proofwidgets has complicated requirements that can't be support from the toml yet.

[Kim Morrison]

I'll try aesop now, hopefully that is straightforward? (edit: https://github.com/leanprover-community/aesop/pull/131)

[Kim Morrison]

I'd be happy to hear reports of people making the migration in downstream projects, too!

[Kim Morrison]

It looks to me like meta if get_config? env = some "dev" then is the biggest blocker to moving more repositories to lakefile.toml.

@Mac Malone, do we have an issue about this?

[Mario Carneiro]

That's lake install I think: issue lean4#3423, PR lean4#3998

[Mario Carneiro]

I think it would be good to have an issue specifically for conditional dependencies in toml though, independently of lake install (which is poised to eliminate doc-gen from everyone's lakefiles)

[Yaël Dillies]

Kim Morrison said:

It looks to me like meta if get_config? env = some "dev" then is the biggest blocker to moving more repositories to lakefile.toml.

Sadly, all of LeanAPAP, LeanCamCombi, Con(NF), PFR use conditional dependencies to avoid everyone having to download doc-gen, so I can't actually switch to lakefile.toml in any of my projects

[Kim Morrison]

Mario's message immediately above is about avoiding the need to have a dependency at all (conditional or otherwise) on doc-gen once lake install lands.

[Marc Huisinga]

Kim Morrison said:

Similarly Cli? Marc Huisinga?

Sure.

[Jon Eugster]

This is is probably more a featrue request more than anything else. Most of my lakefiles currently have the following pattern in there:

import Lake
open Lake DSL

def leanVersion : String := s!"v{Lean.versionString}"

[...]

require std from git "https://github.com/leanprover/std4.git" @ leanVersion
require i18n from git "https://github.com/hhu-adam/lean-i18n.git" @ leanVersion

[...]

This is mainly to ensure that packages that do not import mathlib are still compatible with the stable releases. So far that's been the most ideomatic way I know of: You update leantoolchain to the version you want, call lake update and you're good. I think it would be nice if the .toml files also supported an easy way to follow stable releases without editing the version once per dependency. My reasons are mainly:

• non-mathlib/batteries projects should probably be encouraged to follow the stable releases. After all that's why there are releases, right?
• lake update is a bit of a false friend for beginners/intermediates as it might mess up your project. Therefore, I like to set up my config in a way that rm -rf ./lake lake-manifest.json && lake update is a 100% reliable way to recover if things went wrong.

[David Renshaw]

Updated tryAtEachStep.
After lake translate-config toml, I needed to manually move the defaultTargets line up that that it did not fall under [leanOptions].

[Siddhartha Gadgil]

I seem to have trouble upgrading when meta-programming from a Lean script. Concretely, lines of the following form worked fine in earlier versions (after running initSearchPath):

let env' ← importModules #[{module := `LeanAide}] {}

But now I get the error uncaught exception: unknown package 'ImportGraph'.

This does not seem to depend on what the array of modules being imported is so long as it is non-empty. I get the same error with

let env' ← importModules #[{module := `Mathlib}] {}

[Kim Morrison]

@Siddhartha Gadgil, you might have to give us more context to be able to help you.

[Eric Wieser]

Does running lake build help?

[Mac Malone]

David Renshaw said:

Updated tryAtEachStep.
After lake translate-config toml, I needed to manually move the defaultTargets line up that that it did not fall under [leanOptions].

Could you elaborate on this and/or create an issue with a failing #mwe?

[Siddhartha Gadgil]

I am trying.

[Jon Eugster]

@Siddhartha Gadgil this does sound like it would help to check if importGraph is in your lake-manifest.json and also in .lake/packages/importGraph. That might give a hint whether your dependencies are imported correctly, it sounds a bit as if mathlib itself wouldnt properly work in your project, but that's a very far speculation.

[Siddhartha Gadgil]

Thanks @Jon Eugster

It was the case that this was missing from my initSearchPath. Adding this fixed the error @Kim Morrison @Mac Malone thanks.

Unfortunately there is another error. I will try to minimize and then report.
I was doing things in a needlessly complicated way. Cleaning my code (and the initSearchPath correction) fixes all issues.

[Siddhartha Gadgil]

@Mac Malone The root cause of the error was my manually including all the places where lake places oleans in my initSearchPath. For example:

def initFiles : List System.FilePath := [".lake/build/lib", ".lake/packages/mathlib/.lake/build/lib",  ".lake/packages/std/.lake/build/lib", ".lake/packages/Qq/.lake/build/lib", ".lake/packages/aesop/.lake/build/lib", ".lake/packages/proofwidgets/.lake/build/lib", ".lake/packages/importGraph/.lake/build/lib" ]

Is there a function in the Lake API I can use instead?

[Kim Morrison]

Maybe it is helpful to #xy here, and explain why you need those locations?

[Siddhartha Gadgil]

I need them because I write files in my main library that run to core, and then run in lean_exe targets by building and passing an environment. The relevant lines in my code are (within IO):

initSearchPath (← Lean.findSysroot) initFiles
let env ←
    importModules #[{module := `Mathlib},
    {module:= `LeanAide.TheoremElab},
    {module:= `LeanCodePrompts.Translate}] {}

[Siddhartha Gadgil]

By "run" above I meant use Core.run to get an EIO before passing to IO etc.

[Siddhartha Gadgil]

Just read what #xy means and my actual goal is to pass an environment to run CoreM stuff in compiled Lean code.

[Kim Morrison]

What about searchPathRef.set compile_time_search_path%?

[Siddhartha Gadgil]

Thanks @Kim Morrison
Indeed this worked fine as a replacement to my hacky initSearchpath

[Peiran Wu]

Mac Malone said:

David Renshaw said:

Updated tryAtEachStep.
After lake translate-config toml, I needed to manually move the defaultTargets line up that that it did not fall under [leanOptions].

Could you elaborate on this and/or create an issue with a failing #mwe?

I've encountered the same problem as David Renshaw has. I have filed an issue: https://github.com/leanprover/lean4/issues/4099

[Kim Morrison]

Thanks for the report. Hopefully we'll be able to include a fix for this in v4.8.0-rc2 (perhaps next week?)

[Michael Rothgang]

At yesterday's Lean workshop in Berlin, some participants had trouble installing Lean. I was particularly puzzled by one error message: typing lake exe cache get in the project's root directory resulted in the error could not find file ./lakefile.lean.

This was puzzling since the user was in the root directory --- but the repository we were using had a lakefile.toml and not lakefile.lean. (This error didn't occur for all users, just some.) Is this

• just a bug in the error message (i.e., cache also checks for a lakefile.toml, but the error doesn't mention it)?
• a bug in cache (not checking for lakefile.toml)
• something else (mumble mumble paths) --- which belongs into a different thread?

[Michael Rothgang]

Alternatively, a pointer to cache's source code so I can check myself is also welcome.

[Mario Carneiro]

is there a find in there, or did it really say could not file?

[Mario Carneiro]

this is a lake error message, most likely caused by using a lake version that doesn't know about toml

[Michael Rothgang]

Mario Carneiro said:

is there a find in there, or did it really say could not file?

I don't remember precisely, but am pretty sure I just omitted the find now - fixed, thanks!

[Kim Morrison]

i.e. you need to make sure the lean-toolchain says v4.8.0-rc1

[Michael Rothgang]

Mario Carneiro said:

this is a lake error message, most likely caused by using a lake version that doesn't know about toml

So the fix would be to ensure participants have the right version of lake... I see!
(The lean-toolchain does say v4.8.0-rc1.)

[Kim Morrison]

Hmm -- as soon as the lean-toolchain is right, you should have the right version of lake.

[Kim Morrison]

That is determined by the lean-toolchain.