algebra.order.field.power missing

Stream: mathlib4

[Kevin Buzzard]

Not quite sure what's going on here. Currently ./scripts/port_status.py is reporting algebra.order.absolute_value as ready for porting so I claimed it. But the autoported file is barfing on the notation →ₙ*, which in Lean 3 is notation for docs#mul_hom , defined in algebra.hom.group which does not seem to have been ported.

Digging a little further it seems that in mathlib3, algebra.order.absolute_value imports algebra.order.hom.basic which imports tactic.positivity; so far so good, and we have Mathlib.Tactic.Positivity in mathlib4. However in mathlib3 tactic.positivity imports algebra.order.field.power (because it uses zpow_bit0_nonneg, presumably deprecated in Lean 4) and this latter file has not yet been ported to mathlib4 as far as I can see; in mathlib4 this import is avoided. But I think that this means that actually algebra.order.absolute_value is not at all ready for porting. Is my diagnosis correct and, if it is, how should I indicate this to the system?

[Ruben Van de Velde]

See previous discussion here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress/near/311248898

[Ruben Van de Velde]

Short term, you could add some explicit imports on the mathlib3 side; medium term the script should pick this up, I think

[Eric Wieser]

Adding the explicit import seems totally reasonable on the mathlib3 side

[Scott Morrison]

Yes. The leanproject import-graph --exclude-tactics jumps through some hoops to remember transitive imports as it removes vertices corresponding to tactics files. However port_status.py doesn't.

[Scott Morrison]

Clearly the right solution here is to replace ./scripts/port_status.py with leanproject port-status, so we don't have independent calculations of the "ready" set.

[Eric Wieser]

https://github.com/leanprover-community/mathlib-tools/pull/146 will be a prerequisite for that, currently leanproject doesn't parse as much of the file as port_status does

[Scott Morrison]

Also, leanproject is really slow, because it runs lean --deps a million times, where port_status.py just parses text files.

[Scott Morrison]

I wonder if lean --deps is actually necessary now that we have normalised all the import lines in mathlib.

[Scott Morrison]

I think it used to be necessary because people wrote multiple imports on lines, etc.

[Eric Wieser]

leanproject import_graph isn't just for mathlib, so it ought to deal with things written not in the mathlib style

[Eric Wieser]

Are you happy with https://github.com/leanprover-community/mathlib/pull/17620? It will need a mathlibtools release to unbreak people

[Scott Morrison]

Re: https://github.com/leanprover-community/mathlib-tools/pull/146, won't the comments fields you extract here be clobbered by the port_status() function, which write "ready" without looking?

[Eric Wieser]

Oh, I hadn't realized that the FileStatus objects were mutated later on

[Eric Wieser]

Maybe @Yakov Pechersky can advise what the comments field was intended for

[Scott Morrison]

I think we should just have a separate "ready" field!

[Eric Wieser]

Or just keep a separate is_ready[filestatus] dictionary around inside port_status rather than attaching extra state to FileStatus that is sometimes uninitialized

[Yakov Pechersky]

The mutation is only for the graph display, it doesn't end up reserializing the mutated FileStatus anywhere.

[Yakov Pechersky]

If you do keep the is_ready as a separate dictionary, the coloring code/logic now has to look in several places -- that's why I kept it localized to the FileStatus for now

[Yakov Pechersky]

the comments field was intended for the various additional text that users had put in the yaml, like WIP or claimed by Foo Bar

[Eric Wieser]

I think that's what my PR put in those fields, so it sounds like I did that right at least