How does one import a sibling .lean file in a lake proj...

Stream: lean4

[Daniel Donnelly]

image.png

My goal is basic. I just want to import a "declarations.lean" file that declares a bunch of variables that will be used later on.

Is this possible? How can I get importing to work?

[Eric Wieser]

Dropping the .leanin the import line might work

[Eric Wieser]

Though you might also need to open the folder under your lean4 folder in vscode

[Daniel Donnelly]

Eric Wieser said:

Dropping the .leanin the import line might work

Doesn't work - same error essentially

[Eric Wieser]

To be clear, import Hello.lean is certainly an error and it should be import Hello

[Mario Carneiro]

you also need to either put hello2 in Hello/Hello2.lean and import it as import Hello.Hello2, or declare a separate Hello2 project in your lakefile

[Mario Carneiro]

the usual project structure has a folder Hello/ containing all your sources for the Hello package

[Eric Wieser]

Ah, so lake enforces one project per top-level directory?

[Mario Carneiro]

no, but if you want multiple projects then you have to declare multiple projects

[Mario Carneiro]

there are also more elaborate globs and things you can use to import files at other paths, but they are not by default

[Daniel Donnelly]

@Mario Carneiro K I followed ur guys' instructions:
image.png

[Mario Carneiro]

that's a lake version issue, go into the lakefile and change defaultTarget to default_target

[Eric Wieser]

What's causing all our new users to have a bad lake version?

[Mario Carneiro]

the problem being that when you ran lake new hello it was with an older version of lake (your global install) than the version specified in the lean-toolchain

[Eric Wieser]

Is it people who installed Lean4 a long time ago, or are the instructions on the MSR website leading people to the old version?

[Mario Carneiro]

the former

[Mario Carneiro]

I think you have to run elan update leanprover/lean4:nightly to update your global install

[Daniel Donnelly]

Okay, I changed defaultTarget to default_target, then had to restart vscode, now getting this:
image.png
Granted I moved the files back out of the folder, but it's the same error essentially either way. ;\

[Daniel Donnelly]

I'm already using nightly I think

[Daniel Donnelly]

@Mario Carneiro @Eric Wieser :D

[Chris Bailey]

Remove lean_packages, and I would look at something like std4 to understand the module structure. The one you're using isn't going to work.

[Daniel Donnelly]

@Daniel Donnelly @Chris Bailey did, that same lean startup errors as last screenshot

[Chris Bailey]

Can you post the contents of your lakefile

[Daniel Donnelly]

import Lake
open Lake DSL

package «hello3» {
  -- add any package configuration options here
}

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

@[default_target]
lean_lib «Hello3» {
  -- add any library configuration options here
}

@Chris Bailey

[Daniel Donnelly]

Anyone have an idea on this? I would like to do some coding, but I can't really import any math theory library yet

[Siddhartha Gadgil]

If you have to import Hello2 in Hello, you need to do one of the following:

• (recommended) Have Hello2.lean in the folder Hello3and use import Hello3.Hello2- ideally Hello.lean should also be in this folder.
• Have a lean_lib Hello2 in the lakefile

[Daniel Donnelly]

@Siddhartha Gadgil I tried the first one already

[Daniel Donnelly]

I had a folder with the right name

[Siddhartha Gadgil]

What was the error?

[Daniel Donnelly]

@Siddhartha Gadgil still getting this:
image.png

[Daniel Donnelly]

See the lower right messages about LSP stuff?

[Mario Carneiro]

are you running the lean 3 extension?

[Daniel Donnelly]

So I have yet to successfully create a project that can import mathlib nor one that can just import a file next to it

[Daniel Donnelly]

lean4

[Mario Carneiro]

or I guess the lean in your folder could be resolving to lean 3 and the lean 4 extension is talking to it

[Siddhartha Gadgil]

You seem to be importing the wrong way around. In hello4 try import Hello3.Hello3

[Mario Carneiro]

your import syntax is still wrong though

[Daniel Donnelly]

Lean3 is not installed

[Siddhartha Gadgil]

The crash seems to be because hello4 is not part of a target, so Lean will have no idea what to do.

[Mario Carneiro]

you also should probably have a Hello3.lean file at the root that imports everything in your project

[Mario Carneiro]

and what's up with those () after hello4?

[Mario Carneiro]

it's not a function

[Daniel Donnelly]

Okay, I clicked on error, it said to lake update, so doing that now in terminal in root of project
it's doing something; hold up

[Mario Carneiro]

did you try using the lake default setup?

[Mario Carneiro]

you seem to have deleted and moved some files

[Mario Carneiro]

the normal setup looks like this:

lakefile.lean
lean-toolchain
Hello3.lean
Hello3/Foo.lean
Hello3/Bar.lean

[Daniel Donnelly]

@Mario Carneiro still getting this:

Lean (version 4.0.0-nightly-2023-05-16, commit ebc32af2e606, Release)
Watchdog error: Cannot read LSP notification: invalid argument (error code: 22, invalid argument)
[Error - 8:01:27 PM] The Lean 4 server crashed 1 times in the last 3 minutes. The server will not be restarted. See the output for more information.

[Daniel Donnelly]

@Mario Carneiro okay, let me make that lik yours

[Mario Carneiro]

inside Hello3.lean you have

import Hello3.Foo
import Hello3.Bar

and in Hello3/Foo.lean you can use import Hello3.Bar to import the other file

[Daniel Donnelly]

image.png

[Daniel Donnelly]

It seems like the info view comes on for 1 second then those errors pop up

[Daniel Donnelly]

:sweat_smile::sweat_smile::sweat_smile:

[Daniel Donnelly]

What should I do if I want to start over from fresh install?

[Mario Carneiro]

does lake build at the console work?

[Mario Carneiro]

also what does lean --version say

[Mario Carneiro]

if you want to remove everything and start fresh, I think it will work to delete the .elan directory from your home folder and then re-run the elan startup script

[Mario Carneiro]

there is a small probability that your lean is corrupted in some way, but I would put more chances on there being some other configuration error

[Daniel Donnelly]

@Mario Carneiro Redid elan like you said, same error as before even with new lake project

[Mario Carneiro]

Mario Carneiro said:

does lake build at the console work?

Mario Carneiro said:

also what does lean --version say

[Mario Carneiro]

what does your project look like now

[Daniel Donnelly]

PS C:\Users\fruit\OneDrive\Desktop\Lean4\foo> lake build
[0/1] Building Foo
PS C:\Users\fruit\OneDrive\Desktop\Lean4\foo> lean --version
Lean (version 4.0.0-nightly-2023-05-16, commit ebc32af2e606, Release)
PS C:\Users\fruit\OneDrive\Desktop\Lean4\foo>

[Daniel Donnelly]

image.png

[Mario Carneiro]

and what about the vscode extension?

[Mario Carneiro]

you can find it in the extensions panel on the left

[Daniel Donnelly]

So since I followed the instructions to a T, you all must be using linux or mac, because I'm on latest windows 10 64 bit 21h2 version

[Daniel Donnelly]

I tried disabling, reenabling, re-installing

[Daniel Donnelly]

the extenson

[Mario Carneiro]

what version is it

[Daniel Donnelly]

Uploading image.png…

[Daniel Donnelly]

Says I'm current

[Mario Carneiro]

link is broken

[Daniel Donnelly]

v0.0.102

[Daniel Donnelly]

Install another version says it's at the top of th elist

[Daniel Donnelly]

So should I revert back

[Mario Carneiro]

from what I can tell, nothing in lean throws the "error 22, invalid argument" error, but it can be generated by an EINVAL from the underlying C code. Maybe an important file is protected or locked for access?

[Daniel Donnelly]

I tried all versions back to 0.0.85 and they all give me the same error

[Mario Carneiro]

I'm not sure whether there is an easy way to test lake server without writing json manually

[Mario Carneiro]

I assume if you just try running lake serve it does nothing and does not terminate

[Mario Carneiro]

(ctrl-c to close it)

[Daniel Donnelly]

Yes that's correct

[Mario Carneiro]

what happens if you just type a line of garbage and hit enter?

[Mario Carneiro]

this is what I get:

$ lake serve
foobar
Watchdog error: Cannot read LSP request: Invalid header field: "foobar\n"

[Daniel Donnelly]

reinstalling vs code from scratch one sec

[Daniel Donnelly]

@Mario Carneiro

PS C:\Users\fruit\OneDrive\Desktop\Lean4\foo3> lake serve
foobar
Watchdog error: Cannot read LSP request: Invalid header field: "foobar\x0d\n"
PS C:\Users\fruit\OneDrive\Desktop\Lean4\foo3>

[Daniel Donnelly]

So I reinstalled, the plugin was ... still installed after reinstalling vscode, but i uninstalled the extension again, and then reiinstalled

[Mario Carneiro]

I assume this won't make a difference, but have you tried lake new Hello without the mathlib dep

[Daniel Donnelly]

Yep, that's what I currently have loaded into vscode

[Mario Carneiro]

I don't suppose the "Lean: Editor" output views have any useful information?

[Daniel Donnelly]

No, they're empty

[Mario Carneiro]

hm, there is some way to spy on the LSP traffic but I forget what it is

[Daniel Donnelly]

https://github.com/microsoft/language-server-protocol-inspector

[Mario Carneiro]

ok you could try that, use ctrl-, to go to the settings, select "workspace" and "open settings (JSON)" and paste

"lean4.trace.server": "verbose",

in there

[Mario Carneiro]

I'm not entirely sure it will work, lean isn't using the node LSP server directly I think

[Daniel Donnelly]

@Mario Carneiro JSON schemas?
image.png

[Mario Carneiro]

I don't think that matters, just put this after it

[Mario Carneiro]

you could also remove it, probably you just misclicked somewhere

[Mario Carneiro]

the "open settings (JSON)" button is up in the top bar next to the tab title

[Daniel Donnelly]

@Mario Carneiro I'm not sure where you want me to add in "lean4.trace.server" : "verbose", that looks like a JSON dict entry, but I'm not sure where to put it

[Mario Carneiro]

the json file that popped up there

[Mario Carneiro]

you can just replace it with

{
  "lean4.trace.server": "verbose"
}

[Daniel Donnelly]

@Mario Carneiro done
Uploading image.png…

[Mario Carneiro]

I think if you click send too quickly it breaks the image link

[Daniel Donnelly]

[...]
            },
            "implementation": {
                "dynamicRegistration": true,
                "linkSupport": true
            },
            "colorProvider": {
                "dynamicRegistration": true
            },
            "foldingRange": {
                "dynamicRegistration": true,
                "rangeLimit": 5000,
                "lineFoldingOnly": true,
                "foldingRangeKind": {
                    "valueSet": [
                        "comment",
                        "imports",
                        "region"
                    ]
                },
                "foldingRange": {
                    "collapsedText": false
                }
            },
            "declaration": {
                "dynamicRegistration": true,
                "linkSupport": true
            },
            "selectionRange": {
                "dynamicRegistration": true
            },
            "callHierarchy": {
                "dynamicRegistration": true
            },
            "semanticTokens": {
                "dynamicRegistration": true,
                "tokenTypes": [
                    "namespace",
                    "type",
                    "class",
                    "enum",
                    "interface",
                    "struct",
                    "typeParameter",
                    "parameter",
                    "variable",
                    "property",
                    "enumMember",
                    "event",
                    "function",
                    "method",
                    "macro",
                    "keyword",
                    "modifier",
                    "comment",
                    "string",
                    "number",
                    "regexp",
                    "operator",
                    "decorator"
                ],
                "tokenModifiers": [
                    "declaration",
                    "definition",
                    "readonly",
                    "static",
                    "deprecated",
                    "abstract",
                    "async",
                    "modification",
                    "documentation",
                    "defaultLibrary"
                ],
                "formats": [
                    "relative"
                ],
                "requests": {
                    "range": true,
                    "full": {
                        "delta": true
                    }
                },
                "multilineTokenSupport": false,
                "overlappingTokenSupport": false,
                "serverCancelSupport": true,
                "augmentsSyntaxTokens": true
            },
            "linkedEditingRange": {
                "dynamicRegistration": true
            },
            "typeHierarchy": {
                "dynamicRegistration": true
            },
            "inlineValue": {
                "dynamicRegistration": true
            },
            "inlayHint": {
                "dynamicRegistration": true,
                "resolveSupport": {
                    "properties": [
                        "tooltip",
                        "textEdits",
                        "label.tooltip",
                        "label.location",
                        "label.command"
                    ]
                }
            },
            "diagnostic": {
                "dynamicRegistration": true,
                "relatedDocumentSupport": false
            }
        },
        "window": {
            "showMessage": {
                "messageActionItem": {
                    "additionalPropertiesSupport": true
                }
            },
            "showDocument": {
                "support": true
            },
            "workDoneProgress": true
        },
        "general": {
            "staleRequestSupport": {
                "cancel": true,
                "retryOnContentModified": [
                    "textDocument/semanticTokens/full",
                    "textDocument/semanticTokens/range",
                    "textDocument/semanticTokens/full/delta"
                ]
            },
            "regularExpressions": {
                "engine": "ECMAScript",
                "version": "ES2020"
            },
            "markdown": {
                "parser": "marked",
                "version": "1.1.0"
            },
            "positionEncodings": [
                "utf-16"
            ]
        },
        "notebookDocument": {
            "synchronization": {
                "dynamicRegistration": true,
                "executionSummarySupport": true
            }
        }
    },
    "initializationOptions": {
        "editDelay": 200,
        "hasWidgets": true
    },
    "trace": "verbose",
    "workspaceFolders": [
        {
            "uri": "file:///c%3A/Users/fruit/OneDrive/Desktop/Lean4/foo3",
            "name": "foo3"
        }
    ]
}


[Trace - 9:38:45 PM] Received response 'initialize - (0)' in 8133ms.
Result: {
    "serverInfo": {
        "version": "0.1.2",
        "name": "Lean 4 Server"
    },
    "capabilities": {
        "workspaceSymbolProvider": true,
        "typeDefinitionProvider": true,
        "textDocumentSync": {
            "willSaveWaitUntil": false,
            "willSave": false,
            "openClose": true,
            "change": 2
        },
        "semanticTokensProvider": {
            "range": true,
            "legend": {
                "tokenTypes": [
                    "keyword",
                    "variable",
                    "property",
                    "function",
                    "namespace",
                    "type",
                    "class",
                    "enum",
                    "interface",
                    "struct",
                    "typeParameter",
                    "parameter",
                    "enumMember",
                    "event",
                    "method",
                    "macro",
                    "modifier",
                    "comment",
                    "string",
                    "number",
                    "regexp",
                    "operator",
                    "decorator",
                    "leanSorryLike"
                ],
                "tokenModifiers": [
                    "declaration",
                    "definition",
                    "readonly",
                    "static",
                    "deprecated",
                    "abstract",
                    "async",
                    "modification",
                    "documentation",
                    "defaultLibrary"
                ]
            },
            "full": true
        },
        "referencesProvider": true,
        "hoverProvider": true,
        "foldingRangeProvider": true,
        "documentSymbolProvider": true,
        "documentHighlightProvider": true,
        "definitionProvider": true,
        "declarationProvider": true,
        "completionProvider": {
            "triggerCharacters": [
                "."
            ],
            "resolveProvider": false
        },
        "codeActionProvider": {
            "workDoneProgress": false,
            "resolveProvider": true,
            "codeActionKinds": [
                "quickfix",
                "refactor"
            ]
        }
    }
}


[Trace - 9:38:45 PM] Sending notification 'initialized'.
Params: {}


[Trace - 9:38:45 PM] Received request 'client/registerCapability - (register_ilean_watcher)'.
Params: {
    "registrations": [
        {
            "registerOptions": {
                "watchers": [
                    {
                        "kind": null,
                        "globPattern": "**/*.ilean"
                    }
                ]
            },
            "method": "workspace/didChangeWatchedFiles",
            "id": "ilean_watcher"
        }
    ]
}


[Trace - 9:38:45 PM] Sending response 'client/registerCapability - (register_ilean_watcher)'. Processing request took 0ms
No result returned.


[Trace - 9:38:45 PM] Sending notification 'textDocument/didOpen'.
Params: {
    "textDocument": {
        "uri": "file:///c%3A/Users/fruit/OneDrive/Desktop/Lean4/foo3/Foo3.lean",
        "languageId": "lean4",
        "version": 1,
        "text": "def hello := \"world\""
    }
}


[Trace - 9:38:45 PM] Sending request 'textDocument/documentSymbol - (1)'.
Params: {
    "textDocument": {
        "uri": "file:///c%3A/Users/fruit/OneDrive/Desktop/Lean4/foo3/Foo3.lean"
    }
}


[Trace - 9:38:45 PM] Sending request 'textDocument/codeAction - (2)'.
Params: {
    "textDocument": {
        "uri": "file:///c%3A/Users/fruit/OneDrive/Desktop/Lean4/foo3/Foo3.lean"
    },
    "range": {
        "start": {
            "line": 0,
            "character": 20
        },
        "end": {
            "line": 0,
            "character": 20
        }
    },
    "context": {
        "diagnostics": [],
        "triggerKind": 2
    }
}


Watchdog error: Cannot read LSP notification: invalid argument (error code: 22, invalid argument)
[Trace - 9:38:45 PM] Sending request 'textDocument/foldingRange - (3)'.
Params: {
    "textDocument": {
        "uri": "file:///c%3A/Users/fruit/OneDrive/Desktop/Lean4/foo3/Foo3.lean"
    }
}

[Error - 9:38:45 PM] The Lean 4 server crashed 1 times in the last 3 minutes. The server will not be restarted. See the output for more information.

That does seem to give more output than usual

[Mario Carneiro]

and it's more promising than I expected: it is completing the initialization handshake correctly, it just gets stuck when opening the file

[Mario Carneiro]

This is still a very weird error. As far as I can tell from this output, it reads the initialize message from stdin, then goes to read the didOpen message and dies by an EINVAL IO error while reading those bytes from stdin (before it has even parsed the message into JSON, let alone opened Foo3.lean)

[Mario Carneiro]

I think I'm basically out of ideas, maybe someone who knows the server better (@Gabriel Ebner @Sebastian Ullrich @Wojciech Nawrocki) might know what's going on. Unfortunately none of the devs use windows AFAIK so the support is sometimes a bit lagged.

[Kevin Buzzard]

@Daniel Donnelly can you download and run my IISc project https://github.com/kbuzzard/IISc-experiments ?

[Notification Bot]

rami3l has marked this topic as resolved.

[Notification Bot]

Eric Wieser has marked this topic as unresolved.

[Eric Wieser]

@rami3l, I don't think you should resolve a thread you didn't start

[rami3l]

@Eric Wieser I'm really sorry, I don't even know I have marked this topic as resolved. Must have been a misclick. My apologies!

[Neil Strickland]

@Daniel Donnelly Did you ever resolve the "Cannot read LSP notification" thing? I am getting this error with everything freshly installed on one Windows 11 machine, despite the fact that everything is working correctly on two other Windows 11 machines with apparently identical configuration, which is very frustrating.

[Daniel Donnelly]

Neil Strickland said:

Daniel Donnelly Did you ever resolve the "Cannot read LSP notification" thing? I am getting this error with everything freshly installed on one Windows 11 machine, despite the fact that everything is working correctly on two other Windows 11 machines with apparently identical configuration, which is very frustrating.

Sorry for late reply. I never resolved that. Just switched projects. Now I'm back at it, and haven't run into the issue. Windows 10. So just try now I guess!