merged

merged

tuned text

sections on @{code} and code_reflect

formal syntax diagram for code_reflect

distinguish SML and Eval explicitly

no_frees_* is subsumed by new framework mechanisms in Code_Preproc

reject term variables explicitly

avoid frees and vars in terms to be evaluated by abstracting and applying

tuned whitespace

make SML/NJ happier

more conventional conversion signature

added nbe paper

continued section abut evaluation

make SML/NJ happier

new lemma

merged

new lemmas

revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms

basic setup for Session_Dockable controls;

tuned signature;

more content for Session_Dockable;

basic support for full document rendering;

Session_Dockable: basic syslog output;

just one Session.raw_messages event bus;

more reactive handling of Isabelle_Process startup errors;

eliminated Simple_Thread shorthands that can overlap with full version;

main Isabelle_Process via Isabelle_System.Managed_Process; simplified init message: no pid; misc tuning and simplification;

more robust Managed_Process.kill: check after sending signal;

more robust lib/scripts/process, with explicit script/no_script mode; added general Isabelle_System.Managed_Process, with bash_output as application; tuned;

Standard_System.with_tmp_file: deleteOnExit to make double sure;

refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;

tuned whitespace;

tuned;

added Standard_System.slurp convenience; tuned;

added Simple_Thread.future convenience; tuned;

refined ML/Scala bash wrapper, based on more general lib/scripts/process;

tuned;

more robust Isabelle_System.rm_fifo: avoid external bash invocation, which might not work in JVM shutdown phase (due to Runtime.addShutdownHook);

tuned;

added Isabelle_Process.syslog; refined Isabelle_Process.process_manager: startup_output via syslog, explicit join of auxiliary threads; tuned;

updated keywords;

merged

merged

corrected long-overlooked slip: the Pure equality of a code equation is no part of the code equation itself

dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term

Pure equality is a regular cpde operation

full palette of dynamic/static value(_strict/exn)

Factored out ML into separate file

merged

merged

remove needless exception

preprocess "Ex" before doing clausification in Metis; this is dual to "All" in b96941dddd04

expand_fun_eq -> fun_eq_iff

use buffers instead of string concatenation

renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;

more antiquotations;

added XML.content_of convenience -- cover XML.body, which is the general situation;

merged

merged

more accurate exception handling

merged

merge tracing of two related modules

merged

preprocess "All" before doing clausification in Metis; helps the definitional clausifier produce fewer clauses

reorder proof methods and take out "best"; suggestions from Tobias

renaming variable name to decrease likelyhood of nameclash

code_pred_intro can be used to name facts for the code_pred command

replacing temporary hack by checking for environment settings of the component

removing unnessary options for code_pred

moving renaming_vars to post_processing; removing clone in values and quickcheck of code_prolog

removing clone in code_prolog and predicate_compile_quickcheck

adjusted

updated file duplicate

\\isatypewrite now part of isabelle latex style

made smlnj happy

properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models

do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)

generalized lemma insort_remove1 to insort_key_remove1

generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants

merged

less intermediate data structures

Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);

simplified Isabelle_System.mk_fifo: inlined script, append PPID and PID uniformly;

refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop; tuned;

back to default fold painter -- Circle looks slightly odd in conjunction with bracket matching;

message_actor: more robust treatment of EOF;

simplified Isabelle_Process message kinds; misc tuning and simplification;

recovered basic session stop/restart;

simplified fifo handling -- rm_fifo always succeeds without ever blocking; tuned;

raw_execute: let IOException pass-through unhindered (again);

mkfifo: some workaround to ensure reasonably unique id, even on Cygwin where $PPID might fall back on odd default;

Isabelle_System.mk_fifo: more robust enumeration of unique names, based on persisting JVM pid (parent of shell process);

slightly more robust Isabelle_Process startup -- NB: openening fifo streams synchronizes with other end, which may fail to reach that point;

tuned;

separate Isabelle.logic_selector;

non-editable text area;

basic setup for prover session panel;

ML_Syntax.print_char: more readable output of some well-known ASCII controls -- this is relevant for ML toplevel pp;

discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);

Isabelle_Markup.overview_color: indicate error / warning messages;

some specific message classification;

Syntax.read_asts error: report token ranges within message -- no side-effect here;

Isabelle_Process: status/report do not require serial numbers;

simplified some internal flags using Config.T instead of full-blown Proof_Data;

tuned signature of (Context_)Position.report variants;

merged

merged

update README

regenerate "metis.ML"

fix license

updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)

move functions around

simplify Skolem handling; things are much easier now that Sledgehammer doesn't skolemize, only Metis

make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}

complete refactoring of Metis along the lines of Sledgehammer

got caught once again by SML's pattern maching (ctor vs. var)

added new "Metis_Reconstruct" module, temporarily empty

rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"

move SPASS's Flotter hack to "Sledgehammer_Reconstruct"

skip some "important" messages

refactoring: move ATP proof and error extraction code to "ATP_Proof" module

merged

added lemmas

merged

proper closures for static evaluation; no need for FIXMEs any longer

refined static_eval_conv_simple; tuned comments

closures preserve static serializer context for static evaluation; tuned

closures separate serializer initialization from serializer invocation as far as appropriate

add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions

made sml/nj happy

merged

added code_stmts antiquotation from doc-src/more_antiquote.ML

added output_typewriter from doc-src/more_antiquote.ML

moved material intro distribution proper

merged

merged

separation of static and dynamic thy context

adjusted setup

dynamic and static value computation; built-in evaluation of propositions

Exn.map_result

adjusted to changes in Code_Runtime

merged

merged

improving replacing higher order arguments to work with tuples

adding another context free grammar example for the predicate compiler

adding values to show and ensure that values works with complex terms and restores numerals on natural numbers

adding restoring of numerals for natural numbers for values command

values command for prolog supports complex terms and not just variables

adapting examples

registering code_prolog as component; using environment variable; adding settings file for prolog code generation

adding mode inference to prolog compilation; separate between (ad-hoc) code modifications and system_configuration; adapting quickcheck

merged

tidied a few proofs

merged

avoid code duplication

tuning

merge constructors

factor out the inverse of "nice_atp_problem"

use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs

factored out TSTP/SPASS/Vampire proof parsing; from "Sledgehammer_Reconstructo" to a new module "ATP_Proof"

prevent exception when calling "Mirabelle.can_apply" on empty proof sequence; the Judgement Day logs sometimes had entries of the form at 970:26 (apply): ------------------ ------------------ ; these were apparently caused by this Mirabelle bug

supply the Metis parameter defaults as argument, instead of patching the Metis sources; these values were found by Larry in 2007 and using anything else risks losing proofs

regenerated "metis.ML"

streamlined "make_metis"

put Isabelle-specifics in a "PortableIsabelle" file maintained by us; as recommended by Joe Hurd

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)