Starting: Debian, VSCode , Lean4 , tutorial, Paperproof

Stream: new members

[M R]

Hi, where can ask questions getting started with Lean4 on Debian, VSCode , tutorial, Paperproof ?

I got everything installed and in VSCode I can see tiny standalone theorems in infoview and Paperproof, but when I try the mathematics_in_lean tutorial project, I get

1. many minutes of build times ( up to 8 CPUS @ 90+% and >1GB RAM on each task (maybe partly shared?)
   when I view MIL's Common.lean:

Common.lean:1:0
info: [1438/1676] Building Mathlib.Algebra.Polynomial.BigOperators

2.
Errors loading files. (I don't know if this is a funny way of saying "file didn't finish building yet" per #1, or a different problem.)

Common.lean:1:0
`$HOME/.elan/toolchains/stable/bin/lake print-paths Init Paperproof Mathlib.Data.Nat.Basic Mathlib.Data.Nat.Parity MIL.Common` failed:

stderr:
error: no such file or directory (error code: 2)
  file: ./././MIL/Common.leann

I started this comment when I thought the build was stalled, but now I'm at info: [1630/1676] Building Mathlib.FieldTheory.Finite.Basic so maybe if I keep waiting longer I'll be fine?

I'm not sure what actions in VSCode cause the system to throw away build work so far and start over when I re-visit a .lean file.

[Ruben Van de Velde]

For 1, you missed lake exe cache get

[M R]

Oh, thank you! I did notice that command on a doc page today, but but I guess I thought it wasn't necessary yet in my context.

Do I need to do all the lake commands in the same directory, or does the tool share packages/caches across my entire logged in user?

[M R]

lake exe cache get downloaded a lot and completed:

lean $
lake exe cache get
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [4/9] Compiling Cache.Requests
info: [4/9] Building Cache.Main
info: [5/9] Compiling Cache.Main
info: [9/9] Linking cache
leantar is too old; downloading more recent version
Attempting to download 3796 file(s)
Downloaded: 3796 file(s) [attempted 3796/3796 = 100%] (100% success)
Decompressing 3796 file(s)
unpacked in 38609 ms

and re-running in the same dir appears to maintain the existing cache (good):

lake exe cache get
No files to download
Decompressing 3796 file(s)
unpacked in 34144 ms

but then when I ran lake exe cache getagain in mathematics_in_lean/ subdir (because I'm not sure what the scope of the cache/build is), I get:

info: Downloading proofwidgets/v0.0.17/linux-64.tar.gz
info: Unpacking proofwidgets/v0.0.17/linux-64.tar.gz
info: [1/9] Building Cache.IO
...
info: [9/9] Linking cache
Attempting to download 3225 file(s)
Downloaded: 0 file(s) [attempted 128/3225 = 3%]
Failed to connect to lakecache.blob.core.windows.net port 443 after 15279 ms: Couldn't connect to server

and the error message keeps repeating until I quit.

Maybe that's transient connectivity / firewall / quota enforcement...

[Ruben Van de Velde]

Yeah, I'd try it again in a little bit

[Kevin Buzzard]

yeah that error doesn't look lean-related. Different projects use different versions of mathlib so you need to download binaries on a per-project basis. Mathlib has about 10 releases per day.

[Kevin Buzzard]

Oh, thank you! I did notice that command on a doc page today, but but I guess I thought it wasn't necessary yet in my context.

It's not necessary, if you're prepared to spend many minutes of build time :-)

[M R]

Something is still wrong with my cache, so I'm leaving mathematics_in_lean compiling Common.lean in the background all day.
I switched to Theorem Proving in Lean and the "Try It" button + import Paperproof is working to execute and visualize those examples. :smiley:
Thanks for the guidance.

[Shreyas Srinivas]

if you want to retry cache after an aborted attempt, it might help to run lake exe cache clean

[Kevin Buzzard]

I think lake clean is even more likely to work (I don't know what the difference is but I've switched to lake clean now always)

[Shreyas Srinivas]

Cache clean specifically purges ~/.cache/mathlib which is usually (and hopefully) not inside the project folder.

[Kevin Buzzard]

And clean just removes stuff like lake_packages and build?

[Shreyas Srinivas]

That's my understanding

[Eric Wieser]

There was a bad release of lake at some point that broke cache (requiring lake clean as a workaround); perhaps MIL doesn't yet have the mathlib change that fixes the issue

[Kevin Buzzard]

Oh maybe that's why I elevated lake clean in my mental model of what to do when things go wrong

[Patrick Massot]

@Eric Wieser which mathlib change are you talking about?

[Patrick Massot]

@M R what is Paperproof in the title of this thread?

[Mauricio Collares]

Patrick Massot said:

Eric Wieser which mathlib change are you talking about?

lean4#2444 introduced new files that should be cached, and #7291 started caching them. In the meantime, the fact that .hash files weren't cached lead to trouble and lake exe cache get didn't work well. I think neither is included in MIL's toolchain though.

[Mauricio Collares]

https://github.com/Paper-Proof/paperproof by @Evgenia Karunus and @Anton Kovsharov.

[Patrick Massot]

Was this ever mentioned here?

[M R]

mathematics_in_lean works pretty well in gitpod, so I was probably just holding it wrong on my local machine. (Unless the gitpod experience is using a fixed good snapshot, and I was using a damaged latest version).

I haven't tried adding Paperproof to the gitpod yet (because I'm running gitpod with Lean on a browser on my phone! :mind_blown: )

I'll try local setup again later, after I run out of free gitpod hours, if I'm not ready to pay.

https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html#getting-started

[Mauricio Collares]

Patrick Massot said:

Was this ever mentioned here?

Not here, but one of the authors posted about it on HN: https://news.ycombinator.com/item?id=37583022

[M R]

I don't think Paperproof can work in Gitpod, since the PaperProof VSCode Extension is not available in the "VSCode for Web" variant that Gitpod uses. (The .lean library seems to work, but there's no way to see the output diagram.)

I'll try again on my local machine at a future point in time, and try to make my local machine setup look the same as the Gitpod workspace.