MacOS brew update of Python breaks leanproject about mathlib-tools HOT 7 CLOSED

This is somewhat "known" bad behavior on Homebrew's part unfortunately. It's why some people in the Python community recommend against using Homebrew's Python. I'm not typically one of them, I use Homebrew's Python myself, but I'm more tempted to agree if you're not doing Python development full time...

from mathlib-tools.

The install_macos.sh script will now do so automatically -- but docs for migrating from the old setup probably is a good idea -- it's essentially going to be pipx uninstall mathlibtools && brew install mathlibtools to move over I believe. If you try that out when you get a minute perhaps and let me know if that works I'm happy to put that command somewhere in the install info if that's helpful.

from mathlib-tools.

Another solution I found recently was to manually fix the link created in

/Users/ar/.local/pipx/venvs/mathlibtools/bin

instead of

python3.9 -> /usr/local/Cellar/[email protected]/3.9.1_7/bin/python3.9

I made it

python3.9 -> /usr/local/bin/python3.9

from mathlib-tools.

FWIW I think a better solution for leanproject will be shipping it as a shiv or zipapp for most users (in which case there's nothing to do, you just download the shiv)... which I meant to POC for y'all at some point but still haven't managed to find some spare time.

from mathlib-tools.

We likely should close this now I think -- despite the above, if you install leanproject via brew install mathlibtools rather than directly via pipx (as `install_macos.sh now does), this issue should no longer exist.

(CC @PatrickMassot)

from mathlib-tools.

Do we have a documentation about this alternative way to install the tools?

from mathlib-tools.

The updated docs are now here. Please post on Zulip or create an issue at our website repo if something is still unclear.

from mathlib-tools.