mathport and forward-porting

Stream: mathlib4

[Mario Carneiro]

This is very much not recommended. If you differ too much from mathport's output then later diffing is a lot harder

[Eric Wieser]

I think the problem is:

• Our current "all mathlib3 PRs must have an open forward-ported PR" stance means that we can't rely on the mathport nightlies to do our work for us.
• There is significant activation energy required to install mathport from the command line.
• Even if everyone did have a mathport installation****, we don't have any tools to compute appropriate diffs

[Mauricio Collares]

Yaël only submitted synchronization PRs as far as I can tell, so maybe mathport was not particularly useful for them

[Eric Wieser]

Right, but @Yaël Dillies did not ask mathport to translate their new lemmas, and instead guessed the translation. I would imagine that probably they made good guesses, but that's not really the point; mathport should be making as many decisions as it can for us,

[Yaël Dillies]

Yes, I feel exactly as Eric on this issue.

[Eric Wieser]

@Mario Carneiro, can mathport be used incrementally? Can I start with mathport output from $(git merge-base HEAD my_pr), and ask it to build the files on my_pr without touching the files with unchanged oleans?

[Notification Bot]

30 messages were moved here from #mathlib4 > port progress by Eric Wieser.

[Mario Carneiro]

Yes I think so. You would need to lean-3-build any files that you want to port (and their dependencies), and then you can call mathport on them

[Eric Wieser]

So lean --make $(filenames-changed) and then mathport $(filenames-changed) would work?

[Mario Carneiro]

modulo finicky command line syntax, yes

[Mario Carneiro]

you also have to make sure you have the right versions of stuff checked out

[Mario Carneiro]

it would be nice to have a makefile target or python program which automates this

[Eric Wieser]

Yes, I'm asking these questions with a view of automating this

[Eric Wieser]

you also have to make sure you have the right versions of stuff checked out

As in, you need merge-base to be a mathport-consumed commit?

[Eric Wieser]

I think it might help if there was a "latest mathport" branch in leanprover-community/mathlib

[Mario Carneiro]

More specifically, the main compiler commands you need are:

• lean --make --recursive --ast --tlean $(filenames-changed) (not entirely sure what --recursive does but it's in the makefile)
• ./build/bin/mathport --make config.json Leanbin::all Mathbin::$(filenames-changed) >> Logs/mathport.out 2> >(tee -a Logs/mathport.err >&2)

[Mario Carneiro]

Eric Wieser said:

you also have to make sure you have the right versions of stuff checked out

As in, you need merge-base to be a mathport-consumed commit?

You need to have the sources/lean and sources/mathlib directories checked out in such a way that calling lean 3 doesn't cause the world to be recompiled

[Mario Carneiro]

it doesn't have to be any particular commit, but you need to have predata that isn't out of date relative to the source files or else lean will recompile

[Gabriel Ebner]

not entirely sure what --recursive does but it's in the makefile

lean --recursive directory/ compiles all *.lean files inside directory/. It doesn't have an effect if you're passing it files.

[Gabriel Ebner]

./build/bin/mathport --make config.json Leanbin::all Mathbin::$(filenames-changed) >> Logs/mathport.out 2> >(tee -a Logs/mathport.err >&2)

That must be:
build/bin/mathport config.json Mathbin::$(lean3-modulenames-changed)

[Gabriel Ebner]

mathport --make will ignore all files that already have a Lean 4 olean.