Add script for metamath-knife verification

[BTernaryTau]

• Create a new verify-knife script for quick verification using metamath-knife
• Update the verifiers workflow to use this script for set.mm and iset.mm, adding a couple new checks
  • Check that printing parsed statements gives back the original formulas
  • Check that the discouraged files are up to date
• Automatically fix line endings during a commit (working directories should be unaffected)

[tirix]

Looks good to me.
If we perform the "Discouraged" check using metamath-knife, do we still need the MMJ2 one?

[benjub]

Why default it to false if the first usage we're making of it is to pass it to true ?

@tirix : I don't see --check-newlines documented on https://github.com/metamath/metamath-knife ?

(If I ask these questions, it's because I may soon try and switch to it!)

[digama0]

--check-newlines is not an option to metamath-knife, it is handled directly in this script, passing the -Z option to diff below when testing the discouraged file.

[benjub]

Oh, thanks. I see in the man page of diff:

-Z, --ignore-trailing-space

So wouldn't it be clearer to use --ignore-trailing-space both in place of -Z in the script, and as the name of the script option ? (so that by default, it is not passed)

[digama0]

I think we should just not use that option, I don't see a need to have an option to allow it

[BTernaryTau]

This script originally started out as a convenience feature just for myself, so I set it up so that I could just run scripts/verify-knife with no extra options while I'm working on set.mm. Because of how my environment is currently configured I sometimes end up with different newlines, which generally isn't a problem since git usually corrects it. But it doesn't do this by default for new files, hence the .gitattributes change, and it won't do anything if I haven't made a commit yet. So when I didn't include the -Z, the script would report that the discouraged file needed to be regenerated even though it was fine. Thus I made ignoring trailing whitespace the default since it should very rarely cause an issue.

But after deciding that this script would be worth adding to the verifiers workflow, I figured I should add the option to check the trailing whitespace so that any issues there would be caught. I tried to keep the flag a bit shorter by calling it --check-newlines instead of --check-trailing-whitespace, but that name could certainly be changed.

I would, however, object to both eliminating the option entirely and to just switching the default behavior, unless there's a consensus that we want to enforce LF line endings within working directories as well as the repository itself. If such a consensus does exist, I would be happy with updating .gitattributes to use * text eol=lf, always checking trailing whitespace in the script, and figuring out how to configure things on my end so my local edits use the right newlines. But I didn't want to make such changes unilaterally, so I went with a more conservative option here.

[jkingdon]

I guess the main thing I have an opinion on is that I'd want us to standardize on LF line endings within the git repository (which we already do, as far as I know).

My usual bias tends to be LF-only line endings in working directories too (yes, even on Windows, although different Windows editors/tools have varying ways of handling LF-only). But the more I read https://docs.github.com/en/get-started/getting-started-with-git/configuring-git-to-handle-line-endings the more I'm not really sure what I think (either in terms of what we have today, or what we'd get with various settings). At some point I'll defer to people more directly affected, assuming this is an issue on Windows and not on Linux.

[tirix]

While it used to be a real thing, I have not been bothered by line endings for years now. I guess everyone just uses LF-only, or the tools we use are clever enough. Or I don't work that much with PCs.

[icecream17]

I have on occasion happened upon this and extra whitespace, so I always do git diff before commits. Once my computer froze with 100% disk for a few minutes, but it's usually fine.

For me, the fix is as easy as dos2unix set.mm

Edit: medium edit

[BTernaryTau]

Since there seems to be support for standardizing on LF line endings in working directories, I've created #4219 as an alternative.

Once this PR or #4219 has been merged, the other one can simply be closed.