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

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

make Mirabelle happy

added Auto Sledgehammer docs

change order of default ATPs; put SPASS first so that it's picked up by Auto Sledgehammer

implemented Auto Sledgehammer

document changes to Auto Nitpick

change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)

always handle type variables in typedefs as global

removed duplicate lemma

adding two more examples to example theory

handling function types more carefully than in e98a06145530

adding order on modes

removing obsolete argument in prepare_intrs; passing context instead of theory in prepare_intrs

type antiquotation: allow arbitrary type abbreviations, but fail with user-space exception on bad input

merged

added Imperative HOL overview

print mode for Imperative HOL overview; tuned and more accurate dependencies

'class' and 'type' are now antiquoations by default

merged

merged

renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI

added and renamed lemmas

merged

directly computing the values of interest instead of composing functions in an unintelligent way that causes exponential much garbage; using the latest theory

added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet

use eta-contracted version for occurrence check (avoids possible non-termination) Test case: lemma "fwrap f = (%v. f v) ==> P f" apply clarify; pointed out by Thomas Sewell

tuned signature; tuned comments;

Type_Infer.finish: index 0 -- freshness supposedly via Name.invents; Type_Infer.fixate_params: full Proof.context;

simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;

tuned;

Type_Infer.preterm: eliminated separate Constraint;

Type_Infer.infer_types: plain error instead of kernel exception TYPE;

load type_infer.ML later -- proper context for Type_Infer.infer_types; renamed Type_Infer.polymorphicT to Type.mark_polymorphic;

common Type.appl_error, which also covers explicit constraints;

eliminated aliases of Type.constraint;

tuned;

tuned messages; tuned comments;

avoid extra wrapping for interrupts;