Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Commandline results for quickcheck / nitpick


view this post on Zulip 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.

view this post on Zulip 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:

https://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy

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

view this post on Zulip 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: Jul 15 2022 at 23:21 UTC