PR which changes nothing is generated

oliver-butterley / lean-update

The action attempts to update Lean and Mathlib. If an update is available then the updated version is tested. This allows for automatic committing of the updated project, opening PRs or opening issues.

MIT License

6 stars 2 forks source link

PR which changes nothing is generated #2

Closed Seasawher closed 4 months ago

Seasawher commented 4 months ago

Thank you for creating nice action!

I tried this for my repository https://github.com/Seasawher/mathlib4-tactics

but generated PR changes nothing. see https://github.com/Seasawher/mathlib4-tactics/pull/4

Can the creation of a PR be skipped if there are no changes?

oliver-butterley commented 4 months ago

When the action ran the mathlib post-update hook updated lean-toolchain. However the only change to the file was a white space change as can be seen in the images of the hex views of the two versions of the file. The difference between \n and \r\n.

However the action saw that the file had changed and then proceeded believing this was an update and consequently the pointless PR was created.

Screenshot from 2024-05-10 16-43-57

oliver-butterley commented 4 months ago

Obviously this isn't ideal! In terms of solutions to this issue, there are some options:

A workaround is just to merge this PR and then the same problem can't happen again unless lean-toolchain is manually edited. I believe lake + mathlib are consistent with the formatting.
Update the part of the action which detects which files have changed in order to ignore any white space. Probably worth doing and not much effort. However I've noticed that the update to lean-toolchain isn't consistent at the moment so would be better to change the functioning of the action: firstly it checks what versions of lean are available and then sets lean-toolchain to the latest (or latest stable). Then it uses lake to update dependencies.

Seasawher commented 4 months ago

Thank you. I tried changing EOL to LF and it works as expected.

Seasawher commented 4 months ago

Update the part of the action which detects which files have changed in order to ignore any white space. Probably worth doing and not much effort.

It sounds good to me.

oliver-butterley commented 4 months ago

In PR #4 the code is updated so that it ignores white space when comparing files.

Generally I'm noticing that there isn't a clear best way to update a lean project using mathlib. The code executed here is the best that I can see for the moment. I was going to avoid further polishing the action until the desired behaviour becomes clear.