leanproject/python problem

Stream: new members

[Heather Macbeth]

Alex Kontorovich said:

When I try from terminal to do: leanproject get -b mathlib:exp_facts
I get this error: zsh: /usr/local/bin/leanproject: bad interpreter: /usr/local/opt/python/bin/python3.7: no such file or directory
Any idea for how to fix it?... Thanks!

Aargh! I just hit the same problem, but fortunately I have a data point about where it came from.

[Heather Macbeth]

I ran the same leanproject command about 10 minutes apart, no problems the first time, the above problem the second time. And I only ran one significant command in between ...

[Heather Macbeth]

MAC-M5TBLVDC:mathlib_map-inversion-smooth heathermacbeth$ leanproject import-graph --from analysis.normed_space.basic ../output.graphml
MAC-M5TBLVDC:lean heathermacbeth$ brew install graphviz

[.... I deleted a long output here ....]

Error: Could not remove python keg! Do so manually:
  sudo rm -rf /usr/local/Cellar/python/3.7.7
MAC-M5TBLVDC:mathlib_map-inversion-smooth heathermacbeth$ leanproject import-graph --from analysis.normed_space.basic ../output.pdf
-bash: /usr/local/bin/leanproject: /usr/local/opt/python/bin/python3.7: bad interpreter: No such file or directory

[Heather Macbeth]

Something must have changed about my python when I ran the brew install graphviz? (I had just seen
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/leanproject.20import-graph
and decided to experiment with graphviz.)

[Yury G. Kudryashov]

So, brew install graphviz removed /usr/local/opt/python/bin/python3.7?

[Heather Macbeth]

Seems so. How can I get it back?

[Yury G. Kudryashov]

I'm not a Mac user.

[Yury G. Kudryashov]

Could you please pastebin the long output?

[Heather Macbeth]

https://pastebin.com/fNq6zj7z

[Yury G. Kudryashov]

It says

==> Deleted Formulae
python ✔                 elasticsearch@2.4        i386-elf-grub            sflowtool                wpscan
cryptopp                 elasticsearch@5.6        kibana@5.6               tomee-jax-rs

[Yury G. Kudryashov]

I've no idea why graphviz conflicts with python in brew

[Yury G. Kudryashov]

It seems that it installed new python@3.7 and python@3.8

[Yury G. Kudryashov]

Probably at new locations

[Heather Macbeth]

Would it be safe to re-run the python part listed at
https://leanprover-community.github.io/install/macos_details.html
?

brew install python3 pipx
pipx ensurepath
pipx install mathlibtools

[Yury G. Kudryashov]

Try reinstalling mathlibtools

[Yury G. Kudryashov]

try the last two commands

[Heather Macbeth]

-bash: pipx: command not found

[Yury G. Kudryashov]

What about pip install mathlibtools or pip3 install mathlibtools?

[Heather Macbeth]

running brew install pipx now.

[Yury G. Kudryashov]

Will it uninstall graphviz?

[Heather Macbeth]

Family calling for dinner, thank you for your help! Will try more later.

[Heather Macbeth]

I seem to have fixed it with

pipx install --force mathlibtools
pipx ensurepath

(it didn't work without the --force). It still complains every time I use leanproject:

zsh: /usr/local/bin/leanproject: bad interpreter: /usr/local/opt/python/bin/python3.7: no such file or directory

but works nonetheless.

[Heather Macbeth]

Would be interested to hear any ideas for getting rid of the complaint.

[Heather Macbeth]

And tagging @Alex Kontorovich -- I was lucky ( :wink: ) enough to hit the same error as you, right after you did!

[Alex Kontorovich]

Great! Now the previous line you told me (leanproject get -b mathlib:exp_facts) worked. ... now what? :)

[Heather Macbeth]

You should have a new copy of mathlib called mathlib_exp_facts? Go into it and make your edits.

[Julian Berman]

Heather Macbeth said:

Would be interested to hear any ideas for getting rid of the complaint.

What is head -n1 /usr/local/bin/leanproject and type -a python3 and type -a python3.7 and brew list | grep python and echo $PATH