Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add script for metamath-knife verification #4209

Closed
wants to merge 3 commits into from
Closed

Add script for metamath-knife verification #4209

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c648200
Automatically fix line endings
BTernaryTau Sep 17, 2024
62c1fab
Create a script for verifying a file using metamath-knife
BTernaryTau Sep 17, 2024
6e4433f
Use metamath-knife to verify parsed statements and discouraged files
BTernaryTau Sep 17, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitattributes
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
* text=auto
16 changes: 4 additions & 12 deletions .github/workflows/verifiers.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -247,20 +247,12 @@ jobs:
git clone --depth 1 https://github.com/metamath/metamath-knife.git &&
cd metamath-knife &&
cargo build --release
- name : Update PATH
run: echo "metamath-knife/target/release" >> "$GITHUB_PATH"
- name: Verify set.mm
run: |
metamath-knife/target/release/metamath-knife --verify \
--verify-markup --parse-typesetting ./set.mm
run: scripts/verify-knife --check-newlines ./set.mm ./discouraged
- name: Verify iset.mm
run: |
metamath-knife/target/release/metamath-knife --verify \
--verify-markup --parse-typesetting ./iset.mm
- name: Check axiom usage for set.mm
run: |
metamath-knife/target/release/metamath-knife --verify-usage ./set.mm
- name: Check axiom usage for iset.mm
run: |
metamath-knife/target/release/metamath-knife --verify-usage ./iset.mm
run: scripts/verify-knife --check-newlines ./iset.mm ./iset-discouraged

###########################################################
mmj2:
Expand Down
42 changes: 42 additions & 0 deletions scripts/verify-knife
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
#!/bin/sh

# Verify mmfile $1 (default "set.mm") and discouraged file $2 (default
# "discouraged") using metamath-knife.
# Usage:
# verify-knife [--check-newlines] [source=set.mm] [discouraged_file=discouraged]

check_newlines='false'

if [ "$1" = '--check-newlines' ] ; then
check_newlines='true'
shift
fi
Comment on lines +6 to +13
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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!)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

--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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

@icecream17 icecream17 Sep 19, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


source="${1:-set.mm}"
discouraged_file="${2:-discouraged}"

metamath-knife ${source} --verify \
--verify-parse-stmt \
--verify-usage \
--verify-markup

if [ $? != 0 ]; then
exit 1
fi

metamath-knife ${source} -D discouraged.new >/dev/null

if [ "$check_newlines" = 'true' ]; then
diff ${discouraged_file} discouraged.new >/dev/null
else
diff -Z ${discouraged_file} discouraged.new >/dev/null
fi

if [ $? != 0 ]; then
echo "The file '${discouraged_file}' needs regenerated."
rm discouraged.new
exit 1
fi

rm discouraged.new
exit 0
Loading