mathlib-tools#126

Stream: PR reviews

[Scott Morrison]

My PR to the mathlib-tools repository mathlib-tools#126 is failing in CI, because CI can't install PyInstaller.

I know leanproject is eventually going to be abandoned / replaced, so I guess it's okay if we say it's at end-of-life.

On the other hand, I'm still using it to help understand porting requirements to mathlib4.

Is there anyone with PyInstaller expertise who could take a look?

[Kevin Buzzard]

There's plenty of new people at Imperial using leanproject (I installed it myself on a machine today) and come January assuming the port hasn't happened there will be plenty more

[Scott Morrison]

leanproject will continue working, the question is whether we have bandwidth to update it and make changes.

[Mario Carneiro]

Yeah, I don't think leanproject is EOL yet. Hopefully someone else has more time to spend on it though

[Eric Wieser]

If we're really stumped here we could likely remove pyinstaller support entirely; I don't think we ever recommended it as an install method, it was just there for users who wanted it

[Patrick Massot]

I was weak the day I accepted a PR adding this pysintaller thing while I didn't know anything about it. Now it blocks all development of leanproject so any PR removing the pyinstaller thing will be merged right away.

[Eric Wieser]

https://github.com/leanprover-community/mathlib-tools/pull/127 unblocks things, thanks @Scott Morrison!