Re: [isabelle] Any fans of "try"?



As a relative novice, I use "try" a lot, especially for Eugene Stark's
reason-2: it teaches me what the various solvers are good at. I also happen
to like "nitpick," not so much because it finds errors in my theorems, but
because it finds errors in the way I've *stated* my theorems; they way we
write things in Isabelle is rather a lot like the way we write things in
mathematics, but not completely, and Nitpick often warns me that I've
tumbled into another of the rough spots.

Another note in praise of nitpick: in doing some work in synthetic affine
and projective geometry, I wanted to exhibit a four-point affine plane. To
do so required writing out the incidence relation (which points are on
which lines), which was a case-by-case nightmare to write and read. But
when instead I asked "try" to prove the theorem that every affine plane
contains at least 5 points, nitpick instantly generated the standard
4-point affine plane for me. That's kind of a backwards approach, but it
was, as I say, very useful.





On Tue, May 26, 2020 at 6:29 AM Jasmin Blanchette via Cl-isabelle-users <
cl-isabelle-users at lists.cam.ac.uk> wrote:

> Dear all,
>
> The "try0" and "try" commands were introduced to give an easy way to try
> out various tactics and tools. "try0" only applies a selection of tactics,
> whereas "try" additionally runs "solve_direct", Quickcheck, and reduced
> versions of Nitpick and Sledgehammer.
>
> I know people use "try0", including some experts, but I'm trying to find
> out whether "try" is used. The feedback I have about it, as well as my own
> impression, is that it just uses too much CPU at the same time to be
> useful, making the machine overheat. Also, because Nitpick and Sledgehammer
> are not the real thing, after a failed "try" one might still want to run
> them (esp. Sledgehammer), so "try" is not helping much. Finally,
> "solve_direct" and Auto Quickcheck are run by default, and you can also
> enable Auto Nitpick (which I've done for years), so in the end, "try" is
> really just "try0 + reduced Sledgehammer + lots of heat".
>
> My proposal:
>
> 1. Remove the "try" command.
>
> 2. Rename "try0" to "try".
>
> 3. (Maybe?) Enable Auto Nitpick.
>
> (Auto Nitpick is a reduced version of Nitpick that doesn't take that much
> CPU and won't run for more than 5 s. It's useful on nonexecutable
> conjectures like "hd [] = 0" and other problems with an axiomatic flavor.)
>
> Any opinions?
>
> Jasmin
>
>
>



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