Zulip Chat Archive

Stream: mathlib4

Topic: how to port?

Violeta Hernández (Jan 20 2023 at 00:30):

Sorry, I'm entirely clueless here. I want to port this relatively simple PR #18236 over to Mathlib 4. I've downloaded the mathlib4 and mathlib3port repos, but other than that, I have no idea what to do.

Violeta Hernández (Jan 20 2023 at 00:30):

Is there some sort of guide I'm not seeing?

Mario Carneiro (Jan 20 2023 at 00:31):

#port-wiki

Eric Wieser (Jan 20 2023 at 00:31):

I think the conclusion of the meeting was that open mathlib3 PRs should only be ported after they're merged and mathlib3port has been updated with their contents

Eric Wieser (Jan 20 2023 at 00:31):

Is that now discussed on the wiki?

Mario Carneiro (Jan 20 2023 at 00:31):

...that did not link where I expected

Mario Carneiro (Jan 20 2023 at 00:32):

https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki

Violeta Hernández (Jan 20 2023 at 00:32):

Ah thanks

Violeta Hernández (Jan 20 2023 at 00:33):

So then, I just wait for the PR to be merged, then I do the procedure on the wiki

Eric Wieser (Jan 20 2023 at 00:34):

So far the two reasonable takes I've seen on forward ports are:

  • Do nothing and promise to come back to it later
  • Create a mathlib4 PR with an empty commit (git commit --allow-empty), and update it later once mathlib3port is ready to help you.

and the two less reasonable ones:

  • Run mathport one-shot on the PR files. This is hard to set up in practice
  • Port everything manually before the mathlib3 PR is merged. This is a waste of your time, and also increases the risk of mistakes.

Mario Carneiro (Jan 20 2023 at 00:34):

There is apparently #port-guide, #port-wiki, #port-status and the names don't all seem to match the links

Violeta Hernández (Jan 20 2023 at 04:42):

Hm, wait. So am I supposed to use mathport for these synchronized files?

Violeta Hernández (Jan 20 2023 at 04:42):

Or is the idea that I write the code myself?

Violeta Hernández (Jan 20 2023 at 04:43):

Or do I need to wait for mathport to be able to port that?

Violeta Hernández (Jan 20 2023 at 04:43):

I don't get it :frown:

Johan Commelin (Jan 20 2023 at 04:49):

@Violeta Hernández Every 2 hrs, mathport builds a new translation of mathlib3.

Violeta Hernández (Jan 20 2023 at 04:50):

Ah, I wasn't aware of that

Johan Commelin (Jan 20 2023 at 04:50):

At that point, you can go to the mathlib3port repo, and navigate to the file that you want to port some decls from

Johan Commelin (Jan 20 2023 at 04:50):

And then just copy paste those decls, and commit them in mathlib4. After that, create more commits that fix the errors.

Johan Commelin (Jan 20 2023 at 04:51):

You are encouraged to create a first commit with "Output of mathport". So that we can review a diff of your changes compared to that baseline.

Violeta Hernández (Jan 20 2023 at 04:59):

You do mean this, right? https://github.com/leanprover-community/mathlib3port

Violeta Hernández (Jan 20 2023 at 04:59):

188 commits seems like too few for "every 2 hours"

Violeta Hernández (Jan 20 2023 at 04:59):

(or maybe I just rejoined at the most inconvenient time possible?)

Johan Commelin (Jan 20 2023 at 05:06):

Until Jan 10 it was updating twice a day.

Ruben Van de Velde (Jan 20 2023 at 06:04):

I thought it updated mathlib 4 every 2 hours and mathlib 3 every 12

Johan Commelin (Jan 20 2023 at 06:05):

Ooh, you are right. So if you want to forward port something from ml3, you might need to wait a bit longer

Violeta Hernández (Jan 20 2023 at 15:29):

Mathlib3port is currently tracking a 20 hour old commit

Violeta Hernández (Jan 20 2023 at 15:38):

Seems more than 12 hours

Eric Wieser (Jan 20 2023 at 15:42):

You would expect the commit to be old by 12 hours + mathport runtime + mathlib3 bors runtime

Eric Wieser (Jan 20 2023 at 15:43):

How old is the commit tracking the 20 hour old commit?

Reid Barton (Jan 20 2023 at 15:47):

The next mathlib commit says it's 17 hours old but I don't know what time that is (i.e. original commit time or bors push time)

Violeta Hernández (Jan 20 2023 at 15:47):

https://github.com/leanprover-community/mathlib3port/commit/f41e4409e581f573c2367566d0eb6ccebdc651ee

Violeta Hernández (Jan 20 2023 at 15:47):

It's 12 hours old

Violeta Hernández (Jan 20 2023 at 15:48):

Ah so I see,

  • mathlib 3 is updated 20 hours ago
  • mathlib3port reads that last PR 12 hours ago

Violeta Hernández (Jan 20 2023 at 15:48):

I'm bad at maths it seems

Last updated: Dec 20 2023 at 11:08 UTC