Re: [isabelle] Commandline results for quickcheck / nitpick

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.