[isabelle] Any fans of "try"?

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?


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