Use last-changed SHAs instead of HEAD shas

[eric-wieser]

This changes the SHA in the file header to refer to the last commit at which the Lean3 file was changed (at or before the revision used by mathport), rather than always pointing at the latest revision. This means that mathport will no longer update every single file every time it runs on a new version of mathlib3.

Advantages of this approach:

• the repo size will be smaller to host on and download from github
• diff views in the github UI are not going to include 3000 lines of sha changes hiding interesting changes
• analysis scripts for the mathlib-port-status webpage do not need to check every file for changes in every commit

Disadvantages of this approach:

• The sha is now less effective as a proxy for "which run of mathlib3port did this file come from". The sha is already ineffective for this though, as mathlib3port output is updated 12x daily, while the sha is updated just once.
• It does not track changes to mathport output caused by changes to lean3 files that a file depend on. I don't know if these are possible. Note however that the upstream-rev file still contains the same sha as it always did; so this information remains visible in the repo.

Tested by looking at the CI output and verifying the sha for algebra/algebra/basic.lean points to the expected commit.

---

• depends on: #229

[eric-wieser]

This now uses https://github.com/leanprover-community/mathlib/commit/4ea65cad5ad088877e021da13201d55a93c92366 for algebra/algebra/basic.lean instead of the https://github.com/leanprover-community/mathlib/commit/28aa996fc6fb4317f0083c4e6daf79878d81be33 which is used in mathlib3port

So this seems to be working as intended.

[eric-wieser]

Discussed on Zulip here

[gebner]

@eric-wieser This PR broke CI.

find sources/lean/library/ -name "*.ast.json" -o -name "*.tlean" -o -name upstream-rev -o file-revs.json | tar -czvf lean3-predata.tar.gz -T -
find: paths must precede expression: `file-revs.json'
find sources/mathlib/ -name "*.ast.json" -o -name "*.tlean" -o -name upstream-rev -o file-revs.json | tar -czvf mathlib3-predata.tar.gz -T -
find: paths must precede expression: `file-revs.json'

[eric-wieser]

Whoops, sorry. I think Mario pushed a fix.