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 gmail.com> wrote:
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
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


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