Zulip Chat Archive

Stream: mathlib4

Topic: mathport runs


Johan Commelin (Jan 11 2023 at 08:33):

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

Johan Commelin (Jan 11 2023 at 08:33):

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

Mario Carneiro (Jan 11 2023 at 11:24):

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 (Jan 11 2023 at 11:26):

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

Johan Commelin (Jan 11 2023 at 11:26):

Oneshot can be used in that way, right?

Johan Commelin (Jan 11 2023 at 11:28):

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 (Jan 11 2023 at 11:31):

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 (Jan 11 2023 at 17:54):

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 (Jan 11 2023 at 17:57):

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 (Jan 11 2023 at 17:58):

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 (Jan 11 2023 at 18:03):

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

Johan Commelin (Jan 11 2023 at 18:04):

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 (Jan 11 2023 at 19:27):

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 (Jan 11 2023 at 19:30):

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

Eric Wieser (Jan 11 2023 at 19:34):

Where does the current CI run from?

Gabriel Ebner (Jan 11 2023 at 19:40):

I'm not sure I understand the question.

Eric Wieser (Jan 11 2023 at 19:41):

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

Gabriel Ebner (Jan 11 2023 at 19:41):

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

Gabriel Ebner (Jan 11 2023 at 19:42):

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

Eric Wieser (Jan 11 2023 at 19:42):

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC