Zulip Chat Archive

Stream: general

Topic: Cannot import tactic

Yuhang Lin (Jun 24 2021 at 09:24):

I am trying to import Lean's standard tactics in VSC but there is an error message stating "invalid import: tactic". How to solve this problem?

Julian Berman (Jun 24 2021 at 09:31):

tactic comes from mathlib (not strictly Lean's "standard" tactics) -- what did you run? If you're trying to create a project you should follow these instructions if you haven't already: https://leanprover-community.github.io/leanproject.html#creating-a-new-project, or otherwise let us know what you're trying to do.

Yuhang Lin (Jun 24 2021 at 09:37):

Thank you for answering. I tried to add mathlib to that project using "leanproject add-mathlib" in the project folder. But an error message occurred saying "Invalid git repository".

Julian Berman (Jun 24 2021 at 09:47):

Ah. You have an existing project? How did you create it? Can you show what the layout of your project looks like? And if you know how to do so, the output of lean --path run from your project directory?

Yuhang Lin (Jun 24 2021 at 10:34):

Output of lean --path:
"is_user_leanpkg_path": true,
"leanpkg_path_file": "/Users/linyuhang/.lean/leanpkg.path",
"path": [


Kevin Buzzard (Jun 24 2021 at 11:42):

There's no path file and no _target

Kevin Buzzard (Jun 24 2021 at 11:43):

Are you working on mathlib or on a project which has mathlib as a dependency? If this is a new project then why not just follow the instructions in the link above for making a new lean project?

Yuhang Lin (Jun 24 2021 at 11:46):

The project has no mathlib dependency. I just wonder how can I add that to the project?

Bryan Gin-ge Chen (Jun 24 2021 at 12:00):

leanproject add-mathlib from the project directory (the same directory that contains leanpkg.toml and .gitignore) should be the way to do it. I'm not sure why it failed earlier, are you sure you ran it in the correct directory?

Yuhang Lin (Jun 24 2021 at 18:30):

Yes, I am pretty sure I did that in the correct directory as I checked using "ls" command.

Bryan Gin-ge Chen (Jun 24 2021 at 18:31):

Can you try running leanproject --debug add-mathlib and pasting the output that appears into Zulip?

Bryan Gin-ge Chen (Jun 24 2021 at 18:32):

If all else fails, running leanproject new new_package_name should create a new Lean project with a dependency on mathlib. Maybe you could try copying your work into a new project created that way.

Yuhang Lin (Jun 24 2021 at 18:51):

Traceback (most recent call last):
File "/Users/linyuhang/opt/anaconda3/lib/python3.8/site-packages/mathlibtools/lib.py", line 330, in from_path
repo = Repo(path, search_parent_directories=True)
File "/Users/linyuhang/opt/anaconda3/lib/python3.8/site-packages/git/repo/base.py", line 181, in __init__
raise InvalidGitRepositoryError(epath)
git.exc.InvalidGitRepositoryError: /Users/linyuhang/Downloads/tutorials

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
File "/Users/linyuhang/opt/anaconda3/bin/leanproject", line 8, in <module>
File "/Users/linyuhang/opt/anaconda3/lib/python3.8/site-packages/mathlibtools/leanproject.py", line 341, in safe_cli
handle_exception(err, str(err))
File "/Users/linyuhang/opt/anaconda3/lib/python3.8/site-packages/mathlibtools/leanproject.py", line 63, in handle_exception
raise exc
File "/Users/linyuhang/opt/anaconda3/lib/python3.8/site-packages/mathlibtools/leanproject.py", line 339, in safe_cli
cli() # pylint: disable=no-value-for-parameter
File "/Users/linyuhang/opt/anaconda3/lib/python3.8/site-packages/click/core.py", line 829, in __call__
return self.main(*args, **kwargs)
File "/Users/linyuhang/opt/anaconda3/lib/python3.8/site-packages/click/core.py", line 782, in main
rv = self.invoke(ctx)
File "/Users/linyuhang/opt/anaconda3/lib/python3.8/site-packages/click/core.py", line 1259, in invoke
return _process_result(sub_ctx.command.invoke(sub_ctx))
File "/Users/linyuhang/opt/anaconda3/lib/python3.8/site-packages/click/core.py", line 1066, in invoke
return ctx.invoke(self.callback, **ctx.params)
File "/Users/linyuhang/opt/anaconda3/lib/python3.8/site-packages/click/core.py", line 610, in invoke
return callback(*args, **kwargs)
File "/Users/linyuhang/opt/anaconda3/lib/python3.8/site-packages/mathlibtools/leanproject.py", line 99, in add_mathlib
File "/Users/linyuhang/opt/anaconda3/lib/python3.8/site-packages/mathlibtools/leanproject.py", line 51, in proj
return LeanProject.from_path(Path('.'), cache_url, force_download,
File "/Users/linyuhang/opt/anaconda3/lib/python3.8/site-packages/mathlibtools/lib.py", line 332, in from_path
raise InvalidLeanProject('Invalid git repository')
mathlibtools.lib.InvalidLeanProject: Invalid git repository

Yuhang Lin (Jun 24 2021 at 18:52):

Thank you, I will just copy the work anyway.

Patrick Massot (Jun 24 2021 at 19:20):

Which command gave you this output? Did you try leanproject new new_package_name? Could you paste the output of leanproject get tutorials?

Last updated: Aug 03 2023 at 10:10 UTC