metamath / metamath-knife

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

Fixing the running of export statements #111

Closed josojo closed 1 year ago

josojo commented 1 year ago

When I was trying to run an export statement, I was getting:


0 diagnostics issued.
thread 'main' panicked at 'The database has not run `name_pass()`. Please ensure it is run before calling depending methods.', src/database.rs:530:31
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

This PR fixes it.

Discussion: If you want to make a helper function that calls name_pass and scope_pass, I am happy to provide it.

Testplan: run an export command like:

cargo run ~/Downloads/metamath/set.mm --export fzval

and see that it runs through.