Zulip Chat Archive

Stream: mathlib4

Topic: mathport re-org


Daniel Selsam (Nov 11 2021 at 17:45):

@Scott Morrison I think having the Lib4 directory (and fake package) is confusing now that we have separate stand-alone packages that download the releases. It also seems annoying to require two separate repos for leanbin and mathbin. I just pushed a commit to my fork that addresses these: https://github.com/dselsam/mathport/commit/ad83ed70e9e0480d082dce6c0cd0d6a500656cc6 Now the mathport outputs are just placed directly in the otherwise-empty Outputs/[lean|math]bin/[oleans|src], and Lean4Packages/[lean|math]bin contains the lakefiles that download the releases from the web. Note: the Lean4Packages lakefiles are still pointing to my "test" release because they are expecting the oleans in the tar file to be top-level rather than inside build/lib. I changed make tarballs accordingly: https://github.com/dselsam/mathport/blob/master/Makefile#L103-L107 but didn't change the github action. Thoughts?

Scott Morrison (Nov 11 2021 at 21:03):

Yes, this is definitely better.

Daniel Selsam (Nov 11 2021 at 22:35):

OK I pushed the commit to leanprover-community. I didn't change the CI branch though -- will it automatically use the master branch for the action? Does it need to be a separate branch or should the action go into master eventually?

Mac (Nov 11 2021 at 23:20):

Note that doing this has the disadvantage of now creating a copy of this monolithic mathport report for each of leanbin and mathbin. At least with the current way Lake resolves sources.

Scott Morrison (Nov 11 2021 at 23:38):

No, the CI branch should eventually be merged. I need to fix up the workflow file first, however. Currently it is set to run on every push to a pull request.

Scott Morrison (Nov 11 2021 at 23:39):

It should probably instead run on every commit to master.


Last updated: Dec 20 2023 at 11:08 UTC