Email Gateway (Nov 15 2021 at 11:09): Email Gateway (Nov 15 2021 at 11:09):From: Alex Weisberger <alex.m.weisberger@gmail.com>
Hi everyone,
quickcheck and nitpick provide great feedback within the jedit IDE. Using
"isabelle build" to build a theory containing one of these commands doesn't
work, however. It's possible that I'm doing something wrong, but it seems
like a theory is invalid if it contains one of these commands. Is this true
This would make sense, since the goal is a checked proof after all. Still,
it is convenient to see these counterexamples sometimes, and seeing them
from the command line would be nice.
Does anyone have any useful information regarding this? Thanks.
Email Gateway (Nov 15 2021 at 12:15):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
You can find how quickcheck is sanity-checked in this theory file in
the repository:
It might not fit exactly to your use case, but it might be a good
starting point on how to continuously check for a counterexample in a
theory. Also, there are some more theory files in the same directory
with some more examples.
Lukas
Email Gateway (Nov 28 2021 at 00:03):From: Alex Weisberger <alex.m.weisberger@gmail.com>
There are examples in the theory that you posted that do what I'm looking
for, specifically:
quickcheck[expect = no_counterexample]
will cause the isabelle build command to fail if a counterexample is
found. It would be nice if the actual counterexample was printed in this
case, but the command failing is still good.
Last updated: Jan 04 2025 at 20:18 UTC