lake build in China

Stream: lean4

[Kevin Buzzard]

buzzard@buster:~/lean-projects/mathlib$ lake build
thread 'main' panicked at src/elan-utils/src/utils.rs:472:32:
called `Result::unwrap()` on an `Err` value: Error { description: "Timeout was reached", code: 28, extra: Some("Failed to connect to github.com port 443 after 129334 ms: Couldn't connect to server") }
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

I have stale oleans for mathlib and figured that if I couldn't lake exe cache get in China (which I can't) then I'd just build mathlib from scratch. I was then surprised to find that I couldn't do that either :-( (the error is the same for both lake build and lake exe cache get). Is there a workaround for this?

[Ruben Van de Velde]

I'm guessing it's trying to fetch the lean version you need?

[Kevin Buzzard]

buzzard@buster:~/lean-projects/mathlib$ elan show
thread 'main' panicked at src/elan-utils/src/utils.rs:472:32:
called `Result::unwrap()` on an `Err` value: Error { description: "Timeout was reached", code: 28, extra: Some("Failed to connect to github.com port 443 after 129875 ms: Couldn't connect to server") }
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
buzzard@buster:~/lean-projects/mathlib$

:-/
Are the FRO interested in making it easier to use Lean in China? Or are we just working on the assumption that everyone has a VPN?

buzzard@buster:~/lean-projects/mathlib$ git checkout 755d1ebf513449da930670946a2a15c06c31b042
HEAD is now at 755d1ebf51 chore(ModelTheory): Add @[simps] to functions creating maps from `HomClass` instances (#16193)
buzzard@buster:~/lean-projects/mathlib$ more lean-toolchain
leanprover/lean4:v4.11.0-rc2
buzzard@buster:~/lean-projects/mathlib$ ls ~/.elan/toolchains/ | grep 11
leanprover--lean4---v4.11.0-rc1
leanprover--lean4---v4.11.0-rc2
buzzard@buster:~/lean-projects/mathlib$ lake build
trace: ././.lake/packages/Qq> git fetch --tags --force origin
trace: stderr:
fatal: unable to access 'https://github.com/leanprover-community/quote4/': GnuTLS recv error (-110): The TLS connection was non-properly terminated.
error: external command 'git' exited with code 128
buzzard@buster:~/lean-projects/mathlib$

Apparently it's not just about the version of lean :-)

[Matthew Ballard]

They are blocking github.

[Kevin Buzzard]

Right, but I don't want to use github, I just want to build mathlib locally on my machine. Is that too much to ask? I'll keep trying commits.

[Matthew Ballard]

If you don't already have the toolchain on your machine, I am not sure how you get it there with this.

[Kevin Buzzard]

I do have the toolchain on my machine for that commit. The last bash dump shows that it's not as simple as that. But I've got it working!

buzzard@buster:~/lean-projects/mathlib$ git checkout 9427959b0501e0da0363adbf64c385fbe730c715
Previous HEAD position was b03feaaa78 feat(ContinuousFunctionalCalculus): show that the non-unital CFC commutes with integration (#16255)
HEAD is now at 9427959b05 feat: Conditioning an event by itself (#16249)
buzzard@buster:~/lean-projects/mathlib$ lake build
⣯ [1068/5015] Running Mathlib.Data.Set.Function (+ 7 more)

Of course I just needed to find a commit where I had the toolchain for all the dependencies, not just lean. Oh -- or maybe "toolchain" means "all the right versions of all the dependencies"? In which case you're right.

[Henrik Böving]

Are the FRO interested in making it easier to use Lean in China?

I don't know about the FRO's plans on this but from the top of my head one issue in doing this would be that either a FRO member or a sufficiently willing guinea pig would need to be in China in order to figure out if stuff is working.

[Kevin Buzzard]

Kids here seem to be passing around USB sticks with oleans!

[Yuyang Zhao]

Related: there is a tool to download lean and mathlib caches using SJTU mirror. See https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/Release.20of.20.60glean.60.3A.20all-in-one.20.20tool.20for.20Lean.20mirror
upd: Oh, no, I think it can't download the caches yet.

[A.]

(deleted)