Imports

Stream: lean4

[Logan Murphy]

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]

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]

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]

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]

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

[Arthur Paulino]

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]

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

[Arthur Paulino]

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

[Sebastian Ullrich]

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

[Wojciech Nawrocki]

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]

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]

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]

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]

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]

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

[Wojciech Nawrocki]

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]

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]

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]

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]

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]

It's Ctrl+Shift+X in VS Code

[Marc Huisinga]

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]

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

[z battleman]

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]

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

[Mario Carneiro]

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]

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