leanprover-community/mathlib-tools#95

Stream: PR reviews

[Eric Wieser]

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

• https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/leanproject.20and.20python.203.2E9.2E1/near/227411279
• https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/leanproject/near/221511733

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

[Patrick Massot]

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]

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

[Eric Wieser]

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

[Eric Wieser]

But thanks for taking a look!

[Sebastien Gouezel]

> Measure-Command { leanproject -h }

Seconds           : 0
Milliseconds      : 641

[Eric Wieser]

Any chance you could time the branch too?

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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]

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

[Eric Wieser]

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

[Eric Wieser]

Thanks for testing though

[Patrick Massot]

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.