Zulip Chat Archive

Stream: new members

Topic: new versions coming out too fast?


view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:29):

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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:30):

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

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:30):

it seems every month there is a new version of lean

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:30):

the latest i think is 3.6 is very slow

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:31):

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

view this post on Zulip Andrew Ashworth (Apr 11 2020 at 23:32):

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

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:32):

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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:32):

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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:32):

as for potential performance regressions, we need numbers

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:33):

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

view this post on Zulip Andrew Ashworth (Apr 11 2020 at 23:33):

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

view this post on Zulip Andrew Ashworth (Apr 11 2020 at 23:34):

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

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:34):

I thought people checked the performance numbers before releasing

view this post on Zulip Andrew Ashworth (Apr 11 2020 at 23:34):

and it works fine for me on windows...

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:35):

i was doing the same

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:35):

you still haven't given any examples

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:35):

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

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:35):

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

view this post on Zulip Andrew Ashworth (Apr 11 2020 at 23:36):

Did you build mathlib?

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:36):

that's because you didn't compile mathlib

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:36):

what kind of performance is being checked before releases

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:36):

lean 3.4.2 had the same behavior

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:36):

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

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:37):

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

view this post on Zulip Andrew Ashworth (Apr 11 2020 at 23:37):

nobody is checking performance regressions in the detail that you want

view this post on Zulip Andrew Ashworth (Apr 11 2020 at 23:37):

contributions welcome :)

view this post on Zulip Andrew Ashworth (Apr 11 2020 at 23:37):

there are no lean developers, just people volunteering

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:38):

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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:38):

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

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:38):

it was built before i opened the files

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:38):

for some reason that isn't the case

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:38):

the question is what happened to cause that

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:38):

how do you know?

view this post on Zulip Andrew Ashworth (Apr 11 2020 at 23:39):

it doesn't take 15 minutes for anybody else

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:39):

because this has happened many many times in other discussions

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:39):

anybody using windows?

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:40):

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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:40):

it is just super slow and people get the wrong impression

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:40):

i compiled it using leanpkg test before opening my editor

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:40):

leanproject check will try to diagnose this problem

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:41):

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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:41):

leanproject is the new version

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:42):

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

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:42):

hmmm, will check that

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:42):

noi use leanpkg toolbox install first

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:42):

then it can build with the latest version

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:43):

will try leanproject though

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:43):

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

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:43):

hopefully, no new versions come out before it finishes compiling

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:44):

the latest version is 3.7.2 btw

view this post on Zulip Scott Morrison (Apr 11 2020 at 23:44):

3.8 as of last night :-)

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:44):

check again,

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:44):

lol

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:44):

lol

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:45):

is mathlib on 3.8 yet?

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:46):

when you have elan, this doesn't really matter

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:46):

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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:47):

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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:47):

unless you choose to upgrade mathlib and lean along with it

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:48):

everyone knows that

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:48):

then what's the problem?

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:48):

the new versions are too slow!

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:48):

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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:49):

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

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:51):

not confusing to me

view this post on Zulip Sayantan Majumdar (Apr 11 2020 at 23:51):

good night

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:51):

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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:52):

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

view this post on Zulip Bryan Gin-ge Chen (Apr 12 2020 at 01:10):

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 (?).

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 06:22):

@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

view this post on Zulip Patrick Stevens (Apr 12 2020 at 06:59):

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.

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:08):

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


Last updated: May 12 2021 at 04:19 UTC