Zulip Chat Archive

Stream: PR reviews

Topic: leanprover-community/mathlib-tools#95


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Mar 03 2021 at 20:47):

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

view this post on Zulip Eric Wieser (Mar 03 2021 at 20:48):

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

view this post on Zulip Eric Wieser (Mar 03 2021 at 20:48):

But thanks for taking a look!

view this post on Zulip Sebastien Gouezel (Mar 03 2021 at 21:17):

> Measure-Command { leanproject -h }

Seconds           : 0
Milliseconds      : 641

view this post on Zulip Eric Wieser (Mar 03 2021 at 21:46):

Any chance you could time the branch too?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Eric Wieser (Mar 03 2021 at 22:04):

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

view this post on Zulip Eric Wieser (Mar 03 2021 at 22:04):

Thanks for testing though

view this post on Zulip 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: May 06 2021 at 12:15 UTC