new versions coming out too fast?

Stream: new members

[Sayantan Majumdar]

Are the new versions in leanprover-community coming out too fast? 3.6 seems too slow takes forever to do anything!

[Mario Carneiro]

fast in what sense? your two sentences are talking about different things

[Sayantan Majumdar]

it seems every month there is a new version of lean

[Sayantan Majumdar]

the latest i think is 3.6 is very slow

[Mario Carneiro]

again, what do those two things have to do with one another?

[Andrew Ashworth]

If you have a concrete example of something that was a certain speed in in Lean 3.5 that is slow in 3.6, that would be valuable to know about

[Sayantan Majumdar]

there is no time to check if the recently released version is working properly!

[Mario Carneiro]

yes, the timetable for releases has shrunk (this is a low bar considering it was effectively abandoned for 2 years)

[Mario Carneiro]

as for potential performance regressions, we need numbers

[Mario Carneiro]

lean has some performance issues but I'm not aware of any specific places where it's gotten worse

[Andrew Ashworth]

You always have the option to not upgrade Lean? It's only necessary if you want to maintain compatibility with mathlib development.

[Andrew Ashworth]

Maybe I'm in the minority here on the chat but I still have a set environment with a specific mathlib commit that I build with lean --make, I still use leanpkg and I've never learned how to use all leanproject or elan

[Sayantan Majumdar]

I thought people checked the performance numbers before releasing

[Andrew Ashworth]

and it works fine for me on windows...

[Sayantan Majumdar]

i was doing the same

[Mario Carneiro]

you still haven't given any examples

[Mario Carneiro]

there are a ton of ways to use lean, performance depends on what you are doing

[Sayantan Majumdar]

i typed import data.real.basic and it took a min to load

[Andrew Ashworth]

Did you build mathlib?

[Mario Carneiro]

that's because you didn't compile mathlib

[Sayantan Majumdar]

what kind of performance is being checked before releases

[Mario Carneiro]

lean 3.4.2 had the same behavior

[Mario Carneiro]

you forgot an important step, this isn't lean's fault

[Sayantan Majumdar]

I compiled everything first then opened the first_proofs.lean worked after 15 mins

[Andrew Ashworth]

nobody is checking performance regressions in the detail that you want

[Andrew Ashworth]

contributions welcome :)

[Andrew Ashworth]

there are no lean developers, just people volunteering

[Sayantan Majumdar]

before anyone is done with the performance check a new major version will be out

[Mario Carneiro]

15 mins is definitely an indication that something is being built on load

[Sayantan Majumdar]

it was built before i opened the files

[Mario Carneiro]

for some reason that isn't the case

[Mario Carneiro]

the question is what happened to cause that

[Sayantan Majumdar]

how do you know?

[Andrew Ashworth]

it doesn't take 15 minutes for anybody else

[Mario Carneiro]

because this has happened many many times in other discussions

[Sayantan Majumdar]

anybody using windows?

[Mario Carneiro]

I actually think it is a minor bug that lean even lets you use the file when it's not compiled like this

[Mario Carneiro]

it is just super slow and people get the wrong impression

[Sayantan Majumdar]

i compiled it using leanpkg test before opening my editor

[Mario Carneiro]

leanproject check will try to diagnose this problem

[Mario Carneiro]

if you have a later version of mathlib, leanpkg doesn't work anymore

[Mario Carneiro]

leanproject is the new version

[Mario Carneiro]

IIRC leanpkg uses an old version of lean to build and so the new version will see that the oleans are out of date and recompile them

[Sayantan Majumdar]

hmmm, will check that

[Sayantan Majumdar]

noi use leanpkg toolbox install first

[Sayantan Majumdar]

then it can build with the latest version

[Sayantan Majumdar]

will try leanproject though

[Mario Carneiro]

I'm not an expert on leanpkg but I think it is not supported anymore

[Sayantan Majumdar]

hopefully, no new versions come out before it finishes compiling

[Mario Carneiro]

the latest version is 3.7.2 btw

[Scott Morrison]

3.8 as of last night :-)

[Sayantan Majumdar]

check again,

[Mario Carneiro]

lol

[Sayantan Majumdar]

lol

[Mario Carneiro]

is mathlib on 3.8 yet?

[Mario Carneiro]

when you have elan, this doesn't really matter

[Mario Carneiro]

it just uses the right version of lean as requested in the toml file, so when mathlib upgrades it happens automatically

[Mario Carneiro]

even if a new version comes out it won't invalidate your compile

[Mario Carneiro]

unless you choose to upgrade mathlib and lean along with it

[Sayantan Majumdar]

everyone knows that

[Mario Carneiro]

then what's the problem?

[Sayantan Majumdar]

the new versions are too slow!

[Mario Carneiro]

lean can update every day and it shouldn't cause you any trouble

[Mario Carneiro]

It's very confusing talking about these two completely unrelated topics at once

[Sayantan Majumdar]

not confusing to me

[Sayantan Majumdar]

good night

[Mario Carneiro]

Nothing has been done regarding the loading process in the last few versions

[Mario Carneiro]

I encourage you to make sure your olean files are up to date, and come back with an independently verifiable test case if it keeps being slow

[Bryan Gin-ge Chen]

There was a bug with 3.7.0 and 3.7.1 which caused oleans not to be loaded properly on Windows. As far as I know those issues are fixed now though (?).

[Kevin Buzzard]

@Sayantan Majumdar if data.real.basic takes more than a few seconds to import then your setup is bad. You need to use leanproject if you've moved from 3.4.2

[Patrick Stevens]

Sayantan Majumdar said:

everyone knows that

As a meta-point, asserting "everyone knows <something>" is quite bold (especially in the "new users" stream where we can expect to find a very wide range of experience starting at "literally just started learning maths and programming"); declaring in this way that you don't need the help of the people who are trying to help is not likely to get you the help you need.

Please note also that your default position when the major figures in Lean say "performance has not got substantially worse, and moreover nobody else thinks it has" should probably not be "Lean has got really slow for everyone" but "something is wrong for me locally", especially since you already knew that people check the performance numbers before releasing; extraordinary claims require extraordinary evidence. It is possible that performance has got substantially worse in a way that uniquely affects you, but you shouldn't simply assert that it has and then, when asked for evidence, just assert it again.

[Kevin Buzzard]

Their problem is probably that they're using old tooling which doesn't play well with versions of lean after 3.4