chore: move to module system

[zhikaip]

Ran Modulize.lean (placed the file under scripts folder).

There's some metaprogramming things that I'm not quite sure how to fix, consulted ChatGPT which managed to remove all errors, but I'm completely lost and would like to ask for a double check. The changes are in PhysLean/Meta/Basic.lean, other changes are just meta imports/ meta defs.

Removed private lemma labels in PhysLean/Mathematics/SchurTriangulation.lean and PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean. Those broke the files so I removed them for now, not sure what's the correct way to label them in the module system.

Currently I'm stuck at sorryful declarations, where there's no error in the file, but the build fails with error message Unknown attribute [Sorryful_attr] (e.g. PhysLean/ClassicalMechanics/Pendulum/CoplanarDoublePendulum.lean). I believe there's a same issue with the pseudo attribute. Can't figure this out and would like to ask for assistance.

Edit: I guess the github workflows should also be updated

[morrison-daniel]

This is not something I'm knowledgeable in so take my suggestion with a grain of salt, but this is what I figured out from looking at error messages.

I believe the only issue with the Python based style linter is that only certain commands are allowed before the module doc-string, imports being one of them, and it's complaining now that imports have public in front of them. It looks like it's defined in physlib/scripts/lint-style.py on line 295 with

if words[0] != "import" and words[0] != "--" and words[0] != "/-!" and words[0] != "#align_import":

I think it should work if you change this to

if words[0] != "module" and words[0] != "public" and words[0] != "--" and words[0] != "/-!" and words[0] != "#align_import":

These are essentially the only ways that lines are allowed to start before doing the module doc-string.

[jstoobysmith]

I think the sorryful attribute error is down to needing to use the meta phase:

https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/#meta-phase

Not sure exactly how this works, but an example is here:

https://github.com/leanprover-community/mathlib4/blob/6e9770b32070f0b41f9cc08bf2838afdd7d58c17/Mathlib/Tactic/Bound/Attribute.lean#L13

I will try and experiment when I get chance.

[zhikaip]

I think I fixed most changes, I had to remove all private declarations wherever it was throwing errors, and there's some meta imports both for sorryful and when native_decide is used. I'm currently stuck on PhysLean/Mathematics/List.lean where's there's some very nasty fintype casting going on, which is a result of List.insertionSort and List.orderedInsert no longer exposed. Not sure whether any additional API is needed or there are cleverer ways to work around this.

[zhikaip]

update: I now realise I can do import all to circumvent some expose issues, now there's only one lemma near the end (insertionSortEquiv_order) which has synthesising issue due to casting in insertionSortEquiv.

Edit: tried hacking my way through more of it, but the insertionSortEquiv is causing all sorts of trouble. @jstoobysmith would appreciate if you have time to have a look and review whether the current implementation needs updating. QFT/Koszul rely quite heavily on this and I'm not comfortable pushing this further without knowing what I'm doing.

[jstoobysmith]

There was somewhere you added native_decide right? I can't seem to find it anymore

[jstoobysmith]

@copilot What files in this PR contain changes other than standard changes going to the module system.

[Copilot]

@jstoobysmith I've opened a new pull request, #980, to work on those changes. Once the pull request is ready, I'll request review from you.

[jstoobysmith]

What files in this PR contain changes other than standard changes going to the module system.

This didn't do what I intended - sorry for the noise :).

[Copilot]

@jstoobysmith I've opened a new pull request, #981, to work on those changes. Once the pull request is ready, I'll request review from you.

[zhikaip]

There was somewhere you added native_decide right? I can't seem to find it anymore

This is the final commit, in wickcontraction/extractequiv

[zhikaip]

I'm not sure what @[pseudo] does, are those precisely the native_decide uses? I think these were where meta import were used, but I can't find a list of pseudo tags

Other changes are in mathematics/list.lean and files that import it, maybe you can look for import all (implementation of insertionsort and orderedinsert not exposed or something along those lines)

[jstoobysmith]

Will do - native_decide adds a new axiom (it assumes the compiler), the tag @[pseudo] is just a way to track which results use this extra axiom

[jstoobysmith]

Fixed native_decide based on https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Fin.2Efind.3F.20and.20decide.20in.20v4.2E26.2E0/with/578113269

[jstoobysmith]

I would like to see how far we could get without actually modifying the Lean code in the Lists sections.
It seems like using

@[expose] section

works better here, then using

@[expose] public section

But I am not sure the consequences there of.

Also... just

public section 

seems to work.

[jstoobysmith]

I fixed the lists parts using the module system so reverted some of your changes.

Two further questions:

• Do you know of any further files where you changed e.g. proofs?
• What is the status of the linters - do we know if they all still work?

[zhikaip]

bf34ee8

Should be the remaining changes

For linters I only changed lint-style.py following @morrison-daniel 's comment above and hard coding the first word of different import statements

[zhikaip]

If you mean the sorryful attributes, changing it to public meta imports seems to solve the issues, but I'm not sure if it works (is public meta import same as public import + meta import?)

[jstoobysmith]

Yeah I think your method works here. This all looks good to me now. I'll check through the files again sometime this afternoon. But then will approve.

When we merge this we should probably post on the Zulip given that it is a fairly big change.

[jstoobysmith]

Approved - you should be able to merge after linters.
Many thanks for doing this.