tooling

Stream: mathlib4

[Scott Morrison]

Thanks to @Yakov Pechersky's efforts on leanproject, and some organisational work around the #port-status page, we now have a nice new tool for inspecting the progress of the port.

cd src
leanproject import-graph --to algebra.order.ring --exclude-tactics --port-status algebra.order.ring.pdf

produces algebra.order.ring.pdf

Here nodes in green have been ported. Nodes in light blue are ready to port. Nodes in darker blue have a PR open already. Nodes in orange are blocked for some reason. You can get more detailed information from

scripts/port_status.py

which currently says

# The following files have all dependencies ported already, and should be ready to port:
# Earlier items in the list are required in more places in mathlib.
logic.basic    -- WIP #484
data.option.defs
data.prod.basic    -- WIP
algebra.group.to_additive
data.bool.basic    -- WIP Kevin Buzzard
control.functor
lean_core.data.vector
data.char
logic.lemmas
category_theory.concrete_category.bundled
algebra.order.floor    -- Blocked by tactic.abel and tactic.linarith
category_theory.elementwise
data.stream.defs
data.rbtree.init    -- Blocked by init.data.ordering.basic
data.num.basic
data.lazy_list
data.nat.bits
data.rbtree.default_lt
lean_core.data.dlist
control.ulift
lean_core.data.buffer
lean_core.data.buffer.parser
data.vector3
algebra.group_power.identities    -- Blocked by current status of ring tactic: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/status.20of.20.60ring.60/near/303965507
data.json
data.sigma.default
control.basic
algebra.hierarchy_design

# The following files have their immediate dependencies ported already, and may be ready to port:
logic.unique
data.option.basic    -- PRd as mathlib4#493
data.nat.cast.defs
logic.relation
group_theory.eckmann_hilton
data.quot
algebra.group.commutator