Linting PhysLean

Stream: PhysLean

[Joseph Tooby-Smith]

I made this PR PhysLean#790 which contains some documentation about the various linters which can be run on PhysLean and what they do. If anyone has any suggestions of how it can be improved, I would be very glad to hear them.

[Fabio Anzà]

Hey @Joseph Tooby-Smith , I was going through the linters (lake exe lint_all) and the Style linter was flagging a bunch of stuff on SpaceTime, which is not at all what I worked on.

The question is: should I fix those as well?

[Joseph Tooby-Smith]

Hmm odd, could you paste the output here? But no need to fix these.

[Joseph Tooby-Smith]

Ok, I manage to work this out - the linter errors you are seeing are on "optional linters" (lets call them), ones that appear in lake exe lint_all but are not strictly enforced by GitHub, so sometimes slip through the net.

I have fixed them in PhysLean#820, which I will merge, and then make a note here - after which merging with Master should remove these errors for you. (update: This PR has now been merged into master).

[Joseph Tooby-Smith]

(deleted - on a train with poor internet so sent message twice)

[Fabio Anzà]

Thanks, but it happened again. Not sure why. I'm attaching a screenshot
Screenshot 2025-11-27 at 6.53.07 PM.png

[Fabio Anzà]

I'm happy to fix them and they can get pulled once I issue the PR

[Joseph Tooby-Smith]

They should be fixed now :). You will need to update your fork with master (merge master into your fork), but then these should go away, no need for you to do anything :).

[Rein Zustand]

I saw the style linter in https://github.com/HEPLean/PhysLean/pull/849 took ~30 min to complete. Whereas in Mathlib, most lints completed in ~2 min or less: https://github.com/leanprover-community/mathlib4/pull/33368. Is it because the GH Actions CI compiled the entirety of PhysLean in addition to just checking the syntax? If so I think it would be more productive to separate the syntax checking and fail the long compilation early when the syntax check / any fast checks fail.

[Joseph Tooby-Smith]

I think the underlying reason behind this is that Mathlib is caching builds, whilst PhysLean isn't. There have been a few discussions on best ways to set up a cache for PhysLean, but none have yet led to anything.

Some of the linters specifically require PhysLean to be build before they can be applied, and this is why things are slowed. But no doubt things can be rearanged in a better way, and I think this is something we should explore.

In the mean time, I recommend people lint locally rather than relying on the linters on GitHub. Instructions can be found here:

https://github.com/HEPLean/PhysLean/blob/master/scripts/README.md

[Rein Zustand]

Ah, I see. Updating on my previous post, I was comparing apples to oranges. The fast linter that took < 2 min is actually the Python-based linter, which PhysLean already uses. The time comparison should have been 11 min Mathlib lake build vs 30 min PhysLean lake build.

There have been a few discussions on best ways to set up a cache for PhysLean, but none have yet led to anything.

I couldn't find the discussions (I searched with the keyword "cache"). Would following how Mathlib does it be strictly better than the current setup? There could always be a better method, but this can be discussed in the future. I can help prepare this, if agreed.

[Joseph Tooby-Smith]

Here is a previous discussion on this:

#general > Cache for PhysLean and projects downstream of Mathlib

I believe that Mathlib's cache is stored on a server (either explicitly, or the workflow is run directly on said server), and paying for said server is one of the things that prohibits us copying Mathlib's approach.

[Rein Zustand]

I see (I only searched within #PhysLean ), the Mathlib's cache seems to be stored in Azure Blob Storage (https://github.com/leanprover-community/mathlib4/blob/69fc0048aa48ab4674e6fb9f0ad1b6446d04eca7/Cache/Requests.lean#L251C6-L251C45).

From the release note of Lean 4.25, remote cache feature is already in:

#10188 adds support for remote artifact caches (e.g., Reservoir) to Lake. As part of this support, a new suite of lake cache CLI commands has been introduced to help manage Lake's cache. Also, the existing local cache support has been overhauled for better interplay with the new remote support.

I think there is no uncertainty on the direction of which method to use.

[Rein Zustand]

paying for said server is one of the things that prohibits us copying Mathlib's approach.

Claude Code's estimate is ~$500/month (because of the egress traffic). But Mathlib also uses Cloudflare R2, which has $0 egress fee. The fee could as well be $50/month.

[Joseph Tooby-Smith]

Rein Zustand said:

paying for said server is one of the things that prohibits us copying Mathlib's approach.

Claude Code's estimate is ~$500/month (because of the egress traffic). But Mathlib also uses Cloudflare R2, which has $0 egress fee. The fee could as well be $50/month.

I used to pay $50/month for a server for PhysLean - to run a search engine, and an online playground. Over the months this quickly adds up though.

I may have some research money I can use for this, but I will need to ask if this is an allowed expense, and how it would work. Otherwise maybe we could get a small grant for it or sponsor etc.

[Rein Zustand]

Otherwise maybe we could get a small grant for it or sponsor etc.

The frontier AI labs are benefiting a lot from the Lean formalization. I think we can ask one or few of them to fund the expenses. If Mathlib's Azure expense were in fact be $500/month, it could likely had been subsidized by Microsoft themselves.

[ZhiKai Pong]

I'm having trouble running lake exe lint_all, here's the error message:

✖ [6/9] Building UnicodeBasic/UnicodeCLib
trace: .> cc -c -o C:\lean\PhysLean\.lake\packages\UnicodeBasic\.lake\build\UnicodeCLib\case.o C:\lean\PhysLean\.lake\packages\UnicodeBasic\UnicodeCLib\case.c -I c:\Users\username\.elan\toolchains\leanprover--lean4---v4.27.0\include -O -fPIC
error: failed to execute 'cc': no such file or directory (error code: 2)
trace: .> cc -c -o C:\lean\PhysLean\.lake\packages\UnicodeBasic\.lake\build\UnicodeCLib\prop.o C:\lean\PhysLean\.lake\packages\UnicodeBasic\UnicodeCLib\prop.c -I c:\Users\username\.elan\toolchains\leanprover--lean4---v4.27.0\include -O -fPIC
error: failed to execute 'cc': no such file or directory (error code: 2)
Some required targets logged failures:
- UnicodeBasic/UnicodeCLib
error: build failed

does anyone know what I should do to make this work?

[ZhiKai Pong]

this is after lake update and lake build both succeed

[ZhiKai Pong]

update: seems to work after installing MSYS2 and updating system PATH (following instructions from AI) but not sure whether this is the proper way or am I missing something.

[Joseph Tooby-Smith]

@ZhiKai Pong Are you using windows?

[ZhiKai Pong]

yea this is on windows, not sure what changed

[Joseph Tooby-Smith]

It seems to be working fine for me on a mac, as another data point.