lake new ... math gives `Invalid lake configuration`

Stream: lean4

[Bolton Bailey]

This is what I get after running lake new boltonworkspace math and opening Boltonworkspace/Basic.lean.

`/Users/boltonbailey/.elan/toolchains/leanprover--lean4---v4.16.0-rc2/bin/lake setup-file /Users/boltonbailey/Documents/MyDocuments/Professional/numina-all-files/contribution/boltonworkspace/Boltonworkspace/Basic.lean Init --no-build --no-cache` failed:

stderr:
info: boltonworkspace: no previous manifest, creating one from scratch
trace: boltonworkspace: updating 'mathlib' with {}
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
trace: .> git clone https://github.com/leanprover-community/mathlib4.git ././.lake/packages/mathlib
trace: stderr:
Cloning into '././.lake/packages/mathlib'...
error: RPC failed; HTTP 400 curl 22 The requested URL returned error: 400
fatal: expected 'packfile'
error: external command 'git' exited with code 128
Invalid Lake configuration.  Please restart the server after fixing the Lake configuration file.

Why is it telling me I have an invalid Lake configuration file? I Haven't touched it at all, it's exactly what the lake new command gave:

import Lake
open Lake DSL

package «boltonworkspace» where
  -- Settings applied to both builds and interactive editing
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
  ]
  -- add any additional package configuration options here

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

@[default_target]
lean_lib «Boltonworkspace» where
  -- add any library configuration options here

[Kevin Buzzard]

Is it a network error? Can you connect to GitHub?

[Bolton Bailey]

I guess it probably has something to do with the network, I've seen the git part of the error message when using git clone on a non-mathlib related project. Nevertheless, I am still concerned about why it would be saying the lakefile is bad when its the network that's the issue.

[Bolton Bailey]

I also asked this here, but I'll ask again - there a way to get lake to use ssh rather than http?

[Damiano Testa]

I do not know about the ssh vs http answer, but maybe this conversation can be useful?

[Damiano Testa]

(My hunch based on what I understood from that conversation is that lake prefers it if you use http rather than ssh, but I am not sure.)

[Bolton Bailey]

Indeed, it looks interesting, but I don't seem to have this insteadOf in my gitconfig

credential.helper=osxkeychain
init.defaultbranch=main
user.name=Bolton Bailey
user.email=bolton.bailey@gmail.com
gpg.program=/opt/homebrew/bin/gpg
filter.lfs.clean=git-lfs clean -- %f
filter.lfs.smudge=git-lfs smudge -- %f
filter.lfs.process=git-lfs filter-process
filter.lfs.required=true
init.templatedir=/Users/boltonbailey/.git-templates
http.version=HTTP/1.1
http.postbuffer=524288000

[Bolton Bailey]

Ok after trying several other things switching to mobile internet worked. Not sure what the problem is with my home internet and the internet at the cafe I was at earlier, maybe both are just very slow? Even that doesn't really make sense as I get >100MB/sec in my speed tests.

[Bolton Bailey]

Hmm, I am now trying it again in order to be able to download the carleson project and it is again failing, even over mobile internet.

Is it possible I have just tried to clone mathlib too many times and github is throttling me?

[Alok Singh]

I'm having similar issue, wondering about throttling too

[Nick Ward]

This seems to go against the consensus opinion here, but if you have ssh configured you could try forcing lake to use it by first running:

git config --global url."git@github.com:".insteadOf "https://github.com/"

[Nick Ward]

You can later undo this change to your .gitconfig by deleting the added section or by running:

git config --global --remove-section url."git@github.com:"

[Mauricio Collares]

Bolton Bailey said:

I guess it probably has something to do with the network, I've seen the git part of the error message when using git clone on a non-mathlib related project. Nevertheless, I am still concerned about why it would be saying the lakefile is bad when its the network that's the issue.

Wild guess: I think this might just be a confusing message. To compile your lakefile.lean into lakefile.olean, lake needs to look at mathlib's lakefile.lean due to the require. Then you don't get a lakefile.olean, which is probably the definition of an invalid configuration. Again, just a guess.

[Bolton Bailey]

Yes, here is the line that generates this error. Seems like it simply writes this error message no matter what kind of error is experienced, even if it does not have to do with the lakefile itself being the problem.

[Kim Morrison]

@Mac Malone, could this error message be improved?

[Mac Malone]

@Kim Morrison Sure! Since the real error is already printed, perhaps the following would good?

Failed to configure the Lake workspace. Please restart the server after fixing the error above.

[Bolton Bailey]

This error message looks fine to me.

[Bolton Bailey]

Nick Ward said:

This seems to go against the consensus opinion here, but if you have ssh configured you could try forcing lake to use it by first running:

git config --global url."git@github.com:".insteadOf "https://github.com/"

Thanks for the advice. Doing this, I do not get immediate errors, but unfortunately it does not seem to have sped up the cloning process and I am waiting at least several minutes with the "starting Lean language client message".

[Bolton Bailey]

Mac Malone said:

Kim Morrison Sure! Since the real error is already printed, perhaps the following would good?

Failed to configure the Lake workspace. Please restart the server after fixing the error above.

FYI I made lean4#6827 to track this.

[Bolton Bailey]

And I made a PR lean4#6829 in case we feel this is uncontroversial and can be simply changed quickly.

[Bolton Bailey]

Just got a very similar error message:

stderr:
info: batteries: URL has changed; deleting '././.lake/packages/batteries' and cloning again
info: batteries: cloning https://github.com/leanprover-community/batteries
error: external command 'git' exited with code 128

This is confusing and super frustrating! I was working on this branch just fine yesterday, and I don't think I've checked out any other branches since then - has batteries moved since then?