MacOS brew update of Python breaks leanproject

[arademaker]

Whenever I update the Python with Homebrew, leanproject breaks

zsh: /Users/ar/.local/bin/leanproject: bad interpreter: /Users/ar/.local/pipx/venvs/mathlibtools/bin/python: no such file or directory

Any idea? So far, I am removing the pipx and reinstalling mathlibtools!

[arademaker]

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/python@3.9/3.9.1_7/bin/python3.9

I made it

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

[Julian]

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...

[Julian]

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.

[Julian]

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)

[arademaker]

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

[Julian]

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.

[bryangingechen]

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