Do port status scripts belong in mathlibtools or mathlib?

Stream: mathlib4

[Eric Wieser]

Right now, we have two different parsers for the mathlib port data:

• One in mathlibtools which creates the input graphs
• One in mathlib/scripts which outputs the port status on the command line

Having these live in two different places feels like a mistake, since it means if we change the format we end up breaking one of them. It also means we end up writing the same code twice (or worse, having bugs in one but not the other).

There are two ways we could go about this:

• Push as much upstream into mathlibtools as possible (the approach I took in #17620)
• Remove any knowledge of porting from mathlibtools and put it all in the scripts directory. Those scripts can of course still import mathlibtools.lib to access things like the import_graph.

The advantage of the first approach is that users don't need a checkout of mathlib to run the script. The advantage of the second is that we don't have to have @Patrick Massot publish a new release every time we adjust the script (each release of which risks breaking regular leanproject users with no interest in porting)

[Yakov Pechersky]

Can we ask users to either clone mathlib tools and pip install -e, or pip install directly pointing to the github repo? With pip install -U if needed.

[Scott Morrison]

@Yakov, too complicated, let's not add any installation steps.

[Scott Morrison]

@Eric Wieser, I agree everything should be in one place, but it's not super high priority. I would like there to be an import-graph --port-status command somewhere that generates a PDF, and it seems rather cumbersome to have this anywhere except in mathlibtools, without essentially forking mathlibtools over into mathlib, which sounds a bad idea.

[Scott Morrison]

My preference is thus to push stuff upstream to mathlibtools. I think Patrick is happy for us to play a bit faster and looser there than we used to, in the service of making porting easier. I'm happy to review and hit merge on PRs there, although I don't check it as often so a ping is useful. Similarly, I think Patrick is happy to cut a new release in response to a ping; and if that becomes cumbersome I suspect he's happy to let someone else cut the new releases.

[Yakov Pechersky]

I agree that these are extra steps. But we still require users to upgrade mathlibtools every so often with a pip command

[Yakov Pechersky]

We could put porting py files into mathlib, and retain port-status graph commands in mathlibtools, by doing unholy sys.path manipulation to import pt files from mathlib

[Eric Wieser]

Scott, files in the script directory can still import all the import graph stuff from mathlibtools to build the port graphs

[Eric Wieser]

(maybe that's not true for pipx users ...)