mathlib-tools PR #12

Stream: general

[Gabriel Ebner]

This is about @Patrick Massot's PR making mathlib-tools a python package, installable via pip: https://github.com/leanprover-community/mathlib-tools/pull/12
Who do I need to bug to get this merged? AFAICT pip install mathlibtools works fine now on linux and windows.
The reason why I'm so desperate for this change is because otherwise it's virtually impossible to use mathlib-tools on NixOS.

[Rob Lewis]

@Simon Hudon ? Mind if we merge this? :)

[Patrick Massot]

The canonical answer here is Simon.

[Patrick Massot]

But I guess he wouldn't mind giving admin rights for this repo to more people.

[Patrick Massot]

If you want this merged, what you can do to help is to prepare a mathlib doc update ready to be merged immediately after this PR to mathlib-tools.

[Gabriel Ebner]

Ok, I'm on the doc update.

[Kevin Buzzard]

Just to remark that the auto-generated little blue arrow link in the topic title links to the wrong place.

[Gabriel Ebner]

#2010

[Simon Hudon]

I don't like how the CI scripts are changing. It will always only test the official versions on pip, not the latest commit

[Gabriel Ebner]

The CI scripts in the mathlib-tools repository always check the latest commit, not the one on pypi. (Note: the installation command is pip3 install . and not pip3 install mathlibtools)

[Simon Hudon]

Nice! I missed that

[Scott Morrison]

Maybe we should have a comment on that line to that effect.

[Simon Hudon]

:+1: