Negative use cases database?

[Samuel Goto]

Hey all,

    I'm wondering: is there any chance anyone has built a list of proofs that are expected to fail to check verifiers?

    Context: as I'm trying to verify some of the disjoint variable restrictions, I'm finding that I'm missing a lot of corner cases I missed from the book/specification, and when I do, verifications succeeds rather than fails, and I have to manually catch those bugs. So, if I'm thinking that if had a list of proofs that have known bugs (for the $d statement specifically, but more generally too) that a valid verifier would successfully catch, I'd feel more comfortable knowing that I've captured known ways a proof is invalid.

    Anyone?

    Sam

[Mario Carneiro]

The only source I am aware of is https://github.com/david-a-wheeler/metamath-test and the metamath-exe test suite (https://github.com/metamath/metamath-exe/tree/master/tests). Collecting failing tests and serving as a unit test for new verifiers is part of the stated purpose of the former repository, so perhaps that answers your question.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/63400cee-5e0e-4b16-9c80-fc4ed8b430ddn%40googlegroups.com.

[Jim Kingdon]

When I wrote

* https://github.com/metamath/metamath-exe/blob/master/tests/disjoint1.expected

* https://github.com/metamath/metamath-exe/blob/master/tests/disjoint2.expected

* https://github.com/metamath/metamath-exe/blob/master/tests/disjoint3.expected

I thought there would be a lot more cases, but I wasn't sure what else to add.

Perhaps if you are working on a verifier you can find some cases I missed there.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvY-oggjiATKMa5Co7OukNb5nQSS3PUKp1wqytxFeLBsw%40mail.gmail.com.

[Glauco]

Hi Sam,

here

https://github.com/glacode/yamma/blob/master/server/src/__test__/DisjointVarsManager.test.ts

you can find 4 unit tests I use for yamma (a mmj2 alternative).

The first two tests are for a disj var violation (very bad)

The third test is ok (skip it).

The fourth test is for a missing $d constraint (bad, but easy to fix)

(I wrote them quite some time ago, I don't remember if I copied them from other sources, or I wrote them from scratch)

HTH

Glauco