handy little script

reintroduce missing "critical"s by hand

MIT license -> BSD License

copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle

tuned;

allow embedded reports in regular prover messages, to avoid side-effects for errors for example;

simplified/clarified (Context_)Position.markup/reported_text;

eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;

Isar "default" step needs to fail for solved problems, for clear distinction of '.' and '..' for example -- amending lapse introduced in 9de4d64eee3b (April 2004);

updated generated file;

tuned whitespace

reverse order of datatype declarations so that declarations only depend on already declared datatypes

merged

make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; instead, query the original "Makefile"

dropped obsolete src/Tools/random_word.ML -- superseded by src/Tools/Metis/src/Random.sml stemming from the Metis distribution;

merged

document Metis updating procedure

move "CRITICAL" to "PortableXxx", where it belongs and used to be; now that it is no longer used in "Random.sml"

regenerated "metis.ML"

update comment

make "Unprotected concurrency introduces some true randomness." be true; this code is called often and doesn't need to be considered critical. I added CRITICAL by mistake.

fix parsing of higher-order formulas; this code was never exercised before because the current ATPs perform clausification, but someday ATPs might support FOF natively

merged

load code_runtime immediately again

proper interface for code_reflect

introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy

merged

"Metis." -> "Metis_" to reflect change in "metis.ML"

no need for "metis_env.ML" anymore; it was a neat solution but it didn't work anymore once I removed the "structure Metis"

regenerate "metis.ML", this time without manual hacks

remove needless file for us

got rid of three crude regexps from "make_metis"

more Isabelle-specific changes

tuning

rename

use "Metis_" prefix rather than "Metis" structure; the prefix can then be used not only for structures but also signatures and functors. A few other changes were made to the script, to eliminate the need for "metis_env.ML".

no need for TPTP

put "foldl" and "foldr" in "Useful"; Isabelle hides those symbols from List, but by adding them to Useful we have them throughout Metis without "List." prefix

reintroduce the CRITICAL sections from change 3880d21d6013

apply Larry's hacks directly to the "src" files; these hacks modify the defaults of Metis heuristics and are necessary for backward compatibility

"FILES" is not (anymore?) part of the official Metis sources, so move it up

merged

Code_Runtime.value, corresponding to ML_Context.value; tuned

Code_Runtime.value, corresponding to ML_Context.value

more accurate dependencies

code_eval renamed to code_runtime

merged

static nbe conversion

ignore code cache optionally; corrected scope of term value in static_eval_conv

ignore code cache optionally

dropped redundant normal_form command

more explicit theory name

more accurate dependencies

merged

more clear separation of static compilation and dynamic evaluation

Document.async_state: some attempts to make this more robust wrt. cancelation of the main transaction -- avoid confusing feedback about pending forks;

isatest: reactivated kodkodi and thus HOL-Nitpick_Examples -- being now on a local file system greatly increases the chance that it works;

merged

replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references

replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures

merge

compile on SML/NJ

in debug mode, don't touch "$true" and "$false"

adding option show_invalid_clauses for a more detailed message when modes are not inferred

proposed modes for code_pred now supports modes for mutual predicates

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