Strip trailing spaces from informal descriptions

[eric-wieser]

The changes to putnam.json are the result of a regex replace for \s*\\n with \\n.
These trailing spaces are stripped in the Lean docstrings by VSCode, which previously caused CI to invisibly fail when editing one of these "booby-trapped" files.

If changing the JSON file is not desirable, I can teach the CI script to remove the trailing spaces before comparison instead.

[amit9oct]

This can be avoided just by checking the commit. The space was visible in PR clearly. It is possible that the logic for ignoring trailing spaces is needed in some corner case where we want to have trailing spaces in the informal description. The PR author can simply check the PR for spaces. I'm not sure if it is a great idea to complicate the validation check/CI logic for PRs.

[amit9oct]

These spaces would have been visible even before commit using git diff. One can also change VS code settings.

[eric-wieser]

[...] in some corner case where we want to have trailing spaces in the informal description

I claim that no such situation exists; no reasonable dialect of LaTeX is sensitive to trailing spaces, and all of this text is LaTeX source.

These spaces would have been visible even before commit using git diff.

in the case of #234, there are >600 files, so this it not terribly viable.

One can also change VS code settings.

Either the trailing spaces should be stripped from the lean files in this repo, or the repo should come with config saying "don't strip trailing spaces". I claim that the first option is better, since there is no good reason to keep trailing spaces in the lean files.

[amit9oct]

[...] in some corner case where we want to have trailing spaces in the informal description

I claim that no such situation exists; no reasonable dialect of LaTeX is sensitive to trailing spaces, and all of this text is LaTeX source.

I don't know if your claim covers all corner cases for example someone using pre formatted mode in LaTeX and some other cases which of course you and I are not able to anticipate now.

These spaces would have been visible even before commit using git diff.

in the case of #234, there are >600 files, so this it not terribly viable.

As per your comment on PR 216(#216) you mentioned that one can use git checkout -p. I pointed similar issues, but since only a few people are contributing so it can be handled by changing the VS Code config too.

In my opinion, the right way to do this have only one source of truth and use your script before merge to populate the comments directly in the Lean files. Otherwise accidental changes, difference in editor configs will lead to issues, or something which you cannot anticipate now will break the CI.

A much better solution rather than this complicated validation strategy is change the informal json to precisely match the comment. The easy fix will be to match the informal json to strip terminal spaces, this will keep check simple and easy for anyone editing these files. We will be robust with VS Code settings. The validation in CI will be simple and intuitive rather than some complicated regex match.

[eric-wieser]

The easy fix will be to match the informal json to strip terminal spaces

Is this not precisely what the PR we are writing comments on already does?

[amit9oct]

If changing the JSON file is not desirable, I can teach the CI script to remove the trailing spaces before comparison instead.

My comments are about this.

[GeorgeTsoukalas]

There seems to be agreement that this PR is the right way to go. Thanks for the contribution, Eric!