mathport runs

Stream: mathlib4

[Johan Commelin]

@Mario Carneiro can we easily run mathport on the "shoreline" of the rising tide?

[Johan Commelin]

If that's not to hard, I think it would be helpful to run it every hour

[Mario Carneiro]

hm, that will get awkward because then you have a bunch of partial mathport runs so it's not obvious what to download to make sure you don't get weird errors due to mismatching oleans

[Johan Commelin]

Could there be a Oneshot directory frequently publishes oneshot-ports of the shoreline?

[Johan Commelin]

Oneshot can be used in that way, right?

[Johan Commelin]

I think I'm just hoping that mathport can use some "cache" from previous runs, or something. Having hourly output would be really useful at times.

[Mario Carneiro]

TBH that's not really my expertise. It sounds doable in principle, most of the things are being cached, but wrangling the github actions sounds like something I will pray for someone else to pick up ;P

[Gabriel Ebner]

on the "shoreline" of the rising tide?

I live at the sea, but I can't make any sense of this analogy. Can you be a bit more specific please?

[Gabriel Ebner]

If that's not to hard, I think it would be helpful to run it every hour

We could certainly run mathport more than twice a day for the same mathlib3 commit, that is, only picking up changes from mathlib4. The mathport run takes a bit less than an hour. How about once every two hours?

[Gabriel Ebner]

Picking up changes from mathlib3 more frequently is not really in the cards, it takes a couple of hours to build (and we can't use the caches because we need to generate tlean&ast files).

[Johan Commelin]

Already, picking up new #aligns from mathlib4 would be really useful.

[Johan Commelin]

Re "shoreline": I just mean the files that are ready to be ported (or maybe are 1 step away from ready to be ported)

[Eric Rodriguez]

Gabriel Ebner said:

Picking up changes from mathlib3 more frequently is not really in the cards, it takes a couple of hours to build (and we can't use the caches because we need to generate tlean&ast files).

Could we make the mathlib3 CI build and store these too? Or is it not worth it?

[Gabriel Ebner]

I don't think it's really worth it at this point. mathlib3 development is slowing down anyhow.

[Eric Wieser]

Where does the current CI run from?

[Gabriel Ebner]

I'm not sure I understand the question.

[Eric Wieser]

Where do I navigate to on GitHub to see the runs?

[Gabriel Ebner]

https://github.com/leanprover-community/mathport/actions

[Gabriel Ebner]

update = bump mathlib4 dependency
mathport = run mathport and push to mathlib3port
predata = build mathlib3

[Eric Wieser]

Thanks!