Ran proofwidgets:extraDep

Stream: general

[Damiano Testa]

Since today, when I run lake exe cache get, I see the following warning:

$ lake exe cache get
⚠ [9/21] Ran proofwidgets:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)

Am I the only one seeing this?

[Damiano Testa]

Running with -v, I see this:

$ lake exe -v cache get
✖ [4/18] (Optional) Fetching proofwidgets:optRelease
trace: .> curl -s -S -f -o ././.lake/packages/proofwidgets/.lake/ProofWidgets4.tar.gz -L ssh://git@github.com/leanprover-community/ProofWidgets4/releases/download/v0.0.42/ProofWidgets4.tar.gz
trace: stderr:
curl: (1) Protocol "ssh" not supported or disabled in libcurl
error: external command 'curl' exited with code 1
⚠ [5/18] Ran proofwidgets:extraDep
warning: building from source; failed to fetch GitHub release (see 'proofwidgets:optRelease' for details)
ℹ [10/18] Replayed Cache.IO
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/damiano/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -Dweak.linter.docPrime=true -Dweak.linter.hashCommand=true -Dweak.linter.oldObtain=true -Dweak.linter.refine=true -Dweak.linter.style.cdot=true -Dweak.linter.style.dollarSyntax=true -Dweak.linter.style.lambdaSyntax=true -Dweak.linter.style.longLine=true -Dweak.linter.style.longFile=1500 -Dweak.linter.style.missingEnd=true -Dweak.linter.style.setOption=true -Dweak.aesop.warn.applyIff=false ././././Cache/IO.lean -R ./././. -o ././.lake/build/lib/Cache/IO.olean -i ././.lake/build/lib/Cache/IO.ilean -c ././.lake/build/ir/Cache/IO.c --json
ℹ [11/18] Replayed Cache.Hashing
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/damiano/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -Dweak.linter.docPrime=true -Dweak.linter.hashCommand=true -Dweak.linter.oldObtain=true -Dweak.linter.refine=true -Dweak.linter.style.cdot=true -Dweak.linter.style.dollarSyntax=true -Dweak.linter.style.lambdaSyntax=true -Dweak.linter.style.longLine=true -Dweak.linter.style.longFile=1500 -Dweak.linter.style.missingEnd=true -Dweak.linter.style.setOption=true -Dweak.aesop.warn.applyIff=false ././././Cache/Hashing.lean -R ./././. -o ././.lake/build/lib/Cache/Hashing.olean -i ././.lake/build/lib/Cache/Hashing.ilean -c ././.lake/build/ir/Cache/Hashing.c --json
ℹ [12/18] Replayed Cache.Requests
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/damiano/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -Dweak.linter.docPrime=true -Dweak.linter.hashCommand=true -Dweak.linter.oldObtain=true -Dweak.linter.refine=true -Dweak.linter.style.cdot=true -Dweak.linter.style.dollarSyntax=true -Dweak.linter.style.lambdaSyntax=true -Dweak.linter.style.longLine=true -Dweak.linter.style.longFile=1500 -Dweak.linter.style.missingEnd=true -Dweak.linter.style.setOption=true -Dweak.aesop.warn.applyIff=false ././././Cache/Requests.lean -R ./././. -o ././.lake/build/lib/Cache/Requests.olean -i ././.lake/build/lib/Cache/Requests.ilean -c ././.lake/build/ir/Cache/Requests.c --json
ℹ [13/18] Replayed Cache.Main
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/damiano/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -Dweak.linter.docPrime=true -Dweak.linter.hashCommand=true -Dweak.linter.oldObtain=true -Dweak.linter.refine=true -Dweak.linter.style.cdot=true -Dweak.linter.style.dollarSyntax=true -Dweak.linter.style.lambdaSyntax=true -Dweak.linter.style.longLine=true -Dweak.linter.style.longFile=1500 -Dweak.linter.style.missingEnd=true -Dweak.linter.style.setOption=true -Dweak.aesop.warn.applyIff=false ././././Cache/Main.lean -R ./././. -o ././.lake/build/lib/Cache/Main.olean -i ././.lake/build/lib/Cache/Main.ilean -c ././.lake/build/ir/Cache/Main.c --json
ℹ [14/18] Replayed Cache.Main:c.o (with exports)
trace: .> /home/damiano/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/leanc -c -o ././.lake/build/ir/Cache/Main.c.o.export ././.lake/build/ir/Cache/Main.c -O3 -DNDEBUG -DLEAN_EXPORTING
ℹ [15/18] Replayed Cache.IO:c.o (with exports)
trace: .> /home/damiano/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/leanc -c -o ././.lake/build/ir/Cache/IO.c.o.export ././.lake/build/ir/Cache/IO.c -O3 -DNDEBUG -DLEAN_EXPORTING
ℹ [16/18] Replayed Cache.Hashing:c.o (with exports)
trace: .> /home/damiano/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/leanc -c -o ././.lake/build/ir/Cache/Hashing.c.o.export ././.lake/build/ir/Cache/Hashing.c -O3 -DNDEBUG -DLEAN_EXPORTING
ℹ [17/18] Replayed Cache.Requests:c.o (with exports)
trace: .> /home/damiano/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/leanc -c -o ././.lake/build/ir/Cache/Requests.c.o.export ././.lake/build/ir/Cache/Requests.c -O3 -DNDEBUG -DLEAN_EXPORTING
ℹ [18/18] Replayed cache
trace: .> /home/damiano/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/leanc -o ././.lake/build/bin/cache ././.lake/build/ir/Cache/Main.c.o.export ././.lake/build/ir/Cache/IO.c.o.export ././.lake/build/ir/Cache/Hashing.c.o.export ././.lake/build/ir/Cache/Requests.c.o.export
Attempting to download 4834 file(s)