Zulip Chat Archive

Stream: lean4

Topic: Imports


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?

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

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

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).

Logan Murphy (Feb 27 2021 at 21:40):

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

Arthur Paulino (Jan 18 2022 at 15:16):

This is an old thread but my question suits the topic.
Suppose I have the files a.lean and b.lean such that b.lean imports a.lean.

In Lean 3, when something changes in a.lean, switching to b.lean automatically triggers a recompilation of b.lean. In Lean 4, however, I have to comment and uncomment the import a line in b.lean everytime I change something in a.lean. This is not a serious issue, but gets a bit annoying with time.

Does anyone else experience this? Is it a bug in the Lean 4 VS Code extension?

Sebastian Ullrich (Jan 18 2022 at 15:21):

It's not a bug, see the very end of https://leanprover.github.io/lean4/doc/quickstart.html

Arthur Paulino (Jan 18 2022 at 15:24):

Oh, thanks!!
Any particular reason why the automatic update was dropped?

Sebastian Ullrich (Jan 18 2022 at 15:27):

It was easier to implement in the new server infrastructure. And at least the developers vastly prefer it, I believe.

Wojciech Nawrocki (Jan 18 2022 at 19:00):

To elaborate a bit, the issue was mainly that opening a random file deep within mathlib and accidentally (or even intentionally, to try something out) a line would trigger a massive rebuild. So we decided to make the rebuilding something the user has to decide to do consciously, although there could be an option that restores the Lean 3 behaviour (not implemented atm).

Gabriel Ebner (Jan 18 2022 at 19:17):

So we decided to make the rebuilding something the user has to decide to do consciously,

Rebuilding is not a conscious action though. It happens automatically whenever you open a file. (And with no opt-out, unlike in Lean 3.) Accidentally changing a line in mathlib will still trigger a massive rebuild.

Wojciech Nawrocki (Jan 18 2022 at 19:25):

Only if you save the mathlib file though. (So the assumption was that saving the file is like committing that you do want the change to persist.)

Arthur Paulino (Jan 18 2022 at 19:26):

The manual refreshing of file dependencies doesn't completely solve the problem though, right?
Re-using the example I posted above, but also supposing that b.lean imports such a deep mathlib file that I decided to play with.
But then, I change something in a.lean and I see myself forced to hit ctrl+shift+x in b.lean. Then the avalanche starts.

An alternative solution (or complementary?), although likely harder to implement, is providing a "safe mode", in which the generated olean file wouldn't replace the one used for other imports. So you'd be able to play with files safely, no matter how deep they are in the chain of imports

Gabriel Ebner (Jan 18 2022 at 19:27):

Only if you save the mathlib file though. (So the assumption was that saving the file is like committing that you do want the change to persist.)

I've set vscode to autosave. :-/

Wojciech Nawrocki (Jan 18 2022 at 19:28):

Ah, well, that's the problem then :) Indeed we should probably have more configuration on this to fit people's different setups.

Wojciech Nawrocki (Jan 18 2022 at 19:33):

providing a "safe mode", in which the generated olean file wouldn't replace the one used for other imports.

Iirc Lean 3 now has something like this, see leanprover-community/lean#208.

Arthur Paulino (Jan 18 2022 at 19:42):

That's nice. It tries to accomplish the same goal. But it doesn't provide a safer environment, in the sense that the olean files do get tweaked in the end

Alex J. Best (Jan 18 2022 at 19:43):

Lean 3s old mode is very much un-safe though, if not used with caution you can end up breaking logical consistency. I really like the idea of the new non-auto refreshing, I think it will solve a lot of the orange bars of hell trouble we see reported on Zulip

Arthur Paulino (Jan 18 2022 at 19:51):

Ah well, this "safe mode" can be just opening a copy of the file named with a tag to be ignored by git :shrug:

Siddhartha Gadgil (Jan 19 2022 at 11:08):

Since it was not mentioned above, instead of commenting and uncommenting a.lean one can use the Lean 4: refresh file dependencies vs-code command. This is what I do and it is pretty efficient since this is always close to the top of my recently used commands.

Sebastian Ullrich (Jan 19 2022 at 11:12):

It's Ctrl+Shift+X in VS Code

Marc Huisinga (Jan 19 2022 at 11:41):

Btw, I'm not sure if Ctrl+Shift+X is such a great keybind :sweat_smile:
I picked it more or less arbitrarily because the keys are all close together, not realizing that it conflicts with the "Open extension sidebar window" command when the editor isn't focused ...

Arthur Paulino (Jan 19 2022 at 11:55):

Re Siddhartha: yeah, it's mentioned in the link Sebastian posted :+1:

z battleman (Jun 12 2022 at 17:54):

is there a way to do relative imports that ignore the lean search path? For example, I have a directory structure like

| Foo
    | somemainfile.lean
| Bar
    | adjdacent_files_that_import_files_from_Foo.lean
    | file1.lean
    | file2.lean

The lean search path points to Foo, but I want to import file1.lean into file2.lean. Does anyone know how to get around this? Thanks!

James Gallicchio (Jun 15 2022 at 03:47):

I think you always need to specify the absolute path (in this case Bar.file1)

Mario Carneiro (Jun 15 2022 at 03:48):

In lean 3 there is support for relative paths via import .foo but it caused problems and mathlib straight up bans its use

Mario Carneiro (Jun 15 2022 at 03:49):

from what I can tell this syntax is no longer recognized in lean 4


Last updated: Dec 20 2023 at 11:08 UTC