add_port_comments.py

Stream: mathlib4

[Eric Wieser]

You need the unreleased version of mathlibtools; I mentioned that in the description of #17600:

pip install git+https://github.com/leanprover-community/mathlib-tools

You might need to uninstall your existing mathlibtools first

[Eric Wieser]

I agree this is sort of problematic, hence me creating this thread on moving the porting stuff out of mathlibtools so that we don't have to deal with release issues

[Riccardo Brasca]

I've done that, but nothing changed. :thinking:

[Eric Wieser]

Did you uninstall the old mathlibtools first?

[Riccardo Brasca]

Ah, I didn't

[Eric Wieser]

Maybe you need pip install git+https://github.com/leanprover-community/mathlib-tools --upgrade to force it to do that

[Riccardo Brasca]

Uninstalling mathlibtools and doing pip install git+https://github.com/leanprover-community/mathlib-tools did something, now there is no error. But there is no output at all

[Riccardo Brasca]

In any case I think we shouldn't say in the wiki to use the script until it is ready

[Eric Wieser]

The script gives no output, it modifies all the files in place

[Notification Bot]

10 messages were moved here from #mathlib4 > Mathlib4 porting meeting series by Eric Wieser.

[Eric Wieser]

Riccardo Brasca said:

In any case I think we shouldn't say in the wiki to use the script until it is ready

We can remove the instruction entirely after #17641