Zulip Chat Archive

Stream: PR reviews

Topic: leanprover-community/mathlib-tools#95


Eric Wieser (Mar 03 2021 at 11:42):

This one's been there for a while now. It's motivated in part by these threads from people with broken python setups:

And partly by things being slow for me on windows. @Patrick Massot, mind taking a look?

Patrick Massot (Mar 03 2021 at 20:44):

I am really reluctant to uglify the code in order to allow broken python setup. I'd be ok if this affect all Windows users. Can other Windows user tell us how much time it takes to run leanproject -h?

Eric Wieser (Mar 03 2021 at 20:47):

I'd expect the ~40% speed improvement to apply on all platforms

Eric Wieser (Mar 03 2021 at 20:48):

And I'd argue this is only really two lines of uglification

Eric Wieser (Mar 03 2021 at 20:48):

But thanks for taking a look!

Sebastien Gouezel (Mar 03 2021 at 21:17):

> Measure-Command { leanproject -h }

Seconds           : 0
Milliseconds      : 641

Eric Wieser (Mar 03 2021 at 21:46):

Any chance you could time the branch too?

Sebastien Gouezel (Mar 03 2021 at 21:51):

If you can give me detailed instructions on how to do this without breaking my setup, yes, sure.

Sebastien Gouezel (Mar 03 2021 at 21:57):

I found a way to do it. Time goes down to 467 Milliseconds. In practice, both are essentially instant. On a laptop which is not blazingly fast.

Sebastien Gouezel (Mar 03 2021 at 21:59):

This was from a powershell console, but from a git bash the figures are essentially the same (0.671s vs 0.456s)

Eric Wieser (Mar 03 2021 at 22:04):

Half a second is a long way from instant for doing nothing at all

Eric Wieser (Mar 03 2021 at 22:04):

Thanks for testing though

Patrick Massot (Mar 04 2021 at 07:57):

Thinking again about this before sleeping yesterday, I thought I've been too strict here. I really don't like importing a module in the middle of a file, but I think your mathlib PR reviewing work deserves some effort on the tooling side. I still recommend you try to understand why your python is so slow, but I'll merge this anyway.


Last updated: Dec 20 2023 at 11:08 UTC