> Am 27.11.2014 um 00:06 schrieb Gerwin Klein <gerwin.kl...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
