Cannot import tactic

Stream: general

[Yuhang Lin]

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]

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]

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]

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]

Output of lean --path:
{
"is_user_leanpkg_path": true,
"leanpkg_path_file": "/Users/linyuhang/.lean/leanpkg.path",
"path": [
"/Users/linyuhang/.elan/toolchains/leanprover-community--lean---3.24.0/bin/../library",
"/Users/linyuhang/.elan/toolchains/leanprover-community--lean---3.24.0/bin/../lib/lean/library",
"/Users/linyuhang/.lean/./."
]
}

Layout:
Screenshot-2021-06-24-at-11.33.23-AM.png

[Kevin Buzzard]

There's no path file and no _target

[Kevin Buzzard]

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]

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

[Bryan Gin-ge Chen]

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]

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

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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]

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>
sys.exit(safe_cli())
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
proj().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]

Thank you, I will just copy the work anyway.

[Patrick Massot]

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