Re: [isabelle] Commandline results for quickcheck / nitpick

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.

On Mon, Nov 15, 2021 at 7:15 AM Lukas Bulwahn <lukas.bulwahn at> wrote:
On Mon, Nov 15, 2021 at 12:10 PM Alex Weisberger
<alex.m.weisberger at> wrote:
> 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 - are they only for interaction purposes, not to count as results of the theory?
> 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.

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.