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 12:10 PM Alex Weisberger
<alex.m.weisberger at gmail.com> 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
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