Zulip Chat Archive

Stream: new members

Topic: leanproject/python problem


Heather Macbeth (Sep 24 2020 at 23:39):

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 (Sep 24 2020 at 23:41):

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 (Sep 24 2020 at 23:42):

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 (Sep 24 2020 at 23:43):

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 (Sep 24 2020 at 23:43):

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

Heather Macbeth (Sep 24 2020 at 23:44):

Seems so. How can I get it back?

Yury G. Kudryashov (Sep 24 2020 at 23:44):

I'm not a Mac user.

Yury G. Kudryashov (Sep 24 2020 at 23:45):

Could you please pastebin the long output?

Heather Macbeth (Sep 24 2020 at 23:47):

https://pastebin.com/fNq6zj7z

Yury G. Kudryashov (Sep 25 2020 at 00:01):

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 (Sep 25 2020 at 00:01):

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

Yury G. Kudryashov (Sep 25 2020 at 00:04):

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

Yury G. Kudryashov (Sep 25 2020 at 00:04):

Probably at new locations

Heather Macbeth (Sep 25 2020 at 00:04):

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 (Sep 25 2020 at 00:04):

Try reinstalling mathlibtools

Yury G. Kudryashov (Sep 25 2020 at 00:04):

try the last two commands

Heather Macbeth (Sep 25 2020 at 00:05):

-bash: pipx: command not found

Yury G. Kudryashov (Sep 25 2020 at 00:06):

What about pip install mathlibtools or pip3 install mathlibtools?

Heather Macbeth (Sep 25 2020 at 00:06):

running brew install pipx now.

Yury G. Kudryashov (Sep 25 2020 at 00:06):

Will it uninstall graphviz?

Heather Macbeth (Sep 25 2020 at 00:06):

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

Heather Macbeth (Sep 25 2020 at 01:58):

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 (Sep 25 2020 at 01:58):

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

Heather Macbeth (Sep 25 2020 at 01:59):

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

Alex Kontorovich (Sep 25 2020 at 02:18):

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

Heather Macbeth (Sep 25 2020 at 02:19):

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

Julian Berman (Sep 25 2020 at 02:50):

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


Last updated: Dec 20 2023 at 11:08 UTC