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;

tuned markup;

updated keywords;

proper antiquotations;

fixed antiquotation;

updated generated file;

updated config options;

removed spurious addition from 9e58f0499f57;

merged

improved error message for common mistake (fun f where "g x = ...")

adding another String.literal example

fiddling with the correct setup for String.literal

refactoring mode inference so that the theory is not changed in the mode inference procedure

Haskell == is infix, not infixl

more correct dependencies

merged

use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson

use the Meson cutoff as the cutoff for using definitional CNF -- it's simpler that way

clarify comment

improve on 65903ec4e8e8: fix more "add_ffpair" exceptions in failed ATP proofs

allow Sledgehammer proofs containing nameless local facts with schematic variables in them

tuning

more precise error messages when Vampire is interrupted or SPASS runs into an internal bug

better error reporting when the Sledgehammer minimizer is interrupted

add cutoff beyond which facts are handled using definitional CNF

"resurrected" a Metis proof

replace two slow "metis" proofs with faster proofs

workaround to avoid subtle "add_ffpairs" unification exception in Sledgehammer; to reproduce the old bug, replace the command by(rule new_Addr_SomeD) on line 27 of Jinja/J/TypeSafe.thy with by (metis new_Addr_SomeD)

improve SInE-E failure message

merged

adding an example with integers and String.literals

adding an example to show how code_pred must be invoked with locales

removing report from the arguments of the quickcheck functions and refering to it by picking it from the context

changing the container for the quickcheck options to a generic data

Tidied up proofs using sledgehammer, also deleting unnecessary semicolons

changing String.literal to a type instead of a datatype

increasing the number of iterations to ensure to find a counterexample by random generation

only conceal primitive definition theorems, not predicate names

merged

modernized primrec

Markup_Tree is already scalable;

Isabelle_Markup.tooltip: explicit indication of ML;

Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);

primitive use_text: let interrupts pass unhindered;

Isabelle.load_icon with some sanity checks;

ML_Compiler.eval: reported positions need to contain offset, to avoid displaced reports due to synthesized line numbers;

NEWS: some notes on interrupts;

refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;

removed dead code;

avoid handling interrupts in user code;

Meson.make_clauses_unsorted: removed spurious debug code stemming from 5146d640aa4a -- must not handle arbitrary exceptions in user space;

main command loops are supposed to be uninterruptible -- no special treatment here;

Exn.is_interrupt: include interrupts that have passed through the IO layer;

more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;

avoid mixing of static and runtime errors in compiler output, to accomodate Proof General; refrain from absorbing Exn.Interrupt, to accomodate asynchronous interaction; actually observe Isabelle/ML naming conventions in exception STATIC_ERRORS;

ML_Compiler.eval: discontinued extra "Static Errors" of raw Poly/ML;

isabelle-jedit.css: suppress "location" markup, which indicates extra positional information intended for plain-old TTY mode;

ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;

clarified -- inlined ML_Env.local_context;

merged

restricting invocation only if PROLOG_HOME is set

tuned proofs (based on fancy gutter icons in Isabelle/jEdit);

merge

remove "safe" (as suggested by Tobias) and added "arith" to "try"

remove "minipick" (the toy version of Nitpick) and some tests; a small step towards making the Nitpick tests take less time

use Future.fork rather than Thread.fork, so that the thread is part of the global thread management

fix editor

merged

merged

tidied using inductive_simps

NEWS

removed ancient constdefs command

put expand_(fun/set)_eq back in as synonyms, for compatibility

set up Nil and Cons to work as fixrec patterns

merged

updated generated document

only write ghc pragma when writing to a file

added flat_program; tuned signature

dropped ancient deresolve_base; plain_const_syntax also needs modification of instance statement

moved flat_program to code_namespace

dropped outdated substitution

Haskell uses generic flat_program combinator

factored out build_module_namespace

added generic flat_program procedure

using the proposed modes for starting the fixpoint iteration in the mode analysis

merged

renamed expand_*_eq in HOLCF as well

expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets

merged

lower expectation in Reg exp example

renewing specification in example file; adding invocation in example file

handling collection of simprules as sets rather than as lists

stating errors in error messages more verbose in predicate compiler

raising an exception instead of guessing some reasonable behaviour for this function

using linear find_least instead of sorting in the mode analysis of the predicate compiler

adding code attribute to definition of equality of finite sets for executability of equality of finite sets

adapting example files

adding the Reg_Exp example

towards time limiting the prolog execution

adding IMP quickcheck examples

adding the CFG example to the build process

adding a List example (challenge from Tobias) for counterexample search

adding dependencies to IsaMakefile; increasing negative search limit for predicate_compile_quickcheck; adding tracing of introduction rules in code_prolog

disposed some old TODO/FIXME;

Document_View: select gutter message icons from markup over line range, not full range results; tuned;

tuned properties;

moved token markup tables to isabelle_markup.scala;

concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;

simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default; tuned Snapshot.convert/revert;

Document_View: more precise painting of gutter icons, only if line selection area is sufficiently large;

basic support for warning/error gutter icons;

Document_View: some markup for main inner syntax categories;

Command.State.accumulate: check actual source range;

Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;

highlight bad range of nested error (here from inner parsing);

Isar_Document.reported_positions: exclude proof state output;

Document_View: less aggressive background coloring, departing from classic PG highlighting; tuned colors;

report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase; tuned color;

slightly more robust Plugin.stop -- components might refer to Isabelle.system even after shutdown;

turned show_hyps and show_tags into proper configuration option;

discontinued obsolete ProofContext.prems_limit; simplified command setup for 'pr' etc.;

ML_Context.thm and ML_Context.thms no longer pervasive;

more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;

merged

When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.

isatest: back to polyml-5.3.0 due to unresolved stability issues of polyml-5.4.0 and HOL/Decision_Procs/Approximation_Ex.thy;

more antiquotations;

ML_Context.thm;

more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);

modernized session ROOT setup;

some results of concurrency code inspection;

merged;

mention ~/.isabelle/etc/settings file

make remote ATP invocation work for those people who need to go through a proxy; thanks go to Mathieu G. for that fix

enabled do notation for option type

removed duplicate lemma

added Option.bind

merged

printing combinator for hierarchical programs

merged

add lemma cont2cont_Let_simple

add lemma cont2cont_split_simple

add List_Cpo.thy to HOLCF/Library

dropped names from serializer interface

added more explicit warning

ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;

use setmp_noncritical for PGIP, which is presumably sequential (PG clone);

use setmp_noncritical for sequential Pure bootstrap;

turned show_brackets into proper configuration option; Sign.certify/type_check: dropped Syntax.pp_show_brackets, which is hard to hold up due to Pretty.pp and not even present in the regular end-user type check;

Syntax.standard_parse_term: eliminated redundant Pretty.pp;

structure Syntax: define "interfaces" before actual implementations;

turned show_sorts/show_types into proper configuration options;

pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;

refined treatment of multi-line subexpressions;

basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);

updated configuration options;

recovered options for goal antiquotations from f45d332a90e3: actually pass context to Proof.pretty_goals (see also 45facd8f358e);

turned eta_contract into proper configuration option;

turned show_structs into proper configuration option;

configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;

pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;

tuned comment;

merged

merged

QND_FLAG is a shell variable, not a string

modernized session ROOT;

disposed left-over user preferences;

turned show_all_types into proper configuration option;

treat show_free_types as plain ML option, without the extras of global default and registration in the attribute name space -- NB: 'print_configs' only shows the latter;

more explicit Config.declare vs. Config.declare_global;

turned show_no_free_types into proper configuration option show_free_types, with flipped polarity;

remove code I submitted accidentally

merged

disable "definitional CNF"; it has a bad impact on "Metis_Examples". Perhaps we should use it more selectively, based on how many clauses we would get using the naive method

redisable Nitpick from Cygwin, until I've investigated the issue

show the number of facts for each prover in "verbose" mode

fix bug in "debug" mode

make sure "Unknown ATP" errors reach the users -- i.e. don't generate them from a thread

If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user

fix trivial "x = x" fact detection

merged

merged

merged

hand out deresolver from serializer invocation

Revert bij_betw changes to simp set (Problem in afp/Ordinals_and_Cardinals)

merged

Updated proofs in Dining Cryptographers theory

Corrected definition and hence removed sorry.

Moved lemmas to appropriate locations

merged

merged

measure unique

merge

move lemmas to correct theory files

factorizable measurable functions

Introduced sigma algebra generated by function preimages.

vimage of measurable function is a measure space

Measurable on product space is equiv. to measurable components

Measurable on euclidean space is equiv. to measurable components

preimages of open sets over continuous function are open

added definition of conditional expectation

proved existence of conditional expectation

introduced integration on subalgebras

changed definition of dynkin; replaces proofs by metis calles

dynkin

dynkin system

merged

Fixes lemma names

NEWS

Introduce surj_on and replace surj and bij by abbreviations.

Permutation implies bij function

bij <--> bij_betw

Add filter_remove1

Add lessThan_Suc_eq_insert_0

merged

updated

set printmode while marking

updated

avoid reference to theory Ferrack altogether

more canonical theory setup

set depth to 1

avoid theory Imperative_HOL altogether

adapted to change eq -> equal

corrected printmode handling

swapped slip

updated

restored and added surpression of case combinators

dropped superfluous presentation names

manage statement selection for presentation wholly through markup

formal markup of generated code for statements

removed namespace stuff from code_printer

merged

reenable Nitpick on Cygwin; we'll see tomorrow if there's still a failure, and if so I'll investigate

merged;

Proof.pretty_state: print everything in the foreground context to give users a chance to configure options, e.g. via "using [[show_consts]]";

turned show_consts into proper configuration option;

prefer regular Proof.context over background theory; misc tuning and simplification;

just one refute.ML;

use existing Integer.pow, despite its slightly odd argument order;

tuned whitespace and indentation, emphasizing the logical structure of this long text;

inner parsing: refrain from too many nested position reports to achieve more precise error feedback in the source;

Document_View: squiggly underline for messages; tuned;

added gfx_range convenience;

Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;

Position.Range: exclude singularity (again);

merged

merged

FIXME -> TODO (nothing is broken)

Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF

use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; this *really* speeds up things -- HOL now builds 12% faster on my machine

make definitional CNF translation code more robust in the presence of existential quantifiers in the "literals"

formal framework for presentation of selected statements

merged

Table.map replaces Table.map'

dropped dead code; tuned

include names need not be considered as reserved any longer

skip empty name bunches; fill up trailing positions with NONEs

use code_namespace module for SML and OCaml code

Table.map replaces Table.map'

avoid cyclic modules

merged

simultaneous modification of statements: statement names

simultaneous modification of statements

explicit modify_stmt parameter

Graph.map, in analogy to Table.map

replaced Table.map' by Table.map

merged

tuned

generalized hierarchical data structure over statements

merged

normalization is allowed to solve True

merged

merged

cosmetics

SNARK doesn't like facts

show real CPU time

factor out code shared by all ATPs so that it's run only once

handle all whitespace, not just ASCII 32

speed up SPASS hack + output time information in "blocking" mode

remove time information in output, since it's confusing anyway

minor refactoring

translate the axioms to FOF once and for all ATPs

run relevance filter in a thread, to avoid blocking

add dependency of "spass" script

more elegant ML

only kill ATP threads in nonblocking mode

lower number of facts given to SInE

share the relevance filter among the provers

got rid of the "theory_relevant" option; instead, have fudge factors that behave more smoothly for all provers

generalize theorem argument parsing syntax

support new option in Mirabelle

fiddled with fudge factor (based on Mirabelle)

give priority to assumptions in structured proofs

introduce fudge factors to deal with "theory const"

rename sledgehammer config attributes

finish moving file

move file

finished renaming

fix typo

shorten a few file names

added "expect" feature of Nitpick to Sledgehammer, for regression testing

update docs

update docs

added "blocking" option to Sledgehammer to run in synchronous mode; sometimes useful, e.g. for testing

normalization fails on unchanged goal

turned show_question_marks into proper configuration option; show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname; tuned;

prefer regular print functions over slightly low-level Term.string_of_vname;

eliminated obsolete old-style goal stack package, which was considered the main Isabelle user interface at some point;

eliminated really ancient OldGoals operations in favour of Goal.prove_internal (with its minimal checks and without normalization of result); tuned white space; tuned indentation;

Document.State.Assignment: eliminated promise in favour of plain values -- signalling is done via event bus in Session;

actually declare "_constrainAbs" as @{syntax_const};

merged

repaired attribute code_unfold_post which has ever been broken

tuned text segment

merged

factored out generic part of Scala serializer into code_namespace.ML

merged

do not print object frame around Scala includes -- this is in the responsibility of the user

repaired codegen tool

tuned internally and made smlnj happy

merged

renewing specifications in HOL-Auth

adapting and tuning example theories

adding further example for quickcheck with prolog code generation

handling the quickcheck result no counterexample more correctly

adding manual reordering of premises to prolog generation

towards support of limited predicates for mutually recursive predicates

improving clash-free naming of variables and preds in code_prolog

exporting mode analysis for use in prolog generation

renaming

improving naming of predicates in code_prolog; changing order of flattened premises once again

changing order of premises generated when flattening functions in premises; adapting example for second attack for hotel key card system

added further hotel key card attack in example file

avoiding warning for a duplicate rewrite rule in preprocessing of the predicate compiler

using Cache_IO interface for a safe parallel prolog execution

storing options for prolog code generation in the theory

adapting example files to latest changes

adding Lambda example theory; tuned

added quite adhoc logic program transformations limited_predicates and replacements of predicates

distinguish between "by" and "apply"

merged

fiddling with "try"

updated

"try" -- a new diagnosis tool that tries to apply several methods in parallel

add one option to Mirabelle

update docs

add a penalty for being higher-order

improve weighting of irrelevant constants, based on Mirabelle experiments

take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter

repaired casual accident; tuned names

corrected misbehaved additional qualification of generated names

merged

avoid strange special treatment of empty module names

allow explicit parameter for code width

evaluate takes ml context and ml expression parameter

modernized; avoid pointless tinkering with structure names

distinguish code production and code presentation

dropped single_module parameter

tuned

record argument for serializers

tuned serializer argument interface

removed serializer interface redundancies

more coherent naming of syntax data structures

Code_Printer.tuplify

dropped legacy interfaces

more permissive: simplification solves the goal when rhs = undefined

merged

tuned

tuned

tuned

tuned

tuned file interface

tuned

eliminated some obscure higher-order arguments

trailing newline by default

width is a formal parameter of serialization

whitespace tuning

tuned comment

merged

fiddle with fact filter

adjust Mirabelle

rule out low-level class facts

make Sledgehammer's relevance filter somewhat slacker

move imperative code to where it belongs

fiddle with fact filter based on Mirabelle experiments

allow configuration of fact filter fudge factors

made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)

execute actions in same order as specified on command line

show index in fact list of all found facts

allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID

deal with duplicates

improve new "sledgehammer_filter" action

remove useless var