lake exe cache get takes 1 minute to do anything

Stream: mathlib4

[Kevin Buzzard]

I'm consistently finding on my laptop that if I clone a students' project (which will depend on mathlib) and then type lake exe cache get that it will spend about 30 seconds to a minute not doing anything at all, before either working fine, or occasionally printing

$ lake exe cache get
error: > git fetch origin    # in directory ./.lake/packages/mathlib
error: stderr:
fatal: the remote end hung up unexpectedly
fatal: early EOF
fatal: index-pack failed
error: external command `git` exited with code 128

Any ideas what I've done wrong?

[Ruben Van de Velde]

It sounds like a networking issue

[Matthew Ballard]

https://www.githubstatus.com is green

[Eric Wieser]

The cache isn't hosted on github

[Henrik Böving]

But it is not fetching the cache here is it? It's clearly saying that it is running git fetch origin in mathlib so it is talking to Github.

[Henrik Böving]

Hm, the internet seems to attribute this to configurations of the network that the computer is connect to, not allowing for chunks of the size that git wishes to transmit and recommends playing with a bunch of options: https://github.com/orgs/community/discussions/39210

This seems highly heuristical to me though, it would be nice to get more debugging information on this type of thing

[Kevin Buzzard]

So it's the beginning of MSc projects here and in the last week I've cloned three projects and I had this issue every time -- a very very long pause after lake exe cache get. How do I get more debugging information?

[Eric Wieser]

Could this be an issue with university wifi in the room you're in?

[Eric Wieser]

I had some connections in my undergrad that blocked SSH, possibly by accident

[Matthew Ballard]

What happens with ssh -T git@github.com?

[Henrik Böving]

SSH cannot be what's going on? Mathlib is pulled in as an http git dependency so git will clone it over HTTP.

[Henrik Böving]

Kevin Buzzard said:

So it's the beginning of MSc projects here and in the last week I've cloned three projects and I had this issue every time -- a very very long pause after lake exe cache get. How do I get more debugging information?

If you go into .lake/packages/mathlib and run

GIT_CURL_VERBOSE=1 GIT_TRACE=1 git fetch origin

what happens?

[Kim Morrison]

Might be worth running time git fetch origin, even, so we can compare. (The verbose messages include timestamps!)

[Kim Morrison]

e.g. I get

% time GIT_CURL_VERBOSE=1 GIT_TRACE=1 git fetch origin
07:50:25.726537 git.c:465               trace: built-in: git fetch origin
07:50:25.738455 run-command.c:657       trace: run_command: GIT_DIR=.git git remote-https origin https://github.com/leanprover-community/mathlib4.git
07:50:25.745683 git.c:750               trace: exec: git-remote-https origin https://github.com/leanprover-community/mathlib4.git
07:50:25.746249 run-command.c:657       trace: run_command: git-remote-https origin https://github.com/leanprover-community/mathlib4.git
07:50:25.757796 http.c:843              == Info: Couldn't find host github.com in the .netrc file; using defaults
07:50:25.760552 http.c:843              == Info: Host github.com:443 was resolved.
07:50:25.760563 http.c:843              == Info: IPv6: (none)
07:50:25.760565 http.c:843              == Info: IPv4: 20.248.137.48
07:50:25.760601 http.c:843              == Info:   Trying 20.248.137.48:443...
07:50:25.781725 http.c:843              == Info: Connected to github.com (20.248.137.48) port 443
07:50:25.781796 http.c:843              == Info: ALPN: curl offers h2,http/1.1
07:50:25.782045 http.c:843              == Info: (304) (OUT), TLS handshake, Client hello (1):
07:50:25.787007 http.c:843              == Info:  CAfile: /etc/ssl/cert.pem
07:50:25.787014 http.c:843              == Info:  CApath: none
07:50:25.802759 http.c:843              == Info: (304) (IN), TLS handshake, Server hello (2):
07:50:25.802999 http.c:843              == Info: (304) (IN), TLS handshake, Unknown (8):
07:50:25.803039 http.c:843              == Info: (304) (IN), TLS handshake, Certificate (11):
07:50:25.805403 http.c:843              == Info: (304) (IN), TLS handshake, CERT verify (15):
07:50:25.805688 http.c:843              == Info: (304) (IN), TLS handshake, Finished (20):
07:50:25.805788 http.c:843              == Info: (304) (OUT), TLS handshake, Finished (20):
07:50:25.805805 http.c:843              == Info: SSL connection using TLSv1.3 / AEAD-CHACHA20-POLY1305-SHA256 / [blank] / UNDEF
07:50:25.805810 http.c:843              == Info: ALPN: server accepted h2
07:50:25.805816 http.c:843              == Info: Server certificate:
07:50:25.805824 http.c:843              == Info:  subject: CN=github.com
07:50:25.805831 http.c:843              == Info:  start date: Mar  7 00:00:00 2024 GMT
07:50:25.805835 http.c:843              == Info:  expire date: Mar  7 23:59:59 2025 GMT
07:50:25.805844 http.c:843              == Info:  subjectAltName: host "github.com" matched cert's "github.com"
07:50:25.805858 http.c:843              == Info:  issuer: C=GB; ST=Greater Manchester; L=Salford; O=Sectigo Limited; CN=Sectigo ECC Domain Validation Secure Server CA
07:50:25.805863 http.c:843              == Info:  SSL certificate verify ok.

[Kim Morrison]

07:50:25.805934 http.c:843              == Info: using HTTP/2
07:50:25.805976 http.c:843              == Info: [HTTP/2] [1] OPENED stream for https://github.com/leanprover-community/mathlib4.git/info/refs?service=git-upload-pack
07:50:25.805981 http.c:843              == Info: [HTTP/2] [1] [:method: GET]
07:50:25.805984 http.c:843              == Info: [HTTP/2] [1] [:scheme: https]
07:50:25.805986 http.c:843              == Info: [HTTP/2] [1] [:authority: github.com]
07:50:25.805990 http.c:843              == Info: [HTTP/2] [1] [:path: /leanprover-community/mathlib4.git/info/refs?service=git-upload-pack]
07:50:25.805993 http.c:843              == Info: [HTTP/2] [1] [user-agent: git/2.45.2]
07:50:25.805996 http.c:843              == Info: [HTTP/2] [1] [accept: */*]
07:50:25.805998 http.c:843              == Info: [HTTP/2] [1] [accept-encoding: deflate, gzip]
07:50:25.806001 http.c:843              == Info: [HTTP/2] [1] [accept-language: en-US, *;q=0.9]
07:50:25.806004 http.c:843              == Info: [HTTP/2] [1] [pragma: no-cache]
07:50:25.806007 http.c:843              == Info: [HTTP/2] [1] [git-protocol: version=2]
07:50:25.806044 http.c:790              => Send header, 0000000246 bytes (0x000000f6)
07:50:25.806059 http.c:802              => Send header: GET /leanprover-community/mathlib4.git/info/refs?service=git-upload-pack HTTP/2
07:50:25.806062 http.c:802              => Send header: Host: github.com
07:50:25.806064 http.c:802              => Send header: User-Agent: git/2.45.2
07:50:25.806067 http.c:802              => Send header: Accept: */*
07:50:25.806069 http.c:802              => Send header: Accept-Encoding: deflate, gzip
07:50:25.806072 http.c:802              => Send header: Accept-Language: en-US, *;q=0.9
07:50:25.806074 http.c:802              => Send header: Pragma: no-cache
07:50:25.806077 http.c:802              => Send header: Git-Protocol: version=2
07:50:25.806079 http.c:802              => Send header:
07:50:26.117847 http.c:790              <= Recv header, 0000000013 bytes (0x0000000d)
07:50:26.117918 http.c:802              <= Recv header: HTTP/2 200
07:50:26.117937 http.c:790              <= Recv header, 0000000026 bytes (0x0000001a)
07:50:26.117944 http.c:802              <= Recv header: server: GitHub-Babel/3.0
07:50:26.117960 http.c:790              <= Recv header, 0000000059 bytes (0x0000003b)
07:50:26.117967 http.c:802              <= Recv header: content-type: application/x-git-upload-pack-advertisement
07:50:26.117976 http.c:790              <= Recv header, 0000000054 bytes (0x00000036)
07:50:26.117990 http.c:802              <= Recv header: content-security-policy: default-src 'none'; sandbox
07:50:26.117998 http.c:790              <= Recv header, 0000000040 bytes (0x00000028)
07:50:26.118005 http.c:802              <= Recv header: expires: Fri, 01 Jan 1980 00:00:00 GMT
07:50:26.118012 http.c:790              <= Recv header, 0000000018 bytes (0x00000012)
07:50:26.118017 http.c:802              <= Recv header: pragma: no-cache
07:50:26.118024 http.c:790              <= Recv header, 0000000053 bytes (0x00000035)
07:50:26.118030 http.c:802              <= Recv header: cache-control: no-cache, max-age=0, must-revalidate
07:50:26.118037 http.c:790              <= Recv header, 0000000023 bytes (0x00000017)
07:50:26.118175 http.c:802              <= Recv header: vary: Accept-Encoding
07:50:26.118252 http.c:790              <= Recv header, 0000000037 bytes (0x00000025)
07:50:26.118282 http.c:802              <= Recv header: date: Mon, 08 Jul 2024 21:50:25 GMT
07:50:26.118292 http.c:790              <= Recv header, 0000000023 bytes (0x00000017)
07:50:26.118298 http.c:802              <= Recv header: x-frame-options: DENY
07:50:26.118306 http.c:790              <= Recv header, 0000000059 bytes (0x0000003b)
07:50:26.118312 http.c:802              <= Recv header: x-github-request-id: E2FE:1FC500:160101C:18FB93F:668C5F21
07:50:26.118333 http.c:790              <= Recv header, 0000000002 bytes (0x00000002)
07:50:26.118340 http.c:802              <= Recv header:
07:50:26.118413 http.c:843              == Info: Connection #0 to host github.com left intact
07:50:26.119067 http.c:843              == Info: Couldn't find host github.com in the .netrc file; using defaults
07:50:26.119104 http.c:843              == Info: Found bundle for host: 0x600001810a50 [can multiplex]
07:50:26.119122 http.c:843              == Info: Re-using existing connection with host github.com
07:50:26.119237 http.c:843              == Info: [HTTP/2] [3] OPENED stream for https://github.com/leanprover-community/mathlib4.git/git-upload-pack
07:50:26.119252 http.c:843              == Info: [HTTP/2] [3] [:method: POST]
07:50:26.119260 http.c:843              == Info: [HTTP/2] [3] [:scheme: https]
07:50:26.119267 http.c:843              == Info: [HTTP/2] [3] [:authority: github.com]
07:50:26.119275 http.c:843              == Info: [HTTP/2] [3] [:path: /leanprover-community/mathlib4.git/git-upload-pack]
07:50:26.119283 http.c:843              == Info: [HTTP/2] [3] [user-agent: git/2.45.2]
07:50:26.119289 http.c:843              == Info: [HTTP/2] [3] [accept-encoding: deflate, gzip]
07:50:26.119297 http.c:843              == Info: [HTTP/2] [3] [content-type: application/x-git-upload-pack-request]
07:50:26.119305 http.c:843              == Info: [HTTP/2] [3] [accept: application/x-git-upload-pack-result]
07:50:26.119312 http.c:843              == Info: [HTTP/2] [3] [accept-language: en-US, *;q=0.9]
07:50:26.119318 http.c:843              == Info: [HTTP/2] [3] [git-protocol: version=2]
07:50:26.119325 http.c:843              == Info: [HTTP/2] [3] [content-length: 155]
07:50:26.119515 http.c:790              => Send header, 0000000318 bytes (0x0000013e)
07:50:26.119551 http.c:802              => Send header: POST /leanprover-community/mathlib4.git/git-upload-pack HTTP/2
07:50:26.119559 http.c:802              => Send header: Host: github.com
07:50:26.119564 http.c:802              => Send header: User-Agent: git/2.45.2
07:50:26.119570 http.c:802              => Send header: Accept-Encoding: deflate, gzip
07:50:26.119576 http.c:802              => Send header: Content-Type: application/x-git-upload-pack-request
07:50:26.119582 http.c:802              => Send header: Accept: application/x-git-upload-pack-result
07:50:26.119588 http.c:802              => Send header: Accept-Language: en-US, *;q=0.9
07:50:26.119594 http.c:802              => Send header: Git-Protocol: version=2
07:50:26.119599 http.c:802              => Send header: Content-Length: 155
07:50:26.119605 http.c:802              => Send header:
07:50:26.422346 http.c:790              <= Recv header, 0000000013 bytes (0x0000000d)
07:50:26.422427 http.c:802              <= Recv header: HTTP/2 200
07:50:26.422445 http.c:790              <= Recv header, 0000000026 bytes (0x0000001a)
07:50:26.422452 http.c:802              <= Recv header: server: GitHub-Babel/3.0
07:50:26.422462 http.c:790              <= Recv header, 0000000052 bytes (0x00000034)
07:50:26.422479 http.c:802              <= Recv header: content-type: application/x-git-upload-pack-result
07:50:26.422488 http.c:790              <= Recv header, 0000000054 bytes (0x00000036)
07:50:26.422494 http.c:802              <= Recv header: content-security-policy: default-src 'none'; sandbox
07:50:26.422502 http.c:790              <= Recv header, 0000000040 bytes (0x00000028)
07:50:26.422516 http.c:802              <= Recv header: expires: Fri, 01 Jan 1980 00:00:00 GMT
07:50:26.422523 http.c:790              <= Recv header, 0000000018 bytes (0x00000012)
07:50:26.422536 http.c:802              <= Recv header: pragma: no-cache
07:50:26.422543 http.c:790              <= Recv header, 0000000053 bytes (0x00000035)
07:50:26.422549 http.c:802              <= Recv header: cache-control: no-cache, max-age=0, must-revalidate
07:50:26.422777 http.c:790              <= Recv header, 0000000023 bytes (0x00000017)
07:50:26.422789 http.c:802              <= Recv header: vary: Accept-Encoding
07:50:26.422796 http.c:790              <= Recv header, 0000000037 bytes (0x00000025)
07:50:26.422802 http.c:802              <= Recv header: date: Mon, 08 Jul 2024 21:50:26 GMT
07:50:26.422809 http.c:790              <= Recv header, 0000000023 bytes (0x00000017)
07:50:26.422815 http.c:802              <= Recv header: x-frame-options: DENY
07:50:26.422822 http.c:790              <= Recv header, 0000000059 bytes (0x0000003b)
07:50:26.422829 http.c:802              <= Recv header: x-github-request-id: E2FE:1FC500:1601033:18FB96D:668C5F22
07:50:26.422839 http.c:790              <= Recv header, 0000000002 bytes (0x00000002)
07:50:26.422845 http.c:802              <= Recv header:
07:50:26.505172 http.c:843              == Info: Connection #0 to host github.com left intact
07:50:26.582938 run-command.c:657       trace: run_command: git rev-list --objects --stdin --not --exclude-hidden=fetch --all --quiet --alternate-refs
From https://github.com/leanprover-community/mathlib4
 * [new branch]            AffineLocalToPretop -> origin/AffineLocalToPretop
07:50:26.659410 run-command.c:1522      run_processes_parallel: preparing to run up to 1 tasks
07:50:26.659452 run-command.c:1549      run_processes_parallel: done
07:50:26.659458 run-command.c:657       trace: run_command: git maintenance run --auto --no-quiet
07:50:26.662804 git.c:465               trace: built-in: git maintenance run --auto --no-quiet
GIT_CURL_VERBOSE=1 GIT_TRACE=1 git fetch origin  0.10s user 0.13s system 23% cpu 0.952 total

[Kim Morrison]

(from Australia)

[Kim Morrison]

Note that is way better than I get in Mathlib itself:

% time GIT_CURL_VERBOSE=1 GIT_TRACE=1 git fetch origin
07:51:56.696545 git.c:465               trace: built-in: git fetch origin
07:51:56.707863 run-command.c:657       trace: run_command: unset GIT_DIR GIT_PREFIX; GIT_PROTOCOL=version=2 ssh -o SendEnv=GIT_PROTOCOL git@github.com 'git-upload-pack '\''leanprover-community/mathlib4.git'\'''
07:52:01.547192 run-command.c:657       trace: run_command: git rev-list --objects --stdin --not --exclude-hidden=fetch --all --quiet --alternate-refs
07:52:01.967568 run-command.c:1522      run_processes_parallel: preparing to run up to 1 tasks
07:52:01.967909 run-command.c:1549      run_processes_parallel: done
07:52:01.967940 run-command.c:657       trace: run_command: git maintenance run --auto --no-quiet
07:52:01.984328 git.c:465               trace: built-in: git maintenance run --auto --no-quiet
GIT_CURL_VERBOSE=1 GIT_TRACE=1 git fetch origin  0.29s user 0.16s system 8% cpu 5.312 total

[Kevin Buzzard]

Thanks -- I'll try again tomorrow (this was reliably happening at work, the first time I cloned a project).

[Mario Carneiro]

to be clear, this is not about cache itself, the network request is to download mathlib so that it can start compiling cache and then run it

[Kevin Buzzard]

huh, I'm trying it again (same repo, same computer, same internet connection) and the problem has gone away. If it comes back I'll report on the output of those commands.

[Kevin Buzzard]

Ooh, the problem is back.

buzzard@buster:~/lean-projects/Goedel_HF_Lean$ lake build
^C
buzzard@buster:~/lean-projects/Goedel_HF_Lean$ lake exe cache get
^C
buzzard@buster:~/lean-projects/Goedel_HF_Lean$ cd .lake/packages/mathlib/
buzzard@buster:~/lean-projects/Goedel_HF_Lean/.lake/packages/mathlib$ GIT_CURL_VERBOSE=1 GIT_TRACE=1 git fetch origin
11:38:52.449119 git.c:439               trace: built-in: git fetch origin
11:38:52.451192 run-command.c:663       trace: run_command: GIT_DIR=.git git-remote-https origin https://github.com/leanprover-community/mathlib4.git
* Couldn't find host github.com in the .netrc file; using defaults
*   Trying 20.26.156.215:443...
* TCP_NODELAY set
* Connected to github.com (20.26.156.215) port 443 (#0)
* found 415 certificates in /etc/ssl/certs
* ALPN, offering h2
* ALPN, offering http/1.1
* SSL connection using TLS1.3 / ECDHE_RSA_AES_128_GCM_SHA256
*    server certificate verification OK
*    server certificate status verification SKIPPED
*    common name: github.com (matched)
*    server certificate expiration date OK
*    server certificate activation date OK
*    certificate public key: EC/ECDSA
*    certificate version: #3
*    subject: CN=github.com
*    start date: Thu, 07 Mar 2024 00:00:00 GMT
*    expire date: Fri, 07 Mar 2025 23:59:59 GMT
*    issuer: C=GB,ST=Greater Manchester,L=Salford,O=Sectigo Limited,CN=Sectigo ECC Domain Validation Secure Server CA
* ALPN, server accepted to use h2
* Using HTTP2, server supports multi-use
* Connection state changed (HTTP/2 confirmed)
* Copying HTTP/2 data in stream buffer to connection buffer after upgrade: len=0
* Using Stream ID: 1 (easy handle 0x55c5da42dab0)
> GET /leanprover-community/mathlib4.git/info/refs?service=git-upload-pack HTTP/2
Host: github.com
user-agent: git/2.25.1
accept: */*
accept-encoding: deflate, gzip, br
accept-language: en-GB, en;q=0.9, *;q=0.8
pragma: no-cache

* Connection state changed (MAX_CONCURRENT_STREAMS == 100)!
< HTTP/2 200
< server: GitHub-Babel/3.0
< content-type: application/x-git-upload-pack-advertisement
< content-security-policy: default-src 'none'; sandbox
< expires: Fri, 01 Jan 1980 00:00:00 GMT
< pragma: no-cache
< cache-control: no-cache, max-age=0, must-revalidate
< vary: Accept-Encoding
< date: Tue, 16 Jul 2024 10:38:52 GMT
< x-frame-options: DENY
< x-github-request-id: 8EDE:1C50D9:1F44320:235E190:66964DBC
<
* Connection #0 to host github.com left intact
11:38:53.180601 run-command.c:663       trace: run_command: git rev-list --objects --stdin --not --all --quiet --alternate-refs
11:38:53.209072 run-command.c:663       trace: run_command: git rev-list --objects --stdin --not --all --quiet --alternate-refs
11:38:53.209962 git.c:439               trace: built-in: git rev-list --objects --stdin --not --all --quiet --alternate-refs
11:38:53.260561 run-command.c:1623      run_processes_parallel: preparing to run up to 1 tasks
11:38:53.260601 run-command.c:1655      run_processes_parallel: done
11:38:53.260930 run-command.c:663       trace: run_command: git gc --auto
11:38:53.261972 git.c:439               trace: built-in: git gc --auto
buzzard@buster:~/lean-projects/Goedel_HF_Lean/.lake/packages/mathlib$

I'm confident that both lake build and lake exe cache get will work, it's just that I have to wait for a while before they do anything. I'm working with a student right now so I'm going to have to actually run them.

OK so in the root directory of the project, after rm -rf .lake, lake exe cache get does nothing for 1 minute and 30 seconds, and then works as normal. After that, everything works as normal (e.g. lake exe cache get is immediate).

If I mv .lake .lake2 then I'm back to 1 minute + of nothing after lake exe cache get.

[Damiano Testa]

Every time that lake exe cache get or lake build give me problems, I usually fix them with rm -i -rf .lake/build/lib/Mathlib/* followed by lake exe cache get. That is, you do not need to remove all of the cache, just a big chunk of it!

[Damiano Testa]

I have never had the delay issue though, so maybe this is not a solution to your problem... :shrug:

[Kim Morrison]

Pinging @Mac Malone.

I wonder if your polluted .lake directory is transferable? Do you want to zip it up and post it here (along with the git SHA for the Mathlib commit you're working at)?

[Kim Morrison]

It would be great to have a repro.

[Mac Malone]

This seems like a firewall / antivirus / real-time scanning problem to me. That is, something on the system is making the network request and/or file system operations slow on the initial pass (e.g., to do some virus checking) and then once it is happy it treats those files as safe.

[Kevin Buzzard]

This is on an Ubuntu laptop and unfortunately I have no idea about networking. But it doesn't look to me.like a poisoned lake file -- the delay is precisely when .lake is not found.