[isabelle-dev] Abbreviations and find_theorems

[Gerwin Klein]

> Am 27.11.2014 um 00:06 schrieb Gerwin Klein <gerwin.klein at nicta.com.au>:
> 
>> I wonder if it would be feasible to create a regression test for interactive commands like find_theorems so this noticed earlier, but that is a different topic.
> 
> We have regression tests for a number of other interactive diagnosis commands -- I'm aware of "nitpick", "quickcheck", and "sledgehammer", and there might be others. For these, it's done simply by adding an option to the command to specify the expected result, e.g.
> 
>    sledgehammer [expect = some]
> 
> (where "some" means "some proof"). Something like that could surely be done for "find_theorems", if there's enough willpower. ;)

The problem is mostly in what to specify for ‘expect’.

find_theorems depends heavily on context (that is its point), so its results are expected to change over time. I.e. specifying the full expected result of a search is not going to be stable for more than a week.

We could add something like ‘expect [factref list]’ (with semantics ‘at least these’) and ‘expect not [factref list]’ (with semantics 'should not match these’) and try to choose examples that we think will be stable over time. I guess that would work.

Now for that willpower..

Cheers,
Gerwin