Zulip Chat Archive
Stream: general
Topic: Error in `alias.lean`?
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.
Gabriel Ebner (May 27 2020 at 14:21):
Can you post the output of lean --version?
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?
Bryan Gin-ge Chen (May 27 2020 at 14:26):
Ah, I just looked it up, it says 3.14.0.
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?
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.
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.
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
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
Kevin Buzzard (May 27 2020 at 14:32):
Another possibility is that he just doesn't have the modern tooling installed at all
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.
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
Bryan Gin-ge Chen (May 27 2020 at 14:34):
https://leanprover-community.github.io/get_started.html#regular-install
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
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.
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.
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.
Sebastien Gouezel (May 27 2020 at 16:47):
If it doesn't work, maybe the vscode extension will install elan for you.
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.
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
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
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.)
Bryan Gin-ge Chen (May 27 2020 at 16:53):
You could try putting #eval lean.version in a file in the project somewhere.
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.
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. ;)
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.
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).
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?
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?
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...
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).
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
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. ;)
Jasmin Blanchette (May 27 2020 at 17:35):
Could it be that I have a too old (2018) version of the VS Code plugin?
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
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. :)
Sebastian Ullrich (May 27 2020 at 17:39):
Did you open mathlib as a project using File > Open Folder?
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.
Jasmin Blanchette (May 27 2020 at 17:41):
@Sebastian Ullrich that did the trick. Thank you so much!
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?
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".
Jasmin Blanchette (May 27 2020 at 17:42):
I think so. I think that's what Johannes did in 2018.
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?
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.
Jasmin Blanchette (May 27 2020 at 17:45):
Ah, I see. Indeed, I see 3.4.2 in there.
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: Dec 20 2023 at 11:08 UTC