mathport experience

Stream: mathlib4

[Michael Stoll]

I have used mathport for a project (consisting of three files) as described here. It worked reasonably well, with a few exceptions.

• Zmod instead of ZMod in the imports (and Tactic.Basic, which does not seem to exist anymore)
• It insists on changing mul into hMul in all theorem names
• In some cases, it fails to change nat.foo or int.foo into Nat.foo or Int.foo
• When p : Nat and a : Int, \u p \mid a now gives an error in some cases (maybe it's unfair to blame mathport for that)
• Similarly with things like a / b, where a : Int and b : Nat (looks for some HDiv instance...)
• It does not translate div and mod in lemma names to ediv and emod where appropriate
• It changes names of definitions and lemmas according to the new naming convention, but does not also change them at places where they are used

[Ruben Van de Velde]

All of those sound like issues we've encountered during porting mathlib (except the hMul one, I haven't seen that)

[Ruben Van de Velde]

And theorem names not being translated is something I've generally seen in the parts of a proof after another error

[Jireh Loreaux]

The import issue is just handled by a specific translation table (or rather, a table of exceptions to the rule, like ZMod), so updating that should be the fix there.

[Eric Wieser]

That table isn't implemented

[Eric Wieser]

We have the interface to it, #align_import, but mathport was never taught how to read it

[Jireh Loreaux]

?? We definitely had something working for NNReal and the like. I remember editing it.

[Jireh Loreaux]

Oh maybe it was part of the start_port script.

[Jireh Loreaux]

Which makes both of our statements agree.

[Mario Carneiro]

Eric Wieser said:

We have the interface to it, #align_import, but mathport was never taught how to read it

I was thinking I would implement it, but it turns out it's not that simple, #align_import is actually dropping its data on the floor so there is nothing mathport can do to recover it

[Michael Stoll]

I noticed that mathport generated #align_import lines in the lean4 files (which led to an error message from expected at the beginning of the following module docstring IIRC).

[Eric Wieser]

Mario Carneiro said:

Eric Wieser said:

We have the interface to it, #align_import, but mathport was never taught how to read it

I was thinking I would implement it, but it turns out it's not that simple, #align_import is actually dropping its data on the floor so there is nothing mathport can do to recover it

Yes, my thinking was that you'd know better what it should be doing with its data anyway, so I'd let you or someone else implement both ends at the same time

[Yaël Dillies]

The hMul problem appeared last Thursday IIRC.

[Michael Stoll]

"appeared" = "was noticed" or "was introduced"?

[Yaël Dillies]

Was introduced. One of Mario's commits. I know it because I mathported one project on Wednesday and one on Thursday and I saw the error appearing from one to the next.

[Yaël Dillies]

And indeed I checked the commits and you can see the mathport going all wrong on mul after that one commit.

[Mario Carneiro]

which one?

[Mario Carneiro]

#3926 implements the environment extension

[Yaël Dillies]

Will be at a computer in a bit. Can tell you.

[Mario Carneiro]

lol, I'm about to board a flight, let's see if you can get it in time

[Mario Carneiro]

Did we actually want to do anything with the origin information in #align_import?

[Mario Carneiro]

I guess you meant last last thursday: https://github.com/leanprover-community/mathlib3port/commit/60285dccd117e90dd1faa65f8ae103e9befb924f

[Eric Wieser]

The origin info was mainly there to support the dashboard

[Mario Carneiro]

And this commit was caused not by any change of mine, but a mathlib bump https://github.com/leanprover-community/mathlib4/compare/72b6e76...d66f29ee

[Mario Carneiro]

which includes a lean bump 08-05 -> 08-15 https://github.com/leanprover/lean4/compare/254582c...b5a7367