Failing to create a lean4 project

Stream: lean4

[Sophie Morel]

Hi, so as usual whenever I try to update mathlib or create a new Lean project, I feel like a total idiot because I fail. This time I tried to follow the instructions there:
https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency
First I updated elan, I have version 2.0.1 now, at least that's what elan -V says.
Then I ran lake +leanprover-community/mathlib4:lean-toolchain new ShinyProject math as instructed, moved to the project folder and tried running lake exe cache get (again as instructed). It tells me
error: dependency 'mathlib' of 'AbstractSimplicialComplex' not in manifest, use `lake update` to update
Well, no problem, I can run lake update. It happily clones a bunch of stuff. Then I try running lake exe cache get and the trouble starts. It downloads 3720 files and panics, as in:

thread '<unnamed>' panicked at 'called `Result::unwrap()` on an `Err` value: Error { kind: UnexpectedEof, message: "failed to fill whole buffer" }', /project/src/ltar.rs:57:34
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread '<unnamed>' panicked at 'called `Result::unwrap()` on an `Err` value: Error { kind: UnexpectedEof, message: "failed to fill whole buffer" }', /project/src/ltar.rs:57:34
thread '<unnamed>' panicked at 'called `Result::unwrap()` on an `Err` value: Error { kind: UnexpectedEof, message: "failed to fill whole buffer" }', /project/src/ltar.rs:57:34
thread '<unnamed>' panicked at 'called `Result::unwrap()` on an `Err` value: Error { kind: UnexpectedEof, message: "failed to fill whole buffer" }', /project/src/ltar.rs:57:34
thread '<unnamed>' panicked at 'called `Result::unwrap()` on an `Err` value: Error { kind: UnexpectedEof, message: "failed to fill whole buffer" }', /project/src/ltar.rs:57:34
uncaught exception: leantar failed with error code 101

If I now try to work on lean file inside the project, the lean server refuses to start. (I can send that error message if it helps.)

So what did I screw up this time ? (Last time I wanted to update mathlib so I could do categories stuff, I never succeeded and ended up creating a new project instead, but at least I was able to create the new project...)

[Sophie Morel]

(Sorry if I sound exasperated, I am to be honest ! Why is it never simple for me to upgrade mathlib/create a project ? :sob: )

[Moritz Firsching]

I saw the same error today, and then ran lake exe cache get again and then it just worked.

[Patrick Massot]

Everybody is exasperated here. We are still in the early days of Lean 4 and lakeisn't yet really usable. We are sorry about that.

[Patrick Massot]

After lake update, try running cp lake-packages/mathlib/lean-toolchain . from the root of your newly created project, and then lake exe cache get.

[Ruben Van de Velde]

In this case, it seems most likely that there was an issue with your internet connection while downloading the cache

[Patrick Massot]

But indeed after reading the error message I agree with Ruben that some internet issue may be involved.

[Sophie Morel]

Okay, I will try all that. I did run lake exe cache get several times already. In fact I tried to do it from the start 4-5 times before I came to whine here.

[Sophie Morel]

So if it's my internet connection, it means that it failed every time and I am basically screwed.

[Ruben Van de Velde]

Maybe try lake exe cache get!, with the exclamation mark? This downloads everything and may help with the corrupted cache you've got

[Sophie Morel]

Patrick, I don't mean to attack anybody, just needed to let off some steam.

[Sophie Morel]

Ruben Van de Velde said:

Maybe try lake exe cache get!, with the exclamation mark? This downloads everything and may help with the corrupted cache you've got

Trying that right now, thanks !

[Ruben Van de Velde]

I think we can all sympathise - the tooling is great when it works, but it still has rough edges when things go wrong

[Sophie Morel]

I mean, I do know that people are working very hard to make Lean4 work and I don't want to disparage their work. I just feel so stupid because every time I try to do anything, it goes wrong and I have to ask for help here.

[Sophie Morel]

Maybe we should have a channel dedicated entirely to expletives ?

[Patrick Massot]

The proper solution is to fix all those issues but it takes some time.

[Sophie Morel]

Well, it seems to be a problem with downloading the files, I've been stuck at 3707/3720 (99% :sad: ) for a while. I guess I just wait and see if the last 13 files eventually download ?

[Ruben Van de Velde]

:fingers_crossed:

[Kevin Buzzard]

Oh when I get stuck in those situations I just ctrl-C to exit and then try it again. The system is quite good at picking up where it left off.

[Sophie Morel]

Ok...

[Sophie Morel]

This time I'm stuck at 3714/3720 instead of 3707/3720. Yay, progress ?

[Kevin Buzzard]

and your internet is OK? And you recently did get!? I would be tempted to just break out and try again. Being stuck is not good.

[Arthur Paulino]

I'm not sure about the details of the new Rust implementation. But in the old Lean 4 implementation, get! would start over from the beginning everytime, ignoring whatever's already been downloaded/cached before

[Sophie Morel]

Yes, that's what it does.

[Sophie Morel]

If I break and try lake exe cache get`` without the !``` then it doesn't even attempt to download the remaining files.

[Kevin Buzzard]

and does lake build work? (in the sense of "returns relatively quickly"?)

[Sophie Morel]

My internet seems to be as stable as it ever gets. I have a wired connection to an ADSL box, which is not the fanciest thing but is also no 64kb model.

[Arthur Paulino]

Are you using some kind of internet connection that imposes some limit in the consumed bandwidth per minute or something like that?

[Sophie Morel]

Arthur Paulino said:

Are you using some kind of internet connection that imposes some limit in the consumed bandwidth per minute or something like that?

I don't know.

[Sophie Morel]

Kevin Buzzard said:

and does lake build work? (in the sense of "returns relatively quickly"?)

Yes it does.

[Sophie Morel]

Now let's see if I can work on an actual Lean file.

[Arthur Paulino]

If you've downloaded most of the files with lake exe cache, then lake build shouldn't take too long, considering that the downloaded files aren't corrupted

[Arthur Paulino]

(that's an optimistic take on the behavior of lake build... I'm not sure if that's actually the case)

[Sophie Morel]

Well, now the Lean server starts. Thanks guys !

[Sophie Morel]

(But I have no idea why it sort of works now when it didn't before...)

[Sophie Morel]

Argh, I get a bunch of errors saying "expected no space before". Did the syntax of rw and exact change in a significant way ? Is there documentation ?

[Sophie Morel]

Ooooh, now simp complains when it made no progress, that is so cool!

[Arthur Paulino]

I suspect that your mathlib clone is out of sync, somehow. Did you do lake update? What does git status say?

[Sophie Morel]

I definitely did a lake update before running lake exe cache get 32443278643724632 times. Let me do it again.

[Arthur Paulino]

No, I meant that lake update shouldn't be called

[Arthur Paulino]

It might change lake-manifest.json and you might end up with the wrong dependencies

[Sophie Morel]

Damn. Well git status says no commits yet.

[Sophie Morel]

But lake exe cache get refused to run the first time and the error message told me to do a lake update... (That was after I had just created the project.)

[Arthur Paulino]

@Mario Carneiro sorry for pinging, but is lake update really advised here?

[Kevin Buzzard]

This is a new project with mathlib as a dependency, right?

[Sophie Morel]

Wait, I figured where some of error messages were coming from, and it is much more basic. Did the turnstile symbol (for indicating that a rw should apply to the current goal) change ?

[Sophie Morel]

Kevin Buzzard said:

This is a new project with mathlib as a dependency, right?

Yup!

[Sophie Morel]

Like, I have a line that says
rw [ShinyLemma] at Hypothesis1 |-
and then Lean complains about the next line. But then I noticed that rw hadn't changed the goal, so I figured the problem is |-. Maybe we use a different symbol now ?

[Ruben Van de Velde]

Using lake update is fine for a project that depends on mathlib (but make sure that the lean toolchain matches, see https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4 )

[Ruben Van de Velde]

Does ⊢ work?

[Patrick Massot]

It's really convenient that mathematicians are masochistic. Otherwise we would have no user.

[Sophie Morel]

That's it, thanks ! I couldn't figure out how to type it in vscode.

[Ruben Van de Velde]

I wasn't aware of a change to |-, but mathlib doesn't use that syntax as far as I can tell, so perhaps it did

[Sophie Morel]

Well it seems to be somehow running now, I just have to update the files (and the turnstiles).

[Patrick Massot]

The |- spelling clashed with |-x|.

[Sophie Morel]

Patrick Massot said:

It's really convenient that mathematicians are masochistic. Otherwise we would have no user.

Oh, we all got trained early with LaTeX... Yes, please hurt me some more, computer !
Excuse me, now I must go and jump in a field of stinging nettles before my usual session of self-whipping. Thanks so much to everybody in this discussion !

[Arthur Paulino]

Patrick Massot said:

It's really convenient that mathematicians are masochistic. Otherwise we would have no user.

I guess anyone who uses a computer to do a bit more than internet browsing is bound to that condition, to some extent :joy:

[Scott Morrison]

I think most of the source of the problem in this thread was not lake, but cache. It sometimes leaves broken files in place after error conditions. Lean relatively recently acquired IO.FS.rename, and it should be used in cache.

[Scott Morrison]

e.g. #7022

[Mario Carneiro]

Arthur Paulino said:

Mario Carneiro sorry for pinging, but is lake update really advised here?

lake update is fine to do in a project that depends on mathlib. It will update your project to the latest version of mathlib. You should not use lake update in mathlib itself though (unless you are a maintainer), as it will update mathlib's dependencies, causing the cache to miss and possibly causing mathlib not to build

[Mario Carneiro]

Scott Morrison said:

I think most of the source of the problem in this thread was not lake, but cache. It sometimes leaves broken files in place after error conditions. Lean relatively recently acquired IO.FS.rename, and it should be used in cache.

Yes, this is the issue. The rust panic message quoted above has been fixed in leantar master, although I haven't released a new version. (This message is complaining that the file was truncated due to an aborted download, and the new version makes this error message clearer.) The rename issue has not yet been fixed but should be relatively simple