Lake errors on a new project

Stream: lean4

[A.]

Any ideas what is going wrong here?

ali@Alistairs-MBP ~ % lake new test math
ali@Alistairs-MBP ~ % cd test
ali@Alistairs-MBP test % lake update
test: no previous manifest, creating one from scratch
mathlib: cloning https://github.com/leanprover-community/mathlib4.git to './.lake/packages/mathlib'
error: > git clone https://github.com/leanprover-community/mathlib4.git ./.lake/packages/mathlib
error: stderr:
Cloning into './.lake/packages/mathlib'...
error: RPC failed; curl 92 HTTP/2 stream 5 was not closed cleanly: CANCEL (err 8)
error: 7531 bytes of body are still expected
fetch-pack: unexpected disconnect while reading sideband packet
fatal: early EOF
fatal: fetch-pack: invalid index-pack output
error: external command `git` exited with code 128

[A.]

ali@Alistairs-MBP ~ % elan show
installed toolchains
--------------------

stable (default)
...
leanprover/lean4:v4.6.0-rc1

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

stable (default)
Lean (version 4.5.0, commit 1a3021f98e55, Release)

[Ruben Van de Velde]

This seems like a network issue. Can you try again?

[A.]

Yes it has been happening all day

[Ruben Van de Velde]

I'm not sure how to help, then :/

[A.]

Well thanks, your answer suggests I should try again from another location. Maybe I'll get the chance tomorrow or the day after.

[A.]

I'm not sure if this is related, or just an unfortunate coincidence, but on an older project:

ali@Alistairs-MBP exists-unique % lake update
mathlib: updating repository './lake-packages/mathlib' to revision 'd475374f5e4e7ad1260dd93b29d3995ff3129941'
error: ./lake-packages/mathlib/lakefile.lean:6:2: error: 'leanOptions' is not a field of structure 'Lake.PackageConfig'
error: ./lake-packages/mathlib/lakefile.lean:76:2: error: unexpected identifier; expected 'abbrev', 'add_decl_doc', 'axiom', 'builtin_initialize', 'class', 'custom_data', 'declare_opaque_type', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'extern_lib', 'family_def', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'lean_exe', 'lean_lib', 'library_data', 'library_facet', 'macro', 'macro_rules', 'module_data', 'module_facet', 'notation', 'opaque', 'package', 'package_data', 'package_facet', 'postfix', 'prefix', 'register_builtin_option', 'register_option', 'script', 'structure', 'syntax', 'target', 'target_data', 'theorem' or 'unif_hint'
error: ./lake-packages/mathlib/lakefile.lean: package configuration has errors

[Emilie (Shad Amethyst)]

Do you have a lean-toolchain file at the root of your project?

[A.]

I do! It says

leanprover/lean4:v4.2.0-rc1

[Emilie (Shad Amethyst)]

Oh, it should be leanprover/lean4:v4.6.0-rc1, from this mathlib commit

[Emilie (Shad Amethyst)]

Normally lake update should do that for you

[Ruben Van de Velde]

Yeah, this is a known issue when you update over a change in the lakefile syntax

[A.]

Hmm I am obviously very unclear about what lake update is for

[Ruben Van de Velde]

lake update updates your dependencies, so you now depend on the latest version of mathlib

[Ruben Van de Velde]

Unfortunately it has some rough edges, of which this is probably the most prominent

[Ruben Van de Velde]

Try updating your lean-toolchain file manually and running lake update again

[A.]

Thanks! but I didn't actually want to update it; I only started messing with lake update because lake exe cache get was failing. I guess that was a wrong turning.

[Ruben Van de Velde]

Yeah, in that case you'll probably need to revert changes to lake-something.json

[Kevin Buzzard]

Just going through what others have already said: for the original issue: I can't reproduce, so this is more evidence that it's a network issue at your end:

buzzard@brutus:~/crap$ lake new test math
buzzard@brutus:~/crap$ cd test
buzzard@brutus:~/crap/test$ lake update
test: no previous manifest, creating one from scratch
mathlib: cloning https://github.com/leanprover-community/mathlib4.git to './.lake/packages/mathlib'
std: cloning https://github.com/leanprover/std4 to './.lake/packages/std'
Qq: cloning https://github.com/leanprover-community/quote4 to './.lake/packages/Qq'
(etc etc)

For the second one, unfortunately indeed this is expected; follow the instructions for updating a project here if you want to update (and it sounds like you don't), and if you're in a mess after typing lake update before that curl command (which edits the lean-toolchain to what it needs to be) then probably you can use git to revert back to your former state, by just dumping all the changes that were made since you started tinkering.

[A.]

I have travelled two hundred miles but still the same problem as at the top of this thread :sad: . I understand it's probably not a Lean problem as such but I am at a bit of a loss.

[Mario Carneiro]

are you able to run the git clone https://github.com/leanprover-community/mathlib4.git ./.lake/packages/mathlib line manually?

[A.]

Apparently not

ali@Alistairs-MBP test % git clone https://github.com/leanprover-community/mathlib4.git ./.lake/packages/mathlib
Cloning into './.lake/packages/mathlib'...
remote: Enumerating objects: 280781, done.
remote: Counting objects: 100% (324/324), done.
remote: Compressing objects: 100% (149/149), done.
error: 3839 bytes of body are still expected4 MiB | 368.00 KiB/s
fetch-pack: unexpected disconnect while reading sideband packet
fatal: early EOF
fatal: fetch-pack: invalid index-pack output

[Kevin Buzzard]

If you're on windows, switch off your antivirus and try again?