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.
On 3/10/23 14:16, Mario Carneiro wrote:
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.
On Fri, Mar 10, 2023 at 5:00 PM Samuel Goto <[email protected]> wrote:
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
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/63400cee-5e0e-4b16-9c80-fc4ed8b430ddn%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/63400cee-5e0e-4b16-9c80-fc4ed8b430ddn%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSvY-oggjiATKMa5Co7OukNb5nQSS3PUKp1wqytxFeLBsw%40mail.gmail.com
<https://groups.google.com/d/msgid/metamath/CAFXXJSvY-oggjiATKMa5Co7OukNb5nQSS3PUKp1wqytxFeLBsw%40mail.gmail.com?utm_medium=email&utm_source=footer>.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/005e5868-20d1-fff5-4aa1-589c11d35cac%40panix.com.
