leanproject stopped working

Stream: new members

[Julian Külshammer]

I don't know what I did wrong but at some point leanproject stopped working properly for me. I have an old copy of the tutorials (and other old lean projects) which I can open and edit as usual but anything I downloaded recently takes ages to compile. I tried to go through the installation guide again (Windows) but it didn't help. When running leanproject get I receive a warning that the authenticity of host can't be established which I didn't get before. When I click OK I get an Error cloning via SSH, trying HTTPS... and then WARNING: leanpkg configurations not specifying path = "src" are deprecated. Any idea what I can do to resolve this mess?

[Bryan Gin-ge Chen]

Can you give an example of what you're trying to do? If you're working mostly on mathlib you shouldn't need to run leanproject get all too often, but you will run leanproject get-cache a lot when switching branches.

[Julian Külshammer]

At the moment I am working mostly on mathlib, yes. As I said, the first thing I noticed was that every file took at some point ages to compile. I then tried to remove the folders (because in some other topic I had read that that had helped and running leanproject get again lead to this weird SSH error. leanproject get-cachegives no error and claims to have found local mathlib oleans.

[Kevin Buzzard]

Within mathlib, try git pull and then leanproject get-cache

[Kevin Buzzard]

switch to master branch. I guess what Bryan said. What are you trying to do? Work on a branch of mathlib? Just get a scratch file compiling with master? etc etc.

[Bryan Gin-ge Chen]

leanproject -f get-cache will redownload the olean files. This can be useful if somehow the cache for a commit got corrupted, though I think this only tends to happen if you're using git hooks or running leanproject mk-cache a lot.

[Julian Külshammer]

git pull says Already up to date. leanproject -f get-cache downloaded something, but the orange bar doesn't disappear just opening any file. Just creating a new file and writing #eval 1+1 worked in no time at all.

[Yakov Pechersky]

Did you do Restart Lean in vscode? (are you in vscode?)

[Julian Külshammer]

Yes, working in vscode which I also reinstalled today to see whether this was the problem. Restarting now also didn't help.

[Bryan Gin-ge Chen]

If you run elan show in your mathlib directory, what does the "active toolchain" section say? Mine looks like this:

active toolchain
----------------

leanprover-community-lean-3.24.0 (overridden by '/.../mathlib/leanpkg.toml')
Lean (version 3.24.0, commit 13007ebb4de6, Release)

[Kevin Buzzard]

What happens if you try to compile mathlib on the command line? In mathlib, try lean --make src. If you have the correct oleans and the correct lean, this should return with no output after a few seconds. If it starts recompiling stuff then at the very least you will have to do leanproject get-cache again.

[Julian Külshammer]

--------------------

stable (default)
leanprover-community-lean-3.14.0
leanprover-community-lean-3.16.5
leanprover-community-lean-3.17.0
leanprover-community-lean-3.17.1
leanprover-community-lean-3.23.0
leanprover-community-lean-3.24.0
3.4.2

active toolchain
----------------

leanprover-community-lean-3.24.0 (overridden by '\\?\C:\Users\julia\Documents\lean-projects\mathlib\leanpkg.toml')
Lean (version 3.24.0, commit 13007ebb4de6, Release)

[Bryan Gin-ge Chen]

What branch are you trying to work on? What does git status say?

[Kevin Buzzard]

One problem I have seen in the past, with people who had set Lean up ages ago, is that in the dim and distant past people used to do things like setting a LEAN_PATH environment variables. Nowadays this should not be set. Another thing I've seen is that the default lean binary for VS Code is overridden to point to e.g. some nightly from 2018, which again might have been the thing to do in 2018.

[Julian Külshammer]

At the moment I just got a fresh copy of master and git status says:

Your branch is up to date with 'origin/master'.

nothing to commit, working tree clean```

[Kevin Buzzard]

so now leanproject get-cache and then lean --make src in the root directory of the repo

[Kevin Buzzard]

see if we can get it working on the command line

[Julian Külshammer]

I tried it and lean --make src didn't finish, even after running leanproject get-cache.

[Kevin Buzzard]

You mean you got some output, e.g. it started compiling a bunch of files?

[Kevin Buzzard]

lean --version?

[Julian Külshammer]

Lean (version 3.24.0, commit 13007ebb4de6, Release)

[Julian Külshammer]

No, I get no output at all (at least for the time I waited).

[Kevin Buzzard]

Oh -- are you on Windows? I think that windows produces no output (this drives me nuts)

[Julian Külshammer]

Yes, I am on windows.

[Kevin Buzzard]

mac and linux it prints which files it's compiling to STDOUT or STDERR

[Kevin Buzzard]

So in ~/.mathlib do you have a file 13007ebb4de6.....tar.xz?

[Kevin Buzzard]

wait no

[Kevin Buzzard]

not that, that's the lean commit

[Kevin Buzzard]

What's the last commit according to git log and what does leanpkg.toml say?

[Alex J. Best]

Have you tried updating leanproject (as a pip package)

[Kevin Buzzard]

!!!

[Kevin Buzzard]

Nice idea!

[Kevin Buzzard]

$ leanproject --version
leanproject, version 1.0.0

[Eric Wieser]

I think if a cache download fails (eg network errors), you end up with a corrupt cache that get-cache refuses to refetch

[Bryan Gin-ge Chen]

leanproject -f get-cache should force a redownload though.

[Kevin Buzzard]

Yes I was going to try and locate the cache file but I don't know its name yet. It's commit-hash.tar.xz in a directory called ~/.mathlib on my system

[Kevin Buzzard]

Just to see if it had the right size

[Julian Külshammer]

How do I update leanproject as a pip package?

[Julian Külshammer]

I think I found that tar.xz file and it is 34 MB.

[Bryan Gin-ge Chen]

I usually just run pip install --upgrade mathlibtools, but I'm not sure if this is a good idea universally. It could depend on your python environment / how you installed mathlibtools.

[Julian Külshammer]

Thanks for all the suggestions. Unfortunately none of them worked so far.

[Kevin Buzzard]

what is output of leanproject --version?

[Julian Külshammer]

leanproject, version 1.0.0

[Julian Külshammer]

I just noticed that I didn't reply to what leanpkg.toml says:

[package]
name = "mathlib"
version = "0.1"
lean_version = "leanprover-community/lean:3.24.0"
path = "src"

[dependencies]

[Julian Külshammer]

And git log now gives

Author: Jesse Michael Han <hyrodi@gmail.com>
Date:   Wed Jan 27 08:42:04 2021 +0000
refactor(category_theory/abelian): golf `mono_of_kernel_ι_eq_zero` (#5914)
Co-authors: `lean-gptf`, Stanislas Polu

[Johan Commelin]

looks fine

[Julian Külshammer]

The leanpkg.toml of the old tutorials folder I have (and where lean works even opening the corresponding files) says the same. It just doesn't work for things I currently tried to download using leanproject get.

[Patrick Massot]

Maybe we should try to have a quick video chat where we could see exactly what you're doing and how your computer reacts.

[Julian Külshammer]

Sure. Which platform?

[Patrick Massot]

For future readers: it turned out Julian had a somehow corrupted 3.24 toolchain in $HOME/.elan. Removing and reinstalling that toolchain solved the issue.

[Julian Külshammer]

Thanks again for all who offered their help, especially to Patrick for finally fixing it.

[Kevin Buzzard]

Usually people's problems are far less weird!

[Julian Külshammer]

I could reproduce the error and I think I found out why it stopped working. While trying to resolve #1534 I tried to add nat.div_add_mod just after nat.mod_add_div. If I understand correctly, I left mathlib and went to chore lean and editing this seems not to be such a good idea. :upside_down:

[Johan Commelin]

Aah, that makes sense.

[Johan Commelin]

Changing core is a different type of game (-; You'll need to work on a different repo, and issue some elan commands to make things work. I would avoid it if you can.

[Johan Commelin]

That makes me think: @Sebastian Ullrich would it be possible for elan to make the lean toolchains in ~/.elan read-only? That way you only modify core if you explicitly work on a manually cloned repo.

[Sebastian Ullrich]

I would accept a PR for that. Would bring elan one step closer to Nix :grinning_face_with_smiling_eyes: .

[Johan Commelin]

I'll put it on my todo list (-;

[Johan Commelin]

I've never looked at the source for elan though

[Patrick Massot]

Johan, do you know the language that Sebastian used to write elan? This may be a shock...

[Adam Topaz]

Patrick Massot said:

Johan, do you know the language that Sebastian used to write elan? This may be a shock...

It's rust right?

[Anne Baanen]

It is! Because what other language features:

• zero-cost abstractions
• move semantics
• guaranteed memory safety
• threads without data races
• trait-based generics
• pattern matching
• type inference
• minimal runtime
• and efficient C bindings?

[Alex J. Best]

Looks like elan already sets some permissions for zip archives on unix at https://github.com/Kha/elan/blob/40e38ccf7392a5a281475197ee114283a855431d/src/elan-dist/src/component/package.rs#L106 so this looks pretty doable with https://doc.rust-lang.org/std/fs/fn.set_permissions.html