name tuning

merge

better weight functions for MePo/MaSh etc.

merge

more

tuned infix table

crank up default timeout for MaSh ATP learning

removed odd associativity of ==

updated SMT certificates

refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)

tuned "use build timeout": tuples cannot be concatenated

use build timeout (wall clock time, default: 2h)

removed unused usedir_options

removed obsolete setting tweaks: build -s already sets output correctly

plain init_components calls instead of symlinks

tolerate non-existent ISABELLE_OUTPUT

removed obsolete parameter for contrib dir; hard-coding is not a problem

mira: do not hard-code polyml version

discontinued legacy antiquotations and styles

avoid references altogether

catch all parsing errors

no need for tracing

updated MaSh serialization number (to reflect new weights)

synchronize access to shared reference and print proper total

add a timeout in induction rule instantiation

contain exponential explosion of term patterns

tuned weights -- keep same relative values, but use 1.0 as the least weight

really honor pattern depth, and use 2 by default

tuned order to help debugging

added table of infix operators

made element and subset relations non-associative (just like all orderings)

merged

more parallel find_unused_assms; tuned messages;

useful commutative diagram for while_option

more hints on technical issues due to shared-disk access of central Mercurial repository;

prefer implicit build_dialog of isabelle jedit; clarified isabelle build variants; back to $HOME despite some chance that Windows users get it wrong;

offer sessions of group "main" first to increase chances that the user makes a sensible choice;

new contributor

updated README;

HOL-Quickcheck_Benchmark works without timeout (NB: isatest imposes global timeout already);

tuning

merged

reverting d466ebc27810 as the previous changeset should allow to run Find_Unused_Assms_Examples again

providing a custom code equation for vimage to overwrite the vimage definition that would be rewritten by set_comprehension_pointfree simproc in the code preprocessor to an non-terminating code equation

tuned signature: use thy_load to adapt to prover/editor specific view on sources;

tuned property name;

allow to suppress ISABELLE_SYMBOLS for experiments;

escape nicknames

generate proper nicks also for instantiated induction rules

added tracing to ATP exporter

merged

MaSh exporter can now export subsets of the facts, as consecutive ranges

avoid creating nested threads for MaSh -- this seems to cause thread creation failures for machines with dozens of cores (unclear yet if that's really the issue)

thread no timeout properly

proper escaping in file name

encode lemma name in file name

more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment; more tooltip options via Rendering;

prefer more official getMenuShortcutKeyMask, in deviation to traditional jEdit technique;

maintain subtree_elements for improved performance of cumulate operator;

more formal class Markup_Tree.Elements;

tuned command line;

merged

unified layout of defs

tuned;

clarified build_dialog command line;

explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;

updated README;

fold main goal;

fold handling within Pretty_Text_Area, based on formal document content, which is static here; fold subgoals;

tuned signature;

tuned;

tuned error dialog;

init gutter according to view properties, which improves symmetry of windows and allows use of folds etc;

more subgoal markup information, which is potentially useful to manage proof state output;

merged

contribution by A. Colgio

merged

renamed "emb" to "list_hembeq"; make "list_hembeq" reflexive independent of the base order; renamed "sub" to "sublisteq"; dropped "transp_on" (state transitivity explicitly instead); no need to hide "sub" after renaming; replaced some ASCII symbols by proper Isabelle symbols; NEWS

actually request heap image in initial up-to-date check;

clarified "isabelle options" command line, to make it more close to "isabelle components";

updated some headers;

clarified README;

more formal components_checksum tool;

just one Admin/components/ directory;

Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors

NEWS

merged

get rid of some junk facts in the MaSh evaluation driver

generate original name as a comment in SPASS problems as well

generate comments with original names for debugging

use MaSh nicknames in ATP problem files to facilitate gathering of statistics

parallelized MaSh exporter

short library for streams

renamed theory

renamed "emb" to "list_hembeq"; make "list_hembeq" reflexive independent of the base order; renamed "sub" to "sublisteq"; dropped "transp_on" (state transitivity explicitly instead); no need to hide "sub" after renaming; replaced some ASCII symbols by proper Isabelle symbols; NEWS

shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other

tuned two lemma names, to avoid name hint clash (which confuses the MaSh evaluation, and which anyway isn't nice or necessary)

tuning

tweaked which facts are included for MaSh evaluations

don't query blacklisted theorems in evaluation driver

export a pair of ML functions

merged;

tuned implementation according to Library.insert/merge in ML;

more formal class Command.Results;

odd bias of sub/superscript keyboard shortcuts -- according to frequency of use;

smarter handling of tracing messages: prover process pauses and enters user dialog;

tuned;

enable Isabelle/ML to produce uninterpreted result messages as well;

include command results in tooltip as well;

more careful handling of Dialog_Result, with active area and color feedback; more formal type Command.Results; propagate command results to output, which is required to resolve update of dialog state; clarified Markup.message: retain uninterpreted messages;

identify dialogs via official serial and maintain as result message; clarified Protocol.is_inlined: suppress result/tracing/state messages uniformly; cumulate_markup/select_markup depending on command state; explicit Rendering.output_messages; tuned source structure;

rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;

support dialog via document content;

merged

further fix related to bd9a0028b063 -- that change was per se right, but it exposed a bug in the pattern for "all"

better tautology check -- don't reject "prod_cases3" for example

tuned debugging file names

more systematic identifier variants to facilitate experimentation;

prevent dedicated MacOSX plugin from switching off vital workarounds;

improved coupling of zoom_box and scale; explicit rescale(1.0) on startup;

really all facts means really all facts (well, almost)

tuning

use modern SAT solvers with modern Kodkod versions

got rid of support for Kodkodi < 1.2.14

made MaSh evaluation driver work with SMT solvers

merge aliased theorems in MaSh dependencies, modulo symmetry of equality

adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)

better name for SMT solver files

updated version of MaSh learner engine

push normalization further -- avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)

disable Find_Unused_Assms_Examples for now, to recover isatest sanity;

less massive arrow heads;

added explicit zoom box;

some attempts at more discrete scale factor;

more official graphics context with font metrics;

just one class with parameters;

initial layout coordinates more like old browser; tuned geometry defaults;

added speculative options for jEdit;

separate instance of class Parameters for each Main_Panel -- avoid global program state; misc tuning;

discontinued long names flag -- better done via entity markup, without affecting layout;

tuned;

tuned;

tuned min/max;

tuned;

keep diagnostic command -- avoid confusion when it disappears;

tuned;

tuned signature;

removed somewhat pointless Edge_Transitive filter, as the graph is always reduced to its Hasse diagram, to have any chance to layout efficiently;

merge

merged

merge

changed capitalization of MeSh filter

(re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores

further clarification for Windows;

merged

more generous tracing limit -- rescaled in MB;

recovered title property from bfb5964e3041;

some clarification for Windows;

stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;

tuned;

generalized notion of active area, where sendback is just one application; some support for graphview via active area;

merged

have MaSh evaluator keep all raw problem/solution files in a directory

clarified transitive_closure: proper cumulation of transitive steps, which is essential for Warshall-style algorithms;

always apply transitive_reduction_acyclic in imitation of old graph browser (essential to avoid slow layout and overcrowded display, e.g. class_deps);

added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;

merged

merge

don't blacklist "case" theorems -- this causes problems in MaSh later

more changes to MaSh Python program (by Daniel K.)

don't have MaSh pretend it knows facts it doesn't know

reverted parallel map idea -- appears to make success rate of ATPs less stable (might even lead to bias in favor of MePo)

fixed embarrassing off-by-one bug in MaSh's Mesh

store evaluation output in a file

use parallel map

tweak MaSh fudge factors

more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"

basic monitor panel, using the powerful jfreechart library; sorted Isabelle menu entries -- this is mainly a catalog;

added jfreechart library, including the old version of iText from its distribution (required for the demo application and examples);

check consistent theory names for direct imports as well -- as claimed in the comments (see also 1cc36c0ec9eb);

make double-sure that the future scheduler is properly shutdown, otherwise its threads are made persistent and will deadlock with the fresh instance after reloading the image (NB: Present.finish involves another Par_List.map over document_variants and thus might fork again);

final report_status within SYNCHRONIZED part of scheduler loop: required for sanity of data;

adhoc recovery from spurious NPEs, similar quantum-effect behind 7c8ce63a3c00;

obsolete;

eliminated old copy of proof.sty (1995), prefer the one usually included in current latex distributions (2005); \usepackage{proof} only where required;

merged

deactivate actual fork -- unstable in scala-2.9.2 on multicore hardware;

some support to recover from spurious crash -- this is Physics, not Mathematics;

avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;

tuned text

corrected nonsensical associativity of `` and dvd

add exponential and uniform distributions

fundamental theorem of calculus for the Lebesgue integral

add Int_atMost

more rigorous "build only" mode: avoid build dialog of logic image and its potential need for GUI display;

fork slow part of Thy_Load.body_files only;

explore theory_body_files via future, for improved performance; further internalization of header errors;

merged

use proper entry point for MaSh in test driver

export ATP and Isar commands separately

proper Sendback.markup, as required for standard Prover IDE protocol (see also c62ce309dc26);

discontinued obsolete "Tracing" button -- limited tracing channel works sufficiently well;

discontinued option jedit_auto_start, which is somewhat pointless as there is no manual session start within Isabelle/jEdit;

updated README;

documentation for isabelle build_dialog and its implicit use in isabelle jedit;

clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL); added jedit option -n to bypass build_dialog;

avoid startup within GUI thread -- it is only required later for dialog; tuned signature;

more uniform default logic, using settings, options, args etc.; clarified build_dialog -C: imitate jEdit logic selection more precisely;

use right names in MePo exporter

parse more liberal MaSh suggestion syntax (for the eval driver)

merged

made Python code compile again (by Daniel K.)

tweaked MaSh proximity

reduce max number of dependencies for MaSh to get rid of junk

more feature tweaks

prioritize chained facts

more MaSh feature tweaking

record free variables as a MaSh feature

expand type classes into their ancestors for MaSh

tweaked MaSh features, based on comments by Josef Urban

increase weight of local facts again (MaSh)

simplify code now that "mash.py" supports weights

added weights to MaSh (by Daniel Kuehlwein)

Move the measurability prover to its own file

Show search depth in the debug output of the measurability prover

Remove looping rule from measurability prover

rules for improper Lebesgue integrals (using tendsto at_top)

take proximity into account for MaSh + fix a debilitating bug in feature generation

tuning

clarified default button (cf. org/gjt/sp/jedit/gui/OptionsDialog.java);

select logic session names, not paths;

added keyboard shortcut for button (canonical way to do that?);

evade ugly default font, notably on Windows laf;

center main window;

more direct dialog via existing GUI components;

clarified logic argument: session name, not path name; tuned;

tuned message;

implicit build_dialog for Isabelle/jEdit; clarified option -l: refer to session name, not image path;

tuned message;

tuned OK feedback;