merged

established emerging canonical names *_eqI and *_eq_iff

moved lemmas map_of_eqI and map_of_eq_dom to Map.thy

more precise name for activation of improveable syntax

tuning

tuning

prefer version 0.6 of Vampire, now that we can parse its output

fix splitting of proof lines for one-line metis calls; needed for newly supported ATPs (Vampire 0.6 local and remote, SNARK)

finish support for E 1.2 proof reconstruction; this involves picking up the axiom and conjecture names specified using a "file" annotation in the TSTP file, since we cannot rely anymore on formula numbers (E 1.2 adds a strange offset)

first step in generalizing to nonnumeric proof step names (e.g. remote Vampire 0.6)

clarify message

use same hack as in "Async_Manager" to work around Proof General bug

export function

generalize proof reconstruction code; first step towards support for nonnumeric formula names, needed for E 1.2

tuning

handle relevance filter corner cases more gracefully; e.g. the minimizer selects 15 facts but "max_relevant = 14"

remove more clutter related to old "fast_descrs" optimization

Sledgehammer should be called in "prove" mode; otherwise the proof text won't fit into the proof document

added a timeout around "try" call in Mirabelle

adapt examples to latest Nitpick changes + speed them up a little bit

tuning

eliminate more clutter related to "fast_descrs" optimization

remove "fast_descs" option from Nitpick; the option has been unsound for over a year and is too imprecise to be of any use when made sound

fixed bug in the "fast_descrs" optimization; the bug is that two sets may actually be the same but because of the three-valued logic a different "The" or "Eps" is chosen; e.g. consider the set {1, 2}. If it is approximated in one place as {1, 2?} and in another place as {1?, 2}, then "Eps" would return 1 in the first case and 2 in the second case. This is of course wrong, because both sets potentially represent {1, 2}. The current fix has a very negative impact on precision.

speed up helper function

tuning

rename internal Sledgehammer constant

merged

merged

adapt to latest Metis version

regenerated "metis.ML" and reintroduced Larry's old hacks manually; see comment at head of file

update scripts

change license, with Joe Hurd's permission

new version of the Metis files

remove old sources

remove "atoms" from the list of options with default values

remove unreferenced identifiers

make Auto Nitpick go through fewer scopes

move equation up where it's not ignored

correctly thread parameter through

indicate triviality in the list of proved things

indicate which goals are trivial

tuning

tuning

keep track of trivial vs. nontrivial calls using "try" for 30 seconds

change signature of "Try.invoke_try" to make it more flexible

use 30 s instead of 60 s as the default Sledgehammer timeout; very few proofs are lost this way (esp. thanks to the parallel use of provers, cf. Boehme & Nipkow 2010), and this is much more tolerable for users

no timeout for Auto Try, since the Auto Tools framework takes care of timeouts

add Proof General option

make Try's output more concise

added Auto Try to the mix of automatic tools

crank up Auto Tools timeout; instead of 2500 ms (for Auto Solve) + 2500 ms (for Auto Quickcheck/Nitpick), have 4000 ms as the cumulative timeout

make Auto Solve part of the "Auto Tools"

tuning

tuning

tuning

tuning

finished renaming "Auto_Counterexample" to "Auto_Tools"

start renaming "Auto_Counterexample" to "Auto_Tools"; Auto Sledgehammer now uses so the name is clearly wrong

setup Auto Sledgehammer