Zulip Chat Archive

Stream: general

Topic: Error in `alias.lean`?


view this post on Zulip Jasmin Blanchette (May 27 2020 at 14:19):

Using mathlib 4d7b8cfdccc93559 (induction branch), I get this weird error in VSCode:

invalid import: tactic.alias
/Users/blanchette/gits/mathlib/src/tactic/alias.lean:42:45: error: invalid character, ' expected

Shouldn't the quotes around 'of' be backticks? Two pairs in the file.

view this post on Zulip Gabriel Ebner (May 27 2020 at 14:21):

Can you post the output of lean --version?

view this post on Zulip Bryan Gin-ge Chen (May 27 2020 at 14:25):

They should be, but I don't think that's what's going on. I suspect you're using a version of Lean that doesn't allow nested comment blocks in doc strings (older than 3.6.0c). What is lean_version in the leanpkg.toml in that branch?

view this post on Zulip Bryan Gin-ge Chen (May 27 2020 at 14:26):

Ah, I just looked it up, it says 3.14.0.

view this post on Zulip Bryan Gin-ge Chen (May 27 2020 at 14:27):

Maybe try restarting Lean in VS Code if you were recently working on a branch of mathlib that used an older version of Lean?

view this post on Zulip Jannis Limperg (May 27 2020 at 14:29):

This is my branch, rebased onto master just two hours ago. It works for me, so something seems to be wrong with Jasmin's setup, but we weren't able to figure out what.

view this post on Zulip Bryan Gin-ge Chen (May 27 2020 at 14:30):

I strongly suspect that Jasmin's computer is using an out-of-date version of Lean.

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:30):

For an old hand like Jasmin, one risk is that the VS Code settings are wrong. Hang on

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:31):

Check Lean: Executable Path in VS Code settings. In 2018 people used to sometimes tinker with this, before elan

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:32):

Another possibility is that he just doesn't have the modern tooling installed at all

view this post on Zulip Bryan Gin-ge Chen (May 27 2020 at 14:33):

Yeah, with the recommended setup now (using elan) that setting should either be lean or be blank. elan will figure out what version of Lean to use and also download and install it for you if you don't have it.

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:34):

In the old days I used to have this pointing to 3.3.0 or a nightly or whatever

view this post on Zulip Bryan Gin-ge Chen (May 27 2020 at 14:34):

https://leanprover-community.github.io/get_started.html#regular-install

view this post on Zulip Jasmin Blanchette (May 27 2020 at 16:44):

I think Kevin is right. It says: /Users/blanchette/.elan/bin/lean as the executable path. That's probably some left over from what Johannes Hölzl did to my computer. :S

view this post on Zulip Jasmin Blanchette (May 27 2020 at 16:45):

I'll need to modernize, but I don't even understand from which state I'm starting, because of this 2018 setup by someone else.

view this post on Zulip Sebastien Gouezel (May 27 2020 at 16:46):

Just clear this line, and restart Vscode. If it works, it means elan is installed, and you don't have anything more to do.

view this post on Zulip Bryan Gin-ge Chen (May 27 2020 at 16:47):

You may also need to run elan self update in your command line if you're using a version of elan from 2018.

view this post on Zulip Sebastien Gouezel (May 27 2020 at 16:47):

If it doesn't work, maybe the vscode extension will install elan for you.

view this post on Zulip Sebastien Gouezel (May 27 2020 at 16:48):

It it doesn't, you might need to install elan following the main instructions, and then start vscode again.

view this post on Zulip Jasmin Blanchette (May 27 2020 at 16:49):

Oh joy:

info: checking for self-updates
info: downloading self-update
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: None })
error: could not download file from 'https://github.com/Kha/elan/releases/download/v0.10.2","user_id":null%7D%7D/elan-x86_64-apple-darwin.tar.gz' to '/var/folders/2g/0fq82_3d4m1gxnz8tqbt1rd80000gn/T/elan-update.wa5jqrIMiePt/elan-x86_64-apple-darwin.tar.gz'
info: caused by: http request returned an unsuccessful status code: 404

view this post on Zulip Bryan Gin-ge Chen (May 27 2020 at 16:50):

Oof. Maybe try reinstalling using: curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh

view this post on Zulip Jasmin Blanchette (May 27 2020 at 16:52):

@Gabriel Ebner I still have the same oddities as before after removing the entry in VS Code options and relaunching. How do I print the version of Lean that VS Code is running? (On the command line, it says Lean (version 3.14.0, commit 0947586ef2af, Release) as ever, but I'm guessing that's not the same.)

view this post on Zulip Bryan Gin-ge Chen (May 27 2020 at 16:53):

You could try putting #eval lean.version in a file in the project somewhere.

view this post on Zulip Sebastian Ullrich (May 27 2020 at 16:57):

If you call lean inside the project directory, it should use the same version as VS Code.

view this post on Zulip Jasmin Blanchette (May 27 2020 at 16:59):

I don't like the phrase "it should". Based on "it shoulds", I'm using 3.14.0 and I should not be having the error I'm having. ;)

view this post on Zulip Jasmin Blanchette (May 27 2020 at 17:00):

And indeed, #eval lean.version is 3.4.2 in VS Code, whereas lean --version in the repository (mathlib) where my .lean file lives says 3.14.0.

view this post on Zulip Jasmin Blanchette (May 27 2020 at 17:02):

OK, well, thanks all for the help. I'll try to figure out what happens on my weird installation or wipe it clean or something (if I can find all the config files for all the tools involved).

view this post on Zulip Sebastian Ullrich (May 27 2020 at 17:03):

Did you clear the setting and restart VS Code? Does which lean on the cmdline point to elan as well?

view this post on Zulip Bryan Gin-ge Chen (May 27 2020 at 17:04):

Do you get the same results if you try lean --version from VS Code's built-in terminal?

view this post on Zulip Sebastian Ullrich (May 27 2020 at 17:06):

I would hope that we don't have that much mutable state flying around that a fresh installation should be necessary. It's mostly settings like the VS Code one and your PATH. The elan update is broken though, yes...

view this post on Zulip Jasmin Blanchette (May 27 2020 at 17:32):

I had cleared the setting (or rather set it to "lean") and restarted VS Code. which lean says /Users/blanchette/.elan/bin/lean (which self-identifies as 3.14.0).

view this post on Zulip Jasmin Blanchette (May 27 2020 at 17:33):

Bryan: Interesting. In a VS Code terminal, I get

gakubatsu ~$ lean --version
Lean (version 3.4.2, commit cbd2b6686ddb, Release)
gakubatsu ~$ which lean
/Users/blanchette/.elan/bin/lean

view this post on Zulip Jasmin Blanchette (May 27 2020 at 17:34):

@Sebastian Ullrich my PATH in VS Code terminal starts with /Users/blanchette/.elan/bin:. Again, I don't trust the word "mostly". Both items your mention are fine, yet I have the problem. ;)

view this post on Zulip Jasmin Blanchette (May 27 2020 at 17:35):

Could it be that I have a too old (2018) version of the VS Code plugin?

view this post on Zulip Bryan Gin-ge Chen (May 27 2020 at 17:35):

Hmm, the output from the VS Code terminal looks like it's being run in your home directory. What happens if you cd to the mathlib directory there?

The VS Code plugin should auto-update. The latest version is 0.15.15

view this post on Zulip Jasmin Blanchette (May 27 2020 at 17:38):

The existence of ~/.vscode/extensions/jroesch.lean-0.15.15/suggests I have the latest and greatest extension. Yeah. :)

view this post on Zulip Sebastian Ullrich (May 27 2020 at 17:39):

Did you open mathlib as a project using File > Open Folder?

view this post on Zulip Jasmin Blanchette (May 27 2020 at 17:40):

No, I just opened the one file I wanted to edit from the command line, from the mathlib directory. Let me try.

view this post on Zulip Jasmin Blanchette (May 27 2020 at 17:41):

@Sebastian Ullrich that did the trick. Thank you so much!

view this post on Zulip Bryan Gin-ge Chen (May 27 2020 at 17:41):

Ah, that would do it. I'm surprised anything worked at all. Did you set up a global install of mathlib at some point?

view this post on Zulip Bryan Gin-ge Chen (May 27 2020 at 17:42):

Usually if you just open a standalone file, all the imports just fail outright with "file not found".

view this post on Zulip Jasmin Blanchette (May 27 2020 at 17:42):

I think so. I think that's what Johannes did in 2018.

view this post on Zulip Jasmin Blanchette (May 27 2020 at 17:42):

Do you know how to remove this global mathlib install that's causing my machine to behave differently from others?

view this post on Zulip Bryan Gin-ge Chen (May 27 2020 at 17:44):

I'm not 100% sure but from inspecting the source of leanpkg real quick I think deleting ~/.lean should do it.

view this post on Zulip Jasmin Blanchette (May 27 2020 at 17:45):

Ah, I see. Indeed, I see 3.4.2 in there.

view this post on Zulip Jasmin Blanchette (May 27 2020 at 17:46):

Thanks a lot everybody. I shouldn't have waited two years to get my stuff in order. ;)


Last updated: May 16 2021 at 21:11 UTC