Creates a python package

[PatrickMassot]

It includes cache-olean, update-mathlib and setup-lean-git-hooks.

Please review but do not merge yet. Merging this will require coordination with mathlib documentation update.

[cipher1024]

What does the installation line become?

[PatrickMassot]

The installation line would be pip install mathlibtools (or the same with --user or sudo depending on the local setup).

[gebner]

The scripts/install_debian.sh file still needs to be updated. Unfortunately, I can't push updates to this branch.

[PatrickMassot]

@gebner can you try to push to https://github.com/leanprover-community/mathlib-tools/tree/package? If this work we can close this PR and reopen from there (unless someone knows how to switch the PR branch origin).

[gebner]

Oh, apparently I can push to this branch as well. Sorry for bothering you.

[PatrickMassot]

This is super weird. Does anyone have any idea how Gabriel hacked my repo?

[gebner]

@PatrickMassot There is an "allow edits from maintainers" button that is automatically checked when creating a PR: https://help.github.com/en/github/collaborating-with-issues-and-pull-requests/allowing-changes-to-a-pull-request-branch-created-from-a-fork

Apparently I'm a mathlib-tools maintainer. 🤷‍♂️

[gebner]

The CI checks only fail due to github API rate limits now.

[cipher1024]

The solutions to this is use a GitHub token to query GitHub and only work on PRs on this repo (no forks)

[gebner]

@cipher1024 I thought this is what GITHUB_CRED is for, but it doesn't seem to be set on PRs. I'm not sure if it's possible to enable the secret for all PRs in travis.

[cipher1024]

I didn't notice, it's on Patrick's repo. That's why the tokens aren't being used.