[isabelle-dev] Feedback from a Isabelle tutorial

[Jasmin Christian Blanchette]

Am 24.06.2011 um 11:32 schrieb Lukas Bulwahn:

> I only noticed that using "try" you often get a misleading response from linarith that "linarith found a counterexample" which beginners might stumble on.
> It might be better to switch off this warning by default (and offer a configuration to switch it on if it is of interest).

I totally agree "try", actually "try_methods", should be silent or succeed, following the Unix tradition. We should add an "linarith_verbose" or "arith_verbose" configuration option to control verbosity, as we have for other tools (e.g. Metis). Whether it's on or off by default isn't for me to decide (I'd vote for "off" unless arith can be sure the counterexample is valid, as it probably could in some cases), but it would be off when "try" is run.

Now, this all sounds well and good, but there is a little glitch. In "try_methods.ML"  the line

    val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)

is meant to tell Metis to be quiet, but somehow it is ignored. If you do

    lemma "map f [] = []"
    using map.simps
    try_methods

you get the warning

    ### Metis: Unused theorems: "List.map.simps_2"

which is strange because in Metis's code that warning is only printed if "verbose" is true. Is "Proof.map_context" not the thing I should be using?

Jasmin