22
$\begingroup$

I am trying to update a large body of Lean code to work with the current version of mathlib. This is difficult because there have been a large number of backwards-incompatible changes even since I last did this in mid-November. When I come across something that no longer works, I guess some keywords and try to search for commits or issues or current code in github that explains what has changed and why. Is there any recommended method that is more systematic than this?

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ I don't know the details of how to do the following, but hopefully someone else will: I believe that for some projects (for example the liquid tensor experiment) there's a script somewhere which checks that the project builds against mathlib master, and if it doesn't then it starts sending notifications or emails or something; this way you discover the moment your project is not compatible with mathlib and it's much easier to fix because the problem is "one of the last few commits" as opposed to "something which happened some time between now and last November". $\endgroup$
    – Kevin Buzzard
    Commented Feb 8, 2022 at 22:25
  • 1
    $\begingroup$ There ought to be a way to use git bisect to pinpoint the change that broke your code. Once you know when precisely it happened, it should be easier to figure out how to adapt your code to the changes. The Lean community might actually be interested in providing some support for this, so that not every Lean user has to learn git bisect. $\endgroup$
    – Andrej Bauer
    Commented Feb 8, 2022 at 22:54
  • $\begingroup$ Unfortunately git bisect can be very expensive if you have any significant dependencies on mathlib. For each bisect, you need to either compile mathlib locally -- which can take hours depending on the dependencies and your machine -- or download an olean cache of up to 60mb. $\endgroup$
    – Rob Lewis
    Commented Feb 8, 2022 at 23:11
  • 3
    $\begingroup$ git log -Slemma_that_used_to_exist is invaluable when updating like this it gives you the log of commits whose diff contains that string, most likely containing the last time it was moved or renamed! $\endgroup$
    – Alex J Best
    Commented Feb 9, 2022 at 0:18

1 Answer 1

Reset to default
17
$\begingroup$

The mathlib commit log serves as a de facto changelog. Since the project updates far too frequently to keep a traditional changelog, a good method if you know approximately when breaking changes occured is to look at commits around that date. Titles are hopefully descriptive, and link to the pull request which explains the change in more detail.

The leanprover-community organization hosts CI for third-party projects, including a GitHub Actions script that will try to update your project periodically. If changes in mathlib break your code, it will open an issue on your repository linking to a diff of the mathlib changes that may be to blame.

Note that this action is most helpful if you fix the breakage relatively quickly. Breaking changes can compound, and it can only alert you at the first breaking change.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.