leanproject new projet fails if default toolchain is not set up correctly

[gebner]

$ leanproject new projet
error: ill-formed search path entry '/home/gebner/lean4/library', should be of form 'pkg=path'
Traceback (most recent call last):
  File "/nix/store/hyr4i0kbvrnxs71z42pgdp43f3ilqw8l-mathlib-tools-0.0.3/bin/.leanproject-wrapped", line 9, in <module>
    sys.exit(cli())
  File "/nix/store/ix2kqmlqy2mbsdqydnfrzylxa0hligxg-python3.7-click-7.0/lib/python3.7/site-packages/click/core.py", line 764, in __call__
    return self.main(*args, **kwargs)
  File "/nix/store/ix2kqmlqy2mbsdqydnfrzylxa0hligxg-python3.7-click-7.0/lib/python3.7/site-packages/click/core.py", line 717, in main
    rv = self.invoke(ctx)
  File "/nix/store/ix2kqmlqy2mbsdqydnfrzylxa0hligxg-python3.7-click-7.0/lib/python3.7/site-packages/click/core.py", line 1137, in invoke
    return _process_result(sub_ctx.command.invoke(sub_ctx))
  File "/nix/store/ix2kqmlqy2mbsdqydnfrzylxa0hligxg-python3.7-click-7.0/lib/python3.7/site-packages/click/core.py", line 956, in invoke
    return ctx.invoke(self.callback, **ctx.params)
  File "/nix/store/ix2kqmlqy2mbsdqydnfrzylxa0hligxg-python3.7-click-7.0/lib/python3.7/site-packages/click/core.py", line 555, in invoke
    return callback(*args, **kwargs)
  File "/nix/store/hyr4i0kbvrnxs71z42pgdp43f3ilqw8l-mathlib-tools-0.0.3/lib/python3.7/site-packages/mathlibtools/leanproject.py", line 66, in new
    LeanProject.new(Path(path), cache_url, force_download)
  File "/nix/store/hyr4i0kbvrnxs71z42pgdp43f3ilqw8l-mathlib-tools-0.0.3/lib/python3.7/site-packages/mathlibtools/lib.py", line 390, in new
    proj = cls.from_path(path, cache_url, force_download)
  File "/nix/store/hyr4i0kbvrnxs71z42pgdp43f3ilqw8l-mathlib-tools-0.0.3/lib/python3.7/site-packages/mathlibtools/lib.py", line 218, in from_path
    repo = Repo(path, search_parent_directories=True)
  File "/nix/store/h5i5dyh5nsgc3m7fnql201lrw2qjng78-python3.7-GitPython-3.0.5/lib/python3.7/site-packages/git/repo/base.py", line 133, in __init__
    raise NoSuchPathError(epath)
git.exc.NoSuchPathError: /home/gebner/projet

[PatrickMassot]

leanpkg has the standing assumption that your elan setup is sane. I don't see I could fix that issue, except for hiding the python Traceback.

[gebner]

Most of the leanproject commands don't care about the default lean version set in elan. They all use the version specified in the leanpkg.toml of the current project.

I wonder how many of our users have set 3.4.0 as the default lean version from when they first installed elan. For them leanproject new will fail as well:

$ elan default 3.4.0
$ leanproject new foo
...
mathlibtools.lib.InvalidMathlibProject: This project does not depend on mathlib

[PatrickMassot]

Fixed in 7f0216d.