improve new "sledgehammer_filter" action

remove useless var

added evaluation method for relevance filter

remove needless parameter

bring Sledgehammer's combinators in line with Metis's; cf. email from Larry

fiddle with the relevance filter

moved Toplevel.run_command to Pure/PIDE/document.ML; eliminated aliases of exception Toplevel.TERMINATE and Toplevel.EXCURSION_FAIL; tuned signatures;

Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body; Position.Id_Range convenience;

tuned;

Node.full_index: allow command spans larger than block_size;

Document_View: repaint overview for any command change of this node (again);

refined proper_line_range (again), to make text_area_extension work with soft wwrap; NB: text_area.offsetToXY returns null for "invisible" positions;

Document state assignment indicates command change;

tuned commands_changed_actor: more precise/efficient handling of visible screen lines;

simplified/clarified Document_View.text_area_extension; tuned Document.Node.block_size, trading some space for better time;

Document.Node: significant speedup of command_range etc. via lazy full_index;

text_edits/recover_spans: reparse at least until line boundary -- increases chance of recovery for bad ML text, for example;

Command.newlines: account for physical newlines;

Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.; simplified Toplevel.error_msg;

tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);

more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;

tuned;

Command.results: ordered by serial number;

message serial number indicates physical order;

tuned;

tuned;

merged

what is hidden is hidden

hide all-too-popular constant name eq

merged

formerly unnamed infix equality now named HOL.eq

code checking: compiler invocation happens in same directory as generated file -- avoid problem with different path representations on cygwin

Quotient Package: dont unfold mem_def, use rsp and prs instead

Quotient Package: added respectfulness and preservation lemmas for mem.

quotient package: added a list of pre-simplification rules for Ball, Bex and mem

quotient package: lemmas to be lifted and descended can be pre-simplified

merged

renamed class/constant eq to equal; tuned some instantiations

improved deresolving of implicits

Document_View.text_area_extension: do not insist in crashing if (weak) assertion is violated;

Isabelle/jEdit property for global tooltip dismiss delay;

External_Hyperlink: proper error dialog;

Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;

JEDIT_JAVA_OPTIONS: actors.enableForkJoin=false is supposed to enable ResizableThreadPoolScheduler, to avoid starvation of excessive amounts of future tasks etc.;

session_actor: ignore spurious TIMEOUT (again) -- probably stemming from earlier use of receiveWithin;

session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;

use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled; clarified session signalling;

Swing_Thread.now: volatile result to make double-sure;

Document_Model.token_marker: misc tuning and simplification;

added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.; Markup_Tree.select: plain Iterator; misc tuning and simplification;

XML.Cache: intern property keys once and for all (again);

more careful locking of jEdit buffer;

avoid application crash due to wrong requirement -- result is joined, but change not necessarily finished due to extra map;

include Document.History in Document.State -- just one universal session state maintained by main actor; Session.command_change_buffer: thread actor ensures asynchronous dispatch; misc tuning;

volatile variables (in Scala);

non-critical output primitives -- depending on thread-safe TextIO, while races wrt. flushing should not matter;

modernized specifications;

discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;

discontinued broken no_warnings_CRITICAL -- global output channels must not be changed after startup initialization;

eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job; modernized attribute setup;

more careful treatment of context visibility flag wrt. spurious warnings; misc tuning;

eliminated obsolete Output.no_warnings, where no warnings were produced anyway;

eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job;

more careful treatment of context visibility flag wrt. spurious warnings;

merged

merged

turn off experimental feature per default + avoid exception on "theory constant"

extended relevance filter with first-order term matching

drop chained facts

rename and simplify

cosmetics

renaming + treat "TFree" better in "pattern_for_type"

fix threshold computation + remove "op =" from relevant constants

avoid needless "that" fact

add nameless chained facts to the pool of things known to Sledgehammer

if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem

improve SPASS hack, when a clause comes from several facts

fix Vampire version numbers

lower penalty for Skolem constants

merged

official support for Scala

updated generated files

tuned whitespace

more xsymbols

re-added accidental omission

proper namespace administration for hierarchical modules

more antiquotations;

eliminated Unsynchronized.ref in favour of configuration option; proper naming of thy: theory vs. ctxt: Proof.context; recovered some Isabelle/ML indendation style;

more appropriate name for configuration option "meson_max_clauses" (cf. output of 'pront_configs');

Sum_Of_Squares: proper configuration options;

tuned printed type names, according to ML;

eliminated unnecessary ref;

clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;

disposed some old debugging tools;

proper configuration option "show_proofs"; modernized syntax translation;

structure Unsynchronized is never opened and set/reset/toggle have been discontinued; retain Unsynchronized.change alias for Proof General;

expanded some aliases from structure Unsynchronized;

merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;

merged

formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj

tuned fact reference

merged

added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory

adapted examples; tuned

moving options; tuned

added generation of predicates for size-limited enumeration of values

NEWS

merged

formerly unnamed infix impliciation now named HOL.implies

merged

proper passing of optional module name

For sublocale it is sufficient to reconsider ancestors of the target.

only print qualified implicits

merged

stub for (later) correct deresolving of class method names

tuned serializer interface

private version of commas, cf. printmode

merged

merged

re-added accidental omission

tuned includes

prevent line breaks after Scala symbolic operators

corrected semantics of presentation_stmt_names; do not print includes on presentation selection

code_include Scala: qualify module nmae

merged

preliminary implementation of hierarchical module name space

tuned

proper context for various Thy_Output options, via official configuration options in ML and Isar;

Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);

eliminated old 'local' command;

more uniform descriptions, which end up in the collective output of 'print_attributes' for example;

Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;

slightly more abstract data handling in Fast_Lin_Arith;

theory data merge: prefer left side uniformly;

tuned;

simplification/standardization of some theory data;

misc tuning and simplification, notably theory data;

renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;

renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;

standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;

merged

merged

consider "locality" when assigning weights to facts

add a bonus for chained facts, since they are likely to be relevant; (especially in a Mirabelle run!) -- chained facts used to be included forcibly, then were treated as any other fact; the current approach seems more flexible

merged

add a penalty for lambda-abstractions; the penalty will kick in only when the goal contains no lambdas, in which case Sledgehammer previously totally disallowed any higher-order construct; this was too drastic; lambdas are dangerous because they rapidly lead to unsound proofs; e.g. COMBI_def COMBS_def not_Cons_self2 with explicit_apply

renaming

fiddle with relevance filter

update docs

reorganize options regarding to the relevance threshold and decay

make relevance filter work in term of a "max_relevant" option + use Vampire SOS; "max_relevant" is more reliable than "max_relevant_per_iter"; also made sure that the option is monotone -- larger values should lead to more axioms -- which wasn't always the case before; SOS for Vampire makes a difference of about 3% (i.e. 3% more proofs are found)

simplify more code

cosmetics

get rid of "defs_relevant" feature; nobody uses it and it works poorly

make SML/NJ happy

renamed "relevance_convergence" to "relevance_decay"

make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts

better workaround for E's off-by-one-second issue

merged

renaming variables to conform to prolog names

changing hotel trace definition; adding simple handling of numerals on natural numbers

added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system

moving preprocessing to values in prolog generation

invocation of values for prolog execution does not require invocation of code_pred anymore

adding hotel keycard example for prolog generation

improving output of set comprehensions; adding style_check flags

improving ensure_groundness in prolog generation; added further example

adding very basic transformation to ensure groundness before negations

Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;

tuned signature;

Pretty: tuned markup objects;

tuned;

organized markup properties via apply/unapply patterns;

added some proof state markup, notably number of subgoals (e.g. for indentation); tuned;

ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;

merged

tuned code

quotient package: deal correctly with frees in lifted theorems

approximation_oracle: actually match true/false in ML, not arbitrary values;

renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;

more precise Command.State accumulation;

eliminated some old camel case stuff;

some attempts to recover Isabelle/ML style from the depths of time;

keep persistent production tables as immutable vectors -- potential performance improvement on modern hardware;

select tangible text ranges here -- more robust against ongoing changes of the markup query model

structure Thm: less pervasive names;

discontinued obsolete 'global' and 'local' commands;

merged

merged

moved generic lemmas in Probability to HOL

merged

traling newline on standard output

Quotient Package / lemma for regularization of bex1_rel for equivalence relations

merged

make Mirabelle happy

compute names lazily; there's no point to compute the names of 10000 facts when only 500 are used

clean handling of whether a fact is chained or not; more elegant and reliable than encoding it in the name

don't backtick facts that contain schematic variables, since this doesn't work (for some reason)

quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")

revert this idea of automatically invoking "metisFT" when "metis" fails; there are very few good reasons why "metisFT" should succeed when "metis" fails, and "metisFT" tends to "diverge" more often than "metis -- furthermore the exception handling code wasn't working properly

use matching of types than just equality - this is needed in nominal to cope with type variables

merge

cosmetics

use a soft time limit for E with a hard limit, "eproof"/"eproof.pl" doesn't show the proof is there's less than 1 second left, yielding "the ATP output is malformed"

make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version

cosmetics

optimize fact filter some more

cache previous iteration's weights, and keep track of what's dirty and what's clean; this speeds up the relevance filter significantly

modified relevance filter

adjust fudge factors in the light of experiments

invert semantics of "relevance_convergence", to make it more intuitive

if no facts were selected on first iteration, try again with a lower threshold

weed out junk in relevance filter

no need for "eq" facts -- good old "=" is good enough for us

revert unintended change

destroy elim rules before checking for finite exhaustive facts

prevent double inclusion of the fact "True_or_False" in TPTP problems

merged

tuned

merged

dropped pre_post_conv

use conv alias

preliminary versions of static_eval_conv(_simple)

use Code_Thingol.static_eval_conv_simple