mathport re-org

Stream: mathlib4

[Daniel Selsam]

@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]

Yes, this is definitely better.

[Daniel Selsam]

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]

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]

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]

It should probably instead run on every commit to master.