metamath / metamath-knife

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.
Apache License 2.0
25 stars 9 forks source link

Option to print the grammar #101

Closed benjub closed 1 year ago

benjub commented 1 year ago

Example:

~/Documents/_metamath/git/metamath-knife (main) $ target/release/metamath-knife -G ../set.mm/iset.mm
0 diagnostics issued.
thread 'main' panicked at 'The database has not run `grammar_pass()`. Please ensure it is run before calling depdending methods.', src/database.rs:660:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

First, there is a typo in "depdending" and second, maybe the -G option could automatically trigger the -g option before it ? (though this may have other implications I do not know about)

david-a-wheeler commented 1 year ago

Yes, -G should trigger -g, otherwise it just fails. I've been bit by that myself.