automatic upgrade of files to a newer mathlib version

Stream: mathlib4

[Roozbeh Yousefzadeh]

Hello, I wonder if there is an automated tool/script that can upgrade a set of Lean files from one version to a more recent one. For example, upgrading from 4.17 to 4.18. Thanks.

[Filippo A. E. Nuccio]

Is your "set of lean files" part of a project?

[Kevin Buzzard]

The short answer is that there isn't, and in the FLT project I am dealing with this by bumping every week or so and if something goes wrong then the changes tend to be fresh in the community's mind so it's not hard to find someone who can fix the problem for you. I agree that this is not ideal, but with lean still in a period of very dynamic development and mathlib not able to promise any backwards compatibility for this and other reasons, that's how things work right now.

[Roozbeh Yousefzadeh]

Filippo A. E. Nuccio said:

Is your "set of lean files" part of a project?

Yes, files are part of multiple projects. It is possible to merge them into a single file.

[Roozbeh Yousefzadeh]

Kevin Buzzard said:

The short answer is that there isn't, and in the FLT project I am dealing with this by bumping every week or so and if something goes wrong then the changes tend to be fresh in the community's mind so it's not hard to find someone who can fix the problem for you. I agree that this is not ideal, but with lean still in a period of very dynamic development and mathlib not able to promise any backwards compatibility for this and other reasons, that's how things work right now.

This is helpful to know. Thank you so much for explaining.

[Roozbeh Yousefzadeh]

Often, the compiler shows some messages that some lemma is deprecated and it should be replaced with some other lemma. Would it be helpful for people if I write a script that reads those messages and tries to replace those lemmas automatically? I understand this might not resolve all the issues that might arise when upgrading the Mathlib version.

[Edison Xie]

Kevin Buzzard said:

bumping every week or so

and if you don't bump mathlib for more than a month, depending on the amount of code you had you might find yourself in some deep trouble :-(

[Anne Baanen]

I should mention the lean-update action which you can set up to run at regular intervals. This will try to do the update for you and depending on whether it succeeded without changes, you can choose between merge the new version, making a pull request or creating an issue in the repository.

[Michael Rothgang]

Roozbeh Yousefzadeh said:

Often, the compiler shows some messages that some lemma is deprecated and it should be replaced with some other lemma. Would it be helpful for people if I write a script that reads those messages and tries to replace those lemmas automatically? I understand this might not resolve all the issues that might arise when upgrading the Mathlib version.

I think such code already exists: @Damiano Testa had a prototype for this at https://github.com/adomani/UpdateDeprecations. See this thread for further discussion.

[Roozbeh Yousefzadeh]

Thank you everyone for your helpful comments and suggestions. I appreciate it.