search

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

expose ProofTreePrinter, make enable_exprs optional #94

Closed digama0 closed 1 year ago

digama0 commented 1 year ago

This makes it possible to disable expr collection inside ProofTreeArray, which is not required when the goal is to build a compressed proof. It also exposes ProofTreePrinter (although possibly the API could use some work) so that it is possible to generate compressed proofs without going through MMP. Eventually it would be nice to have a proof editing interface like metamath.exe's save proof; I already have some use cases for that but probably won't be able to get to it soon.

david-a-wheeler commented 1 year ago

The Ubuntu 18.04 tests can't be rerun due to a "scheduled Ubuntu-18.04 brownout." This is intentional; the Ubuntu-18.04 environment is deprecated and will be removed on April 1st, 2023. GitHub is intentionally making it "not work" sometimes so people will notice it's going away. For more details, see https://github.com/actions/runner-images/issues/6002

So the 18.04 failures should be ignored, and we should remove 18.04 in a separate PR.

tirix commented 1 year ago

GitHub is intentionally making it "not work" sometimes

I actually never got it to pass, even after several trials. Anyway, I'll merge this PR, since the issue here is obviously Ubuntu.