Zulip Chat Archive

Stream: lean4

Topic: Imports


view this post on Zulip Logan Murphy (Feb 26 2021 at 15:20):

I seem to be having trouble with importing anything within a lean4 project

I do

$ mkdir new_lean_project && cd new_lean_project
$ leanpkg init Foo
$ leanpkg build Foo

Then I make a new file in new_lean_project called bar.lean. But when I try to import Foo, I get unknown package 'Foo' . Any ideas as to what's going wrong?

view this post on Zulip Scott Kovach (Feb 27 2021 at 01:08):

yep, you need to follow the directory structure suggested here: https://leanprover.github.io/lean4/doc/setup.html#leanpkg
you'll want to place your files in Foo/ and have only one root level lean file

view this post on Zulip Logan Murphy (Feb 27 2021 at 02:17):

Right, I saw that. My directory structure is

new_lean_project
| Foo.lean
| leanpkg.toml
| Build/
| Foo/
 > | bar.lean

And it is in Foo/bar.lean that I cannot get import Foo or import Foo.baz to seem to work

view this post on Zulip Scott Kovach (Feb 27 2021 at 05:19):

oh yeah, I misread. I tried going through the steps and creating this file:

Foo/bar.lean
import Foo.baz -- contains a definition for `x`
import Foo

#check x
#check main

and everything works just fine. make sure you're using the lean4 nightly build. are you able to rebuild with leanpkg build (is it just an editor issue)? maybe you have an old version of the lean4 extension? (it should be 0.0.7).

view this post on Zulip Logan Murphy (Feb 27 2021 at 21:40):

Thank you Scott - I was on the stable release, switched to nightly and everything is working!


Last updated: May 07 2021 at 12:15 UTC