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



Hi,

I'm using try0 very often. I only use nitpick if I don't trust my
lemma.

My typical sequence to find a proof to some lemma, which is simple
enough such that I can hope for a few lines apply script, goes as
follows:

unfolding relevant-defs
auto simp: relevant-simps
ALLGOALS (try0 or sledgehammer)


One feature that I miss most here would be a sledgehammer configuration
that saves resources while focusing on proof-finding, i.e., when the
first prover has found a proof, suspend the other provers and try proof
reconstruction. When a proof reconstruction is found, terminate and
don't use up resources any more.

This configuration would be beneficial when sledgehammer is run on many
goals in parallel, in my case, the many VCs that a verification
condition generator has left over.

For better usability, it could be combined with a sledgehammer
(allgoals) option, to prevent the current

  subgoal sledgehammer sorry
  subgoal sledgehammer sorry
  ...
  subgoal sledgehammer sorry

boilerplate.

I have requested this feature already two years ago

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2018-February/msg00043.html

but only got a solution proposal that worked on an unofficial branch of
Isabelle.

--
  Peter




On Tue, 2020-05-26 at 12:29 +0200, Jasmin Blanchette via Cl-isabelle-
users 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.