Creating Lean project

Stream: new members

[Saroj N]

I havent been able to create a lean project. When I type "leanproject new my_project" on command prompt, it says "zsh: /Users/saroj/.local/bin/leanproject: bad interpreter: /Users/saroj/.local/pipx/venvs/mathlibtools/bin/python: no such file or directory". Can anyone help?

[Adam Topaz]

Is looks like you installed mathlibtools in a python venv, and the environment hasn't been activated

[Adam Topaz]

In any case, this looks like a path issue

[Adam Topaz]

Can you recall how you installed mathlibtools?

[Saroj N]

I followed the detailed instructions from lean prover community website

[Saroj N]

i followed the detailed instructions on lean prover community

[Kevin Buzzard]

What operating system are you using? Did you use the same terminal to create the lean project as you did when installing? Did you try rebooting? On unix I'd suggest source ~/.profile.

[Julian Berman]

That looks unlikely to be a venv created manually

[Julian Berman]

And should work even without being activated

[Julian Berman]

It seems more likely that that interpreter just actually doesn't exist

[Julian Berman]

What is ls /Users/saroj/.local/pipx/venvs/mathlibtools/bin?

[Julian Berman]

If it comes back not existing, probably rerun pipx install mathlibtools

[Hanting Zhang]

I'm getting this same error now: /Users/jdzhang/.local/bin/leanproject: /Users/jdzhang/.local/pipx/venvs/mathlibtools/bin/python: bad interpreter: No such file or directory

My path looks like this if it matters:

/Library/Frameworks/Python.framework/Versions/3.9/bin:/Users/jdzhang/.elan/bin:/Users/jdzhang/.elan/bin:/usr/local/opt/python/libexec/bin:/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin:/Library/TeX/texbin:/Users/jdzhang/.local/bin:/Library/Frameworks/Python.framework/Versions/3.8/bin:/Users/jdzhang/Library/Python/3.9/bin

Any experts know what's going on? Thanks in advance

[Huỳnh Trần Khanh]

Are you a mathematician, a programmer, or both? If you are a programmer, you can use Docker and install code-server and Lean in a container. That's what I do, well I use LXC, but anyway the point is to use a separate container to avoid software conflicts.

[Huỳnh Trần Khanh]

OK so I guess you are a mathematician and you don't know what Docker is. Are you using an M1 Mac or an Intel Mac?

[Huỳnh Trần Khanh]

In my experience, these kinds of errors are extremely hard to diagnose over chat. It seems that you are also in the Xena Project Discord server, you might want to stream your screen and ask for help there.

[Huỳnh Trần Khanh]

You know, computer programs tend to interact with each other in pretty weird ways. I have several tricks to avoid accumulating "entropy" and I'd be really glad to help you in the voice chat!

[Julian Berman]

@Hanting Zhang that error means the Python installation that pipx used broke basically

[Julian Berman]

You're on macOS I see though -- mathlibtools is now in homebrew

[Julian Berman]

So the easiest thing to do is likely now to run brew install mathlibtools and to discard (or uninstall) your existing installation (probably with pipx uninstall mathlibtools)

[Hanting Zhang]

I'm definitely not a programmer -- what does "mathlibtools is now in homebrew" mean?

[Julian Berman]

Sorry, I was slow typing -- ^^ let me know if that makes sense

[Hanting Zhang]

Ok, let me try that

[Julian Berman]

(Headed out for a bit but hopefully that gets you started, if not will be back later if need be)

[Hanting Zhang]

==> Installing mathlibtools dependency: six
==> Pouring six--1.16.0_1.catalina.bottle.tar.gz
Error: The `brew link` step did not complete successfully
The formula built, but is not symlinked into /usr/local
Could not symlink lib/python3.7/site-packages/six.py
Target /usr/local/lib/python3.7/site-packages/six.py
already exists. You may want to remove it:
  rm '/usr/local/lib/python3.7/site-packages/six.py'

To force the link and overwrite all conflicting files:
  brew link --overwrite six

To list all files that would be deleted:
  brew link --overwrite --dry-run six

Possible conflicting files are:

/usr/local/lib/python3.7/site-packages/six.py
/usr/local/lib/python3.9/site-packages/six.py

[Hanting Zhang]

Should I brew link --overwrite six here?

[Hanting Zhang]

Wait nevermind, leanproject works now!

[Hanting Zhang]

Thank you so much @Julian Berman! :octopus:

[Hanting Zhang]

Nevermind I spoke too soon.

Traceback (most recent call last):
  File "/usr/local/Cellar/mathlibtools/1.0.0/libexec/lib/python3.9/site-packages/git/__init__.py", line 87, in <module>
    refresh()
  File "/usr/local/Cellar/mathlibtools/1.0.0/libexec/lib/python3.9/site-packages/git/__init__.py", line 76, in refresh
    if not Git.refresh(path=path):
  File "/usr/local/Cellar/mathlibtools/1.0.0/libexec/lib/python3.9/site-packages/git/cmd.py", line 309, in refresh
    raise ImportError(err)
ImportError: Bad git executable.
The git executable must be specified in one of the following ways:
    - be included in your $PATH
    - be set via $GIT_PYTHON_GIT_EXECUTABLE
    - explicitly set via git.refresh()

All git commands will error until this is rectified.

This initial warning can be silenced or aggravated in the future by setting the
$GIT_PYTHON_REFRESH environment variable. Use one of the following values:
    - quiet|q|silence|s|none|n|0: for no warning or exception
    - warn|w|warning|1: for a printed warning
    - error|e|raise|r|2: for a raised exception

Example:
    export GIT_PYTHON_REFRESH=quiet


The above exception was the direct cause of the following exception:

Traceback (most recent call last):
  File "/usr/local/bin/leanproject", line 33, in <module>
    sys.exit(load_entry_point('mathlibtools==1.0.0', 'console_scripts', 'leanproject')())
  File "/usr/local/bin/leanproject", line 25, in importlib_load_entry_point
    return next(matches).load()
  File "/usr/local/Cellar/python@3.9/3.9.5/Frameworks/Python.framework/Versions/3.9/lib/python3.9/importlib/metadata.py", line 77, in load
    module = import_module(match.group('module'))
  File "/usr/local/Cellar/python@3.9/3.9.5/Frameworks/Python.framework/Versions/3.9/lib/python3.9/importlib/__init__.py", line 127, in import_module
    return _bootstrap._gcd_import(name[level:], package, level)
  File "<frozen importlib._bootstrap>", line 1030, in _gcd_import
  File "<frozen importlib._bootstrap>", line 1007, in _find_and_load
  File "<frozen importlib._bootstrap>", line 986, in _find_and_load_unlocked
  File "<frozen importlib._bootstrap>", line 680, in _load_unlocked
  File "<frozen importlib._bootstrap_external>", line 855, in exec_module
  File "<frozen importlib._bootstrap>", line 228, in _call_with_frames_removed
  File "/usr/local/Cellar/mathlibtools/1.0.0/libexec/lib/python3.9/site-packages/mathlibtools/leanproject.py", line 7, in <module>
    from git.exc import GitCommandError # type: ignore
  File "/usr/local/Cellar/mathlibtools/1.0.0/libexec/lib/python3.9/site-packages/git/__init__.py", line 89, in <module>
    raise ImportError('Failed to initialize: {0}'.format(exc)) from exc
ImportError: Failed to initialize: Bad git executable.
The git executable must be specified in one of the following ways:
    - be included in your $PATH
    - be set via $GIT_PYTHON_GIT_EXECUTABLE
    - explicitly set via git.refresh()

All git commands will error until this is rectified.

This initial warning can be silenced or aggravated in the future by setting the
$GIT_PYTHON_REFRESH environment variable. Use one of the following values:
    - quiet|q|silence|s|none|n|0: for no warning or exception
    - warn|w|warning|1: for a printed warning
    - error|e|raise|r|2: for a raised exception

Example:
    export GIT_PYTHON_REFRESH=quiet

Jiandongs-MacBook-Pro:mathlib jdzhang$ leanproject check
Traceback (most recent call last):
  File "/usr/local/Cellar/mathlibtools/1.0.0/libexec/lib/python3.9/site-packages/git/__init__.py", line 87, in <module>
    refresh()
  File "/usr/local/Cellar/mathlibtools/1.0.0/libexec/lib/python3.9/site-packages/git/__init__.py", line 76, in refresh
    if not Git.refresh(path=path):
  File "/usr/local/Cellar/mathlibtools/1.0.0/libexec/lib/python3.9/site-packages/git/cmd.py", line 246, in refresh
    cls().version()
  File "/usr/local/Cellar/mathlibtools/1.0.0/libexec/lib/python3.9/site-packages/git/cmd.py", line 588, in <lambda>
    return lambda *args, **kwargs: self._call_process(name, *args, **kwargs)
  File "/usr/local/Cellar/mathlibtools/1.0.0/libexec/lib/python3.9/site-packages/git/cmd.py", line 1134, in _call_process
    return self.execute(call, **exec_kwargs)
  File "/usr/local/Cellar/mathlibtools/1.0.0/libexec/lib/python3.9/site-packages/git/cmd.py", line 785, in execute
    cwd = self._working_dir or os.getcwd()
FileNotFoundError: [Errno 2] No such file or directory

The above exception was the direct cause of the following exception:

Traceback (most recent call last):
  File "/usr/local/bin/leanproject", line 33, in <module>
    sys.exit(load_entry_point('mathlibtools==1.0.0', 'console_scripts', 'leanproject')())
  File "/usr/local/bin/leanproject", line 25, in importlib_load_entry_point
    return next(matches).load()
  File "/usr/local/Cellar/python@3.9/3.9.5/Frameworks/Python.framework/Versions/3.9/lib/python3.9/importlib/metadata.py", line 77, in load
    module = import_module(match.group('module'))
  File "/usr/local/Cellar/python@3.9/3.9.5/Frameworks/Python.framework/Versions/3.9/lib/python3.9/importlib/__init__.py", line 127, in import_module
    return _bootstrap._gcd_import(name[level:], package, level)
  File "<frozen importlib._bootstrap>", line 1030, in _gcd_import
  File "<frozen importlib._bootstrap>", line 1007, in _find_and_load
  File "<frozen importlib._bootstrap>", line 986, in _find_and_load_unlocked
  File "<frozen importlib._bootstrap>", line 680, in _load_unlocked
  File "<frozen importlib._bootstrap_external>", line 855, in exec_module
  File "<frozen importlib._bootstrap>", line 228, in _call_with_frames_removed
  File "/usr/local/Cellar/mathlibtools/1.0.0/libexec/lib/python3.9/site-packages/mathlibtools/leanproject.py", line 7, in <module>
    from git.exc import GitCommandError # type: ignore
  File "/usr/local/Cellar/mathlibtools/1.0.0/libexec/lib/python3.9/site-packages/git/__init__.py", line 89, in <module>
    raise ImportError('Failed to initialize: {0}'.format(exc)) from exc
ImportError: Failed to initialize: [Errno 2] No such file or directory

I deleted my project to get a fresh copy but I can no longer leanproject new my_project

[Julian Berman]

If you run git --help, that works I assume?

[Julian Berman]

Does the directory you're sitting in when running that exist?

[Julian Berman]

It looks like it may not possibly? Run e.g. cd ~/Desktop -- does leanproject new work there?

[Julian Berman]

(you can delete a directory but still be sitting inside it, because computers are great)

[Hanting Zhang]

:dizzy: Yes, that was the problem

[Hanting Zhang]

leanproject works now finally. Thanks again

[Julian Berman]

np