diff --git a/etc/components b/etc/components --- a/etc/components +++ b/etc/components @@ -1,10 +1,9 @@ #built-in components src/Tools/jEdit src/Tools/Graphview src/Tools/VSCode -src/HOL/Mirabelle src/HOL/Mutabelle src/HOL/Library/Sum_of_Squares src/HOL/SPARK src/HOL/Tools src/HOL/TPTP diff --git a/etc/options b/etc/options --- a/etc/options +++ b/etc/options @@ -1,361 +1,363 @@ (* :mode=isabelle-options: *) section "Document Preparation" option browser_info : bool = false -- "generate theory browser information" option document : string = "" -- "build document in given format: pdf, dvi, false" option document_output : string = "" -- "document output directory" option document_variants : string = "document" -- "alternative document variants (separated by colons)" option document_tags : string = "" -- "default command tags (separated by commas)" option thy_output_display : bool = false -- "indicate output as multi-line display-style material" option thy_output_break : bool = false -- "control line breaks in non-display material" option thy_output_cartouche : bool = false -- "indicate if the output should be delimited as cartouche" option thy_output_quotes : bool = false -- "indicate if the output should be delimited via double quotes" option thy_output_margin : int = 76 -- "right margin / page width for printing of display material" option thy_output_indent : int = 0 -- "indentation for pretty printing of display material" option thy_output_source : bool = false -- "print original source text rather than internal representation" option thy_output_source_cartouche : bool = false -- "print original source text rather than internal representation, preserve cartouches" option thy_output_modes : string = "" -- "additional print modes for document output (separated by commas)" section "Prover Output" option show_types : bool = false -- "show type constraints when printing terms" option show_sorts : bool = false -- "show sort constraints when printing types" option show_brackets : bool = false -- "show extra brackets when printing terms/types" option show_question_marks : bool = true -- "show leading question mark of schematic variables" option show_consts : bool = false -- "show constants with types when printing proof state" option show_main_goal : bool = false -- "show main goal when printing proof state" option goals_limit : int = 10 -- "maximum number of subgoals to be printed" option names_long : bool = false -- "show fully qualified names" option names_short : bool = false -- "show base names only" option names_unique : bool = true -- "show partially qualified names, as required for unique name resolution" option eta_contract : bool = true -- "print terms in eta-contracted form" option print_mode : string = "" -- "additional print modes for prover output (separated by commas)" section "Parallel Processing and Timing" public option threads : int = 0 -- "maximum number of worker threads for prover process (0 = hardware max.)" option threads_trace : int = 0 -- "level of tracing information for multithreading" option threads_stack_limit : real = 0.25 -- "maximum stack size for worker threads (in giga words, 0 = unlimited)" public option parallel_limit : int = 0 -- "approximative limit for parallel tasks (0 = unlimited)" public option parallel_print : bool = true -- "parallel and asynchronous printing of results" public option parallel_proofs : int = 1 -- "level of parallel proof checking: 0, 1, 2" option parallel_subproofs_threshold : real = 0.01 -- "lower bound of timing estimate for forked nested proofs (seconds)" +option parallel_presentation : bool = true + -- "parallel theory presentation" option command_timing_threshold : real = 0.1 -- "default threshold for persistent command timing (seconds)" public option timeout_scale : real = 1.0 -- "scale factor for timeout in Isabelle/ML and session build" section "Detail of Proof Checking" option record_proofs : int = -1 -- "set level of proofterm recording: 0, 1, 2, negative means unchanged" option quick_and_dirty : bool = false -- "if true then some tools will OMIT some proofs" option skip_proofs : bool = false -- "skip over proofs (implicit 'sorry')" option strict_facts : bool = false -- "force lazy facts when defined in context" section "Global Session Parameters" option condition : string = "" -- "required environment variables for subsequent theories (separated by commas)" option timeout : real = 0 -- "timeout for session build job (seconds > 0)" option process_output_limit : int = 100 -- "build process output limit (in million characters, 0 = unlimited)" option process_output_tail : int = 40 -- "build process output tail shown to user (in lines, 0 = unlimited)" option profiling : string = "" -- "ML profiling (possible values: time, allocations)" option system_heaps : bool = false -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS" section "ML System" option ML_print_depth : int = 20 -- "ML print depth for toplevel pretty-printing" public option ML_exception_trace : bool = false -- "ML exception trace for toplevel command execution" public option ML_exception_debugger : bool = false -- "ML debugger exception trace for toplevel command execution" public option ML_debugger : bool = false -- "ML debugger instrumentation for newly compiled code" public option ML_system_64 : bool = false -- "ML system for 64bit platform is used if possible (change requires restart)" public option ML_process_policy : string = "" -- "ML process command prefix (process policy)" section "PIDE Build" option pide_reports : bool = true -- "report PIDE markup" option build_pide_reports : bool = true -- "report PIDE markup in batch build" section "Editor Session" public option editor_load_delay : real = 0.5 -- "delay for file load operations (new buffers etc.)" public option editor_input_delay : real = 0.2 -- "delay for user input (text edits, cursor movement etc.)" public option editor_generated_input_delay : real = 1.0 -- "delay for machine-generated input that may outperform user edits" public option editor_output_delay : real = 0.1 -- "delay for prover output (markup, common messages etc.)" public option editor_consolidate_delay : real = 2.0 -- "delay to consolidate status of command evaluation (execution forks)" public option editor_prune_delay : real = 15 -- "delay to prune history (delete old versions)" option editor_prune_size : int = 0 -- "retained size of pruned history (delete old versions)" public option editor_update_delay : real = 0.5 -- "delay for physical GUI updates" public option editor_reparse_limit : int = 10000 -- "maximum amount of reparsed text outside perspective" public option editor_tracing_messages : int = 1000 -- "initial number of tracing messages for each command transaction (0: unbounded)" public option editor_chart_delay : real = 3.0 -- "delay for chart repainting" public option editor_continuous_checking : bool = true -- "continuous checking of proof document (visible and required parts)" public option editor_output_state : bool = false -- "implicit output of proof state" option editor_execution_delay : real = 0.02 -- "delay for start of execution process after document update (seconds)" option editor_syslog_limit : int = 100 -- "maximum amount of buffered syslog messages" public option editor_presentation : bool = false -- "dynamic presentation while editing" section "Headless Session" option headless_consolidate_delay : real = 15 -- "delay to consolidate status of command evaluation (execution forks)" option headless_prune_delay : real = 60 -- "delay to prune history (delete old versions)" option headless_check_delay : real = 0.5 -- "delay for theory status check during PIDE processing (seconds)" option headless_check_limit : int = 0 -- "maximum number of theory status checks (0 = unlimited)" option headless_nodes_status_delay : real = -1 -- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)" option headless_watchdog_timeout : real = 600 -- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)" option headless_commit_cleanup_delay : real = 60 -- "delay for cleanup of already imported theories (seconds, 0 = disabled)" option headless_load_limit : real = 5.0 -- "limit in MB for loaded theory files (0 = unlimited)" section "Miscellaneous Tools" public option find_theorems_limit : int = 40 -- "limit of displayed results" public option find_theorems_tactic_limit : int = 5 -- "limit of tactic search for 'solves' criterion" section "Completion" public option completion_limit : int = 40 -- "limit for completion within the formal context" public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store" -- "glob patterns to ignore in file-system path completion (separated by colons)" section "Spell Checker" public option spell_checker : bool = true -- "enable spell-checker for prose words within document text, comments etc." public option spell_checker_dictionary : string = "en" -- "spell-checker dictionary name" public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment" -- "included markup elements for spell-checker (separated by commas)" public option spell_checker_exclude : string = "document_marker,antiquoted,raw_text" -- "excluded markup elements for spell-checker (separated by commas)" section "Secure Shell" option ssh_config_dir : string = "$HOME/.ssh" -- "SSH configuration directory" option ssh_config_file : string = "$HOME/.ssh/config" -- "main SSH configuration file" option ssh_identity_files : string = "$HOME/.ssh/id_dsa:$HOME/.ssh/id_ecdsa:$HOME/.ssh/id_rsa" -- "possible SSH identity files (separated by colons)" option ssh_compression : bool = true -- "enable SSH compression" option ssh_connect_timeout : real = 60 -- "SSH connection timeout (seconds)" option ssh_alive_interval : real = 30 -- "time interval to keep SSH server connection alive (seconds)" option ssh_alive_count_max : int = 3 -- "maximum number of messages to keep SSH server connection alive" section "Phabricator" option phabricator_version_arcanist : string = "7af9846f994a8d0a1fc89af996e3ddd81f01765e" -- "repository version for arcanist" option phabricator_version_phabricator : string = "2afedad61c5181bb4f832cea27b9b59df19f3fd5" -- "repository version for phabricator" section "Theory Export" option export_theory : bool = false -- "export theory content to Isabelle/Scala" option export_standard_proofs : bool = false -- "export standardized proof terms to Isabelle/Scala (not scalable)" option export_proofs : bool = false -- "export proof terms to Isabelle/Scala" option prune_proofs : bool = false -- "prune proof terms after export (do not store in Isabelle/ML)" section "Theory update" option update_inner_syntax_cartouches : bool = false -- "update inner syntax (types, terms, etc.) to use cartouches" option update_mixfix_cartouches : bool = false -- "update mixfix templates to use cartouches instead of double quotes" option update_control_cartouches : bool = false -- "update antiquotations to use control symbol with cartouche argument" option update_path_cartouches : bool = false -- "update file-system paths to use cartouches" section "Build Database" option build_database_server : bool = false option build_database_user : string = "" option build_database_password : string = "" option build_database_name : string = "" option build_database_host : string = "" option build_database_port : int = 0 option build_database_ssh_host : string = "" option build_database_ssh_user : string = "" option build_database_ssh_port : int = 0 section "Build Log Database" option build_log_database_user : string = "" option build_log_database_password : string = "" option build_log_database_name : string = "" option build_log_database_host : string = "" option build_log_database_port : int = 0 option build_log_ssh_host : string = "" option build_log_ssh_user : string = "" option build_log_ssh_port : int = 0 option build_log_history : int = 30 -- "length of relevant history (in days)" option build_log_transaction_size : int = 1 -- "number of log files for each db update" section "Isabelle/Scala/ML system channel" option system_channel_address : string = "" option system_channel_password : string = "" diff --git a/src/HOL/Main.thy b/src/HOL/Main.thy --- a/src/HOL/Main.thy +++ b/src/HOL/Main.thy @@ -1,73 +1,74 @@ section \Main HOL\ text \ Classical Higher-order Logic -- only ``Main'', excluding real and complex numbers etc. \ theory Main imports Predicate_Compile Quickcheck_Narrowing + Mirabelle Extraction Nunchaku BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices Binomial GCD begin text \Namespace cleanup\ hide_const (open) czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift shift proj id_bnf hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV text \Syntax cleanup\ no_notation bot ("\") and top ("\") and inf (infixl "\" 70) and sup (infixl "\" 65) and Inf ("\") and Sup ("\") and ordLeq2 (infix "<=o" 50) and ordLeq3 (infix "\o" 50) and ordLess2 (infix "(_,/ _)\") bundle cardinal_syntax begin notation ordLeq2 (infix "<=o" 50) and ordLeq3 (infix "\o" 50) and ordLess2 (infix " 'b \ 'b" ("(3\_./ _)" [0, 10] 10) "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) "_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) end diff --git a/src/HOL/Mirabelle/Mirabelle.thy b/src/HOL/Mirabelle.thy rename from src/HOL/Mirabelle/Mirabelle.thy rename to src/HOL/Mirabelle.thy --- a/src/HOL/Mirabelle/Mirabelle.thy +++ b/src/HOL/Mirabelle.thy @@ -1,20 +1,19 @@ -(* Title: HOL/Mirabelle/Mirabelle.thy +(* Title: HOL/Mirabelle.thy Author: Jasmin Blanchette and Sascha Boehme, TU Munich *) theory Mirabelle -imports Main + imports Sledgehammer Predicate_Compile begin -ML_file \Tools/mirabelle.ML\ - -ML \Toplevel.add_hook Mirabelle.step_hook\ - -ML \ -signature MIRABELLE_ACTION = -sig - val invoke : (string * string) list -> theory -> theory -end -\ +ML_file \Tools/Mirabelle/mirabelle.ML\ +ML_file \Tools/Mirabelle/mirabelle_arith.ML\ +ML_file \Tools/Mirabelle/mirabelle_metis.ML\ +ML_file \Tools/Mirabelle/mirabelle_quickcheck.ML\ +(* +ML_file \Tools/Mirabelle/mirabelle_sledgehammer.ML\ +ML_file \Tools/Mirabelle/mirabelle_sledgehammer_filter.ML\ +*) +ML_file \Tools/Mirabelle/mirabelle_try0.ML\ end diff --git a/src/HOL/Mirabelle/Mirabelle_Test.thy b/src/HOL/Mirabelle/Mirabelle_Test.thy deleted file mode 100644 --- a/src/HOL/Mirabelle/Mirabelle_Test.thy +++ /dev/null @@ -1,23 +0,0 @@ -(* Title: HOL/Mirabelle/Mirabelle_Test.thy - Author: Sascha Boehme, TU Munich -*) - -section \Simple test theory for Mirabelle actions\ - -theory Mirabelle_Test -imports Main Mirabelle -begin - -ML_file \Tools/mirabelle_arith.ML\ -ML_file \Tools/mirabelle_metis.ML\ -ML_file \Tools/mirabelle_quickcheck.ML\ -ML_file \Tools/mirabelle_sledgehammer.ML\ -ML_file \Tools/mirabelle_sledgehammer_filter.ML\ -ML_file \Tools/mirabelle_try0.ML\ - -text \ - Only perform type-checking of the actions, - any reasonable test would be too complicated. -\ - -end diff --git a/src/HOL/Mirabelle/etc/settings b/src/HOL/Mirabelle/etc/settings deleted file mode 100644 --- a/src/HOL/Mirabelle/etc/settings +++ /dev/null @@ -1,9 +0,0 @@ -# -*- shell-script -*- :mode=shellscript: - -MIRABELLE_HOME="$COMPONENT" - -MIRABELLE_LOGIC=HOL -MIRABELLE_THEORY=Main -MIRABELLE_TIMEOUT=30 - -ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools" diff --git a/src/HOL/Mirabelle/ex/Ex.thy b/src/HOL/Mirabelle/ex/Ex.thy deleted file mode 100644 --- a/src/HOL/Mirabelle/ex/Ex.thy +++ /dev/null @@ -1,12 +0,0 @@ -theory Ex imports Pure -begin - -ML \ - val rc = Isabelle_System.bash - "cd \"$ISABELLE_HOME/src/HOL/Analysis\"; if isabelle build -n \"$MIRABELLE_LOGIC\"; then isabelle mirabelle arith Inner_Product.thy; fi"; - if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc) - else (); -\ \ \some arbitrary small test case\ - -end - diff --git a/src/HOL/Mirabelle/lib/Tools/mirabelle b/src/HOL/Mirabelle/lib/Tools/mirabelle deleted file mode 100755 --- a/src/HOL/Mirabelle/lib/Tools/mirabelle +++ /dev/null @@ -1,136 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Sascha Boehme -# -# DESCRIPTION: testing tool for automated proof tools - - -PRG="$(basename "$0")" - -function print_action_names() -{ - for TOOL in "$MIRABELLE_HOME/Tools"/mirabelle_*.ML - do - echo "$TOOL" | perl -w -p -e 's/.*mirabelle_(.*)\.ML/ $1/' - done -} - -function print_sledgehammer_options() { - grep -e "^val .*K =" "$MIRABELLE_HOME/Tools/mirabelle_sledgehammer.ML" | \ - perl -w -p -e 's/val .*K *= *"(.*)" *\(\*(.*)\*\)/ $1$2/' -} - -function usage() { - # Do not forget to update the Sledgehammer documentation to reflect changes here. - [ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None" - timeout="$MIRABELLE_TIMEOUT" - echo - echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES" - echo - echo " Options are:" - echo " -L LOGIC parent logic to use (default $MIRABELLE_LOGIC)" - echo " -O DIR output directory for test data (default $out)" - echo " -S FILE user-provided setup file (no actions required)" - echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)" - echo " -d DIR include session directory" - echo " -q be quiet (suppress output of Isabelle process)" - echo " -t TIMEOUT timeout for each action in seconds (default $timeout)" - echo - echo " Apply the given actions at all proof steps in the given theory files." - echo - echo " ACTIONS is a colon-separated list of actions, where each action is" - echo " either NAME or NAME[OPTION,...,OPTION]. Available actions are:" - print_action_names - echo - echo " Available OPTIONs for the ACTION sledgehammer:" - print_sledgehammer_options - echo - echo " FILES is a list of theory files, where each file is either NAME.thy" - echo " or NAME.thy[START:END] and START and END are numbers indicating the" - echo " range the given actions are to be applied." - echo - exit 1 -} - -function fail() -{ - echo "$1" >&2 - exit 2 -} - - -## process command line - -# options - -[ $# -eq 0 ] && usage - -MIRABELLE_DIR= -MIRABELLE_SETUP_FILE= - -while getopts "L:T:O:d:t:S:q?" OPT -do - case "$OPT" in - L) - MIRABELLE_LOGIC="$OPTARG" - ;; - T) - MIRABELLE_THEORY="$OPTARG" - ;; - O) - MIRABELLE_OUTPUT_PATH="$OPTARG" - ;; - d) - MIRABELLE_DIR="$OPTARG" - ;; - t) - MIRABELLE_TIMEOUT="$OPTARG" - ;; - S) - MIRABELLE_SETUP_FILE="$OPTARG" - ;; - q) - MIRABELLE_QUIET="true" - ;; - \?) - usage - ;; - esac -done - -export MIRABELLE_DIR -export MIRABELLE_SETUP_FILE -export MIRABELLE_QUIET - -shift $(($OPTIND - 1)) - -export MIRABELLE_ACTIONS="$1" - -shift - - -# setup - -if [ -z "$MIRABELLE_OUTPUT_PATH" ]; then - MIRABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mirabelle$$" - PURGE_OUTPUT="true" -fi - -mkdir -p "$MIRABELLE_OUTPUT_PATH" - -export MIRABELLE_OUTPUT_PATH - - -## main - -for FILE in "$@" -do - perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE" || fail "Mirabelle failed." -done - - -## cleanup - -if [ -n "$PURGE_OUTPUT" ]; then - rm -rf "$MIRABELLE_OUTPUT_PATH" -fi diff --git a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl deleted file mode 100644 --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl +++ /dev/null @@ -1,182 +0,0 @@ -# -# Author: Jasmin Blanchette and Sascha Boehme -# -# Testing tool for automated proof tools. -# - -use File::Basename; - -# environment - -my $isabelle_home = $ENV{'ISABELLE_HOME'}; -my $mirabelle_home = $ENV{'MIRABELLE_HOME'}; -my $mirabelle_dir = $ENV{'MIRABELLE_DIR'}; -my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'}; -my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'}; -my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'}; -my $timeout = $ENV{'MIRABELLE_TIMEOUT'}; -my $be_quiet = $ENV{'MIRABELLE_QUIET'}; -my $user_setup_file = $ENV{'MIRABELLE_SETUP_FILE'}; -my $actions = $ENV{'MIRABELLE_ACTIONS'}; - -my $mirabelle_thy = $mirabelle_home . "/Mirabelle"; - - -# argument - -my $thy_file = $ARGV[0]; - -my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy"); -my $rand_suffix = join('', map { ('a'..'z')[rand(26)] } 1 .. 10); -my $new_thy_name = $thy_name . "_Mirabelle_" . $rand_suffix; -my $new_thy_file = $path . "/" . $new_thy_name . $ext; - - -# setup - -my $setup_file; -my $setup_full_name; - -if (-e $user_setup_file) { - $setup_file = undef; - my ($name, $path, $ext) = fileparse($user_setup_file, ".thy"); - $setup_full_name = $path . "/" . $name; -} -else { - -my $start_line = "0"; -my $end_line = "~1"; -if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) { - $thy_file = $1; - $start_line = $2; - $end_line = $3; -} - -my $setup_thy_name = $thy_name . "_Setup"; -my $setup_file = $output_path . "/" . $setup_thy_name . ".thy"; -my $log_file = $output_path . "/" . $thy_name . ".log"; - -my @action_files; -my @action_names; -foreach (split(/:/, $actions)) { - if (m/([^[]*)/) { - push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\""; - push @action_names, $1; - } -} -my $tools = ""; -if ($#action_files >= 0) { - # uniquify - my $s = join ("\n", @action_files); - my @action_files = split(/\n/, $s . "\n" . $s); - %action_files = sort(@action_files); - $tools = join("", map { "ML_file " . $_ . "\n" } (sort(keys(%action_files)))); -} - -open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'"; - -print SETUP_FILE < - Config.put_global Mirabelle.timeout $timeout #> - Config.put_global Mirabelle.start_line $start_line #> - Config.put_global Mirabelle.end_line $end_line -*} - -END - -@action_list = split(/:/, $actions); - -foreach (reverse(@action_list)) { - if (m/([^[]*)(?:\[(.*)\])?/) { - my ($name, $settings_str) = ($1, $2 || ""); - $name =~ s/^([a-z])/\U$1/; - print SETUP_FILE "setup {* Mirabelle_$name.invoke ["; - my $sep = ""; - foreach (split(/,/, $settings_str)) { - if (m/\s*([^=]*)\s*=\s*(.*)\s*/) { - print SETUP_FILE "$sep(\"$1\", \"$2\")"; - $sep = ", "; - } - elsif (m/\s*(.*)\s*/) { - print SETUP_FILE "$sep(\"$1\", \"\")"; - $sep = ", "; - } - } - print SETUP_FILE "] *}\n"; - } -} - -print SETUP_FILE "\nend"; -close SETUP_FILE; - -$setup_full_name = $output_path . "/" . $setup_thy_name; - -open(LOG_FILE, ">$log_file"); -print LOG_FILE "Run of $new_thy_file with:\n"; -foreach $action (@action_list) { - print LOG_FILE " $action\n"; -} -close(LOG_FILE); - -} - - -# modify target theory file - -open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'"; -my @lines = ; -close(OLD_FILE); - -my $setup_import = substr("\"$setup_full_name\"" . (" " x 1000), 0, 1000); - -my $thy_text = join("", @lines); -my $old_len = length($thy_text); -$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g; -$thy_text =~ s/\b$thy_name\./$new_thy_name./g; -$thy_text =~ s/(imports)(\s+)/$1 $setup_import$2/g; -die "No 'imports' found" if length($thy_text) == $old_len; - -open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'"; -print NEW_FILE $thy_text; -close(NEW_FILE); - - -# run isabelle - -my $quiet = ""; -my $output_log = 1; -if (defined $be_quiet and $be_quiet ne "") { - $quiet = " > /dev/null 2>&1"; - $output_log = 0; -} - -if ($output_log) { print "Mirabelle: $thy_file\n"; } - -my $cmd = - "isabelle process -o quick_and_dirty -o threads=1" . - " -T \"$path/$new_thy_name\" " . - ($mirabelle_dir ? "-d " . $mirabelle_dir . " " : "") . - "-l $mirabelle_logic" . $quiet; -my $result = system "bash", "-c", $cmd; - -if ($output_log) { - my $outcome = ($result ? "failure" : "success"); - print "\nFinished: $thy_file [$outcome]\n"; -} - - -# cleanup - -if (defined $setup_file) { - unlink $setup_file; -} -unlink $new_thy_file; - -exit ($result ? 1 : 0); diff --git a/src/HOL/ROOT b/src/HOL/ROOT --- a/src/HOL/ROOT +++ b/src/HOL/ROOT @@ -1,1209 +1,1210 @@ chapter HOL session HOL (main) = Pure + description " Classical Higher-order Logic. " options [strict_facts] sessions Tools theories Main (global) Complex_Main (global) document_theories Tools.Code_Generator document_files "root.bib" "root.tex" session "HOL-Examples" in Examples = HOL + description " Notable Examples in Isabelle/HOL. " sessions "HOL-Library" theories Adhoc_Overloading_Examples Ackermann Cantor Coherent Commands Drinker Groebner_Examples Iff_Oracle Induction_Schema Knaster_Tarski "ML" Peirce Records Seq document_files "root.bib" "root.tex" session "HOL-Proofs" (timing) in Proofs = Pure + description " HOL-Main with explicit proof terms. " options [quick_and_dirty = false, record_proofs = 2, parallel_limit = 500] sessions "HOL-Library" theories "HOL-Library.Realizers" session "HOL-Library" (main timing) in Library = HOL + description " Classical Higher-order Logic -- batteries included. " theories Library (*conflicting type class instantiations and dependent applications*) Finite_Lattice List_Lexorder List_Lenlexorder Prefix_Order Product_Lexorder Product_Order Subseq_Order (*conflicting syntax*) Datatype_Records (*data refinements and dependent applications*) AList_Mapping Code_Binary_Nat Code_Prolog Code_Real_Approx_By_Float Code_Target_Numeral Code_Target_Numeral_Float DAList DAList_Multiset RBT_Mapping RBT_Set (*printing modifications*) OptionalSugar (*prototypic tools*) Predicate_Compile_Quickcheck (*legacy tools*) Old_Datatype Old_Recdef Realizers Refute document_files "root.bib" "root.tex" session "HOL-Analysis" (main timing) in Analysis = HOL + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] sessions "HOL-Library" "HOL-Combinatorics" "HOL-Computational_Algebra" theories Analysis document_files "root.tex" "root.bib" session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] theories Complex_Analysis document_files "root.tex" "root.bib" session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" + theories Approximations Metric_Arith_Examples session "HOL-Homology" (timing) in Homology = "HOL-Analysis" + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] sessions "HOL-Algebra" theories Homology document_files "root.tex" session "HOL-Combinatorics" (main timing) in "Combinatorics" = "HOL" + sessions "HOL-Library" theories Combinatorics document_files "root.tex" session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" + theories Computational_Algebra (*conflicting type class instantiations and dependent applications*) Field_as_Ring session "HOL-Real_Asymp" in Real_Asymp = HOL + sessions "HOL-Decision_Procs" theories Real_Asymp Real_Asymp_Approx Real_Asymp_Examples session "HOL-Real_Asymp-Manual" in "Real_Asymp/Manual" = "HOL-Real_Asymp" + theories Real_Asymp_Doc document_files (in "~~/src/Doc") "iman.sty" "extra.sty" "isar.sty" document_files "root.tex" "style.sty" session "HOL-Hahn_Banach" in Hahn_Banach = HOL + description " Author: Gertrud Bauer, TU Munich The Hahn-Banach theorem for real vector spaces. This is the proof of the Hahn-Banach theorem for real vectorspaces, following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach theorem is one of the fundamental theorems of functional analysis. It is a conclusion of Zorn's lemma. Two different formaulations of the theorem are presented, one for general real vectorspaces and its application to normed vectorspaces. The theorem says, that every continous linearform, defined on arbitrary subspaces (not only one-dimensional subspaces), can be extended to a continous linearform on the whole vectorspace. " sessions "HOL-Analysis" theories Hahn_Banach document_files "root.bib" "root.tex" session "HOL-Induct" in Induct = HOL + description " Examples of (Co)Inductive Definitions. Comb proves the Church-Rosser theorem for combinators (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz). Mutil is the famous Mutilated Chess Board problem (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz). PropLog proves the completeness of a formalization of propositional logic (see http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz). Exp demonstrates the use of iterated inductive definitions to reason about mutually recursive relations. " sessions "HOL-Library" theories [quick_and_dirty] Common_Patterns theories Nested_Datatype QuoDataType QuoNestedDataType Term SList ABexp Infinitely_Branching_Tree Ordinals Sigma_Algebra Comb PropLog Com document_files "root.tex" session "HOL-IMP" (timing) in IMP = "HOL-Library" + options [document_variants = document] theories BExp ASM Finite_Reachable Denotational Compiler2 Poly_Types Sec_Typing Sec_TypingT Def_Init_Big Def_Init_Small Fold Live Live_True Hoare_Examples Hoare_Sound_Complete VCG Hoare_Total VCG_Total_EX VCG_Total_EX2 Collecting1 Collecting_Examples Abs_Int_Tests Abs_Int1_parity Abs_Int1_const Abs_Int3 Procs_Dyn_Vars_Dyn Procs_Stat_Vars_Dyn Procs_Stat_Vars_Stat C_like OO document_files "root.bib" "root.tex" session "HOL-IMPP" in IMPP = HOL + description \ Author: David von Oheimb Copyright 1999 TUM IMPP -- An imperative language with procedures. This is an extension of IMP with local variables and mutually recursive procedures. For documentation see "Hoare Logic for Mutual Recursion and Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). \ theories EvenOdd session "HOL-Data_Structures" (timing) in Data_Structures = HOL + options [document_variants = document] sessions "HOL-Number_Theory" theories [document = false] Less_False theories Sorting Balance Tree_Map Interval_Tree AVL_Map AVL_Bal_Set AVL_Bal2_Set Height_Balanced_Tree RBT_Set2 RBT_Map Tree23_Map Tree23_of_List Tree234_Map Brother12_Map AA_Map Set2_Join_RBT Array_Braun Trie_Fun Trie_Map Tries_Binary Queue_2Lists Heaps Leftist_Heap Binomial_Heap Selection document_files "root.tex" "root.bib" session "HOL-Import" in Import = HOL + theories HOL_Light_Maps theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" + description " Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity. " sessions "HOL-Algebra" theories Number_Theory document_files "root.tex" session "HOL-Hoare" in Hoare = HOL + description " Verification of imperative programs (verification conditions are generated automatically from pre/post conditions and loop invariants). " theories Examples ExamplesAbort ExamplesTC Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation document_files "root.bib" "root.tex" session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL + description " Verification of shared-variable imperative programs a la Owicki-Gries. (verification conditions are generated automatically). " theories Hoare_Parallel document_files "root.bib" "root.tex" session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" + sessions "HOL-Number_Theory" "HOL-Data_Structures" "HOL-Examples" theories Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Code_Lazy_Test Code_Test_PolyML Code_Test_Scala theories [condition = ISABELLE_GHC] Code_Test_GHC theories [condition = ISABELLE_MLTON] Code_Test_MLton theories [condition = ISABELLE_OCAMLFIND] Code_Test_OCaml theories [condition = ISABELLE_SMLNJ] Code_Test_SMLNJ session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" + description " Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Testing Metis and Sledgehammer. " sessions "HOL-Decision_Procs" theories Abstraction Big_O Binary_Tree Clausification Message Proxies Tarski Trans_Closure Sets session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL + description " Author: Jasmin Blanchette, TU Muenchen Copyright 2009 " options [kodkod_scala] sessions "HOL-Library" theories [quick_and_dirty] Nitpick_Examples session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" + description " Author: Clemens Ballarin, started 24 September 1999, and many others The Isabelle Algebraic Library. " sessions "HOL-Cardinals" "HOL-Combinatorics" theories (* Orders and Lattices *) Galois_Connection (* Knaster-Tarski theorem and Galois connections *) (* Groups *) FiniteProduct (* Product operator for commutative groups *) Sylow (* Sylow's theorem *) Bij (* Automorphism Groups *) Multiplicative_Group Zassenhaus (* The Zassenhaus lemma *) (* Rings *) Divisibility (* Rings *) IntRing (* Ideals and residue classes *) UnivPoly (* Polynomials *) (* Main theory *) Algebra document_files "root.bib" "root.tex" session "HOL-Auth" (timing) in Auth = HOL + description " A new approach to verifying authentication protocols. " sessions "HOL-Library" directories "Smartcard" "Guard" theories Auth_Shared Auth_Public "Smartcard/Auth_Smartcard" "Guard/Auth_Guard_Shared" "Guard/Auth_Guard_Public" document_files "root.tex" session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" + description " Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge Verifying security protocols using Chandy and Misra's UNITY formalism. " directories "Simple" "Comp" theories (*Basic meta-theory*) UNITY_Main (*Simple examples: no composition*) "Simple/Deadlock" "Simple/Common" "Simple/Network" "Simple/Token" "Simple/Channel" "Simple/Lift" "Simple/Mutex" "Simple/Reach" "Simple/Reachability" (*Verifying security protocols using UNITY*) "Simple/NSP_Bad" (*Example of composition*) "Comp/Handshake" (*Universal properties examples*) "Comp/Counter" "Comp/Counterc" "Comp/Priority" "Comp/TimerArray" "Comp/Progress" "Comp/Alloc" "Comp/AllocImpl" "Comp/Client" (*obsolete*) ELT document_files "root.tex" session "HOL-Unix" in Unix = HOL + options [print_mode = "no_brackets,no_type_brackets"] sessions "HOL-Library" theories Unix document_files "root.bib" "root.tex" session "HOL-ZF" in ZF = HOL + sessions "HOL-Library" theories MainZF Games document_files "root.tex" session "HOL-Imperative_HOL" (timing) in Imperative_HOL = HOL + options [print_mode = "iff,no_brackets"] sessions "HOL-Library" directories "ex" theories Imperative_HOL_ex document_files "root.bib" "root.tex" session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" + description " Various decision procedures, typically involving reflection. " directories "ex" theories Decision_Procs session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + sessions "HOL-Examples" theories Hilbert_Classical Proof_Terms XML_Data session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" + description " Examples for program extraction in Higher-Order Logic. " options [quick_and_dirty = false] sessions "HOL-Computational_Algebra" theories Greatest_Common_Divisor Warshall Higman_Extraction Pigeonhole Euclid document_files "root.bib" "root.tex" session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" + description \ Lambda Calculus in de Bruijn's Notation. This session defines lambda-calculus terms with de Bruijn indixes and proves confluence of beta, eta and beta+eta. The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html). \ options [print_mode = "no_brackets", quick_and_dirty = false] sessions "HOL-Library" theories Eta StrongNorm Standardization WeakNorm document_files "root.bib" "root.tex" session "HOL-Prolog" in Prolog = HOL + description " Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) A bare-bones implementation of Lambda-Prolog. This is a simple exploratory implementation of Lambda-Prolog in HOL, including some minimal examples (in Test.thy) and a more typical example of a little functional language and its type system. " theories Test Type session "HOL-MicroJava" (timing) in MicroJava = HOL + description " Formalization of a fragment of Java, together with a corresponding virtual machine and a specification of its bytecode verifier and a lightweight bytecode verifier, including proofs of type-safety. " sessions "HOL-Library" "HOL-Eisbach" directories "BV" "Comp" "DFA" "J" "JVM" theories MicroJava document_files "introduction.tex" "root.bib" "root.tex" session "HOL-NanoJava" in NanoJava = HOL + description " Hoare Logic for a tiny fragment of Java. " theories Example document_files "root.bib" "root.tex" session "HOL-Bali" (timing) in Bali = HOL + sessions "HOL-Library" theories AxExample AxSound AxCompl Trans TypeSafe document_files "root.tex" session "HOL-IOA" in IOA = HOL + description \ Author: Tobias Nipkow and Konrad Slind and Olaf Müller Copyright 1994--1996 TU Muenchen The meta-theory of I/O-Automata in HOL. This formalization has been significantly changed and extended, see HOLCF/IOA. There are also the proofs of two communication protocols which formerly have been here. @inproceedings{Nipkow-Slind-IOA, author={Tobias Nipkow and Konrad Slind}, title={{I/O} Automata in {Isabelle/HOL}}, booktitle={Proc.\ TYPES Workshop 1994}, publisher=Springer, series=LNCS, note={To appear}} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz and @inproceedings{Mueller-Nipkow, author={Olaf M\"uller and Tobias Nipkow}, title={Combining Model Checking and Deduction for {I/O}-Automata}, booktitle={Proc.\ TACAS Workshop}, organization={Aarhus University, BRICS report}, year=1995} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz \ theories Solve session "HOL-Lattice" in Lattice = HOL + description " Author: Markus Wenzel, TU Muenchen Basic theory of lattices and orders. " theories CompleteLattice document_files "root.tex" session "HOL-ex" (timing) in ex = "HOL-Number_Theory" + description " Miscellaneous examples for Higher-Order Logic. " theories Antiquote Argo_Examples Arith_Examples Ballot BinEx Birthday_Paradox Bit_Lists Bubblesort CTL Cartouche_Examples Case_Product Chinese Classical Code_Binary_Nat_examples Code_Lazy_Demo Code_Timing Coercion_Examples Computations Conditional_Parametricity_Examples Cubic_Quartic Datatype_Record_Examples Dedekind_Real Erdoes_Szekeres Eval_Examples Executable_Relation Execute_Choice Functions Function_Growth Gauge_Integration Guess HarmonicSeries Hebrew Hex_Bin_Examples IArray_Examples Intuitionistic Join_Theory Lagrange List_to_Set_Comprehension_Examples LocaleTest2 MergeSort MonoidGroup Multiquote NatSum Normalization_by_Evaluation PER Parallel_Example Peano_Axioms Perm_Fragments PresburgerEx Primrec Pythagoras Quicksort Radix_Sort Reflection_Examples Refute_Examples Residue_Ring Rewrite_Examples SOS SOS_Cert Serbian Set_Comprehension_Pointfree_Examples Set_Theory Simproc_Tests Simps_Case_Conv_Examples Sketch_and_Explore Sorting_Algorithms_Examples Specifications_with_bundle_mixins Sqrt Sqrt_Script Sudoku Sum_of_Powers Tarski Termination ThreeDivides Transfer_Debug Transfer_Int_Nat Transitive_Closure_Table_Ex Tree23 Triangular_Numbers Unification While_Combinator_Example veriT_Preprocessing theories [skip_proofs = false] SAT_Examples Meson_Test session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" + description " Miscellaneous Isabelle/Isar examples. " options [quick_and_dirty] sessions "HOL-Hoare" theories Structured_Statements Basic_Logic Expr_Compiler Fibonacci Group Group_Context Group_Notepad Hoare_Ex Mutilated_Checkerboard Puzzle Summation document_files "root.bib" "root.tex" session "HOL-Eisbach" in Eisbach = HOL + description \ The Eisbach proof method language and "match" method. \ sessions FOL "HOL-Analysis" theories Eisbach Tests Examples Examples_FOL Example_Metric session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL + description " Verification of the SET Protocol. " sessions "HOL-Library" theories SET_Protocol document_files "root.tex" session "HOL-Matrix_LP" in Matrix_LP = HOL + description " Two-dimensional matrices and linear programming. " sessions "HOL-Library" directories "Compute_Oracle" theories Cplex document_files "root.tex" session "HOL-TLA" in TLA = HOL + description " Lamport's Temporal Logic of Actions. " theories TLA session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" + theories Inc session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" + theories DBuffer session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" + theories MemoryImplementation session "HOL-TPTP" in TPTP = HOL + description " Author: Jasmin Blanchette, TU Muenchen Author: Nik Sultana, University of Cambridge Copyright 2011 TPTP-related extensions. " sessions "HOL-Library" theories ATP_Theory_Export MaSh_Eval TPTP_Interpret THF_Arith TPTP_Proof_Reconstruction theories ATP_Problem_Import session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" + sessions "HOL-Combinatorics" theories Probability document_files "root.tex" session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" + theories Dining_Cryptographers Koepf_Duermuth_Countermeasure Measure_Not_CCC session "HOL-Nominal" in Nominal = HOL + sessions "HOL-Library" theories Nominal session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" + theories Class3 CK_Machine Compile Contexts Crary CR_Takahashi CR Fsub Height Lambda_mu Lam_Funs LocalWeakening Pattern SN SOS Standardization Support Type_Preservation Weakening W theories [quick_and_dirty] VC_Condition session "HOL-Cardinals" (timing) in Cardinals = HOL + description " Ordinals and Cardinals, Full Theories. " theories Cardinals Bounded_Set document_files "intro.tex" "root.tex" "root.bib" session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" + description " (Co)datatype Examples. " directories "Derivation_Trees" theories Compat Lambda_Term Process TreeFsetI "Derivation_Trees/Gram_Lang" "Derivation_Trees/Parallel_Composition" Koenig Lift_BNF Milner_Tofte Stream_Processor Cyclic_List Free_Idempotent_Monoid Regex_ACI Regex_ACIDZ TLList FAE_Sequence Misc_Codatatype Misc_Datatype Misc_Primcorec Misc_Primrec Datatype_Simproc_Tests session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" + description " Corecursion Examples. " directories "Tests" theories LFilter Paper_Examples Stream_Processor "Tests/Simple_Nesting" "Tests/Iterate_GPV" theories [quick_and_dirty] "Tests/GPV_Bare_Bones" "Tests/Merge_D" "Tests/Merge_Poly" "Tests/Misc_Mono" "Tests/Misc_Poly" "Tests/Small_Concrete" "Tests/Stream_Friends" "Tests/TLList_Friends" "Tests/Type_Class" session "HOL-Statespace" in Statespace = HOL + theories [skip_proofs = false] StateSpaceEx document_files "root.tex" session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" + description " Nonstandard analysis. " theories Nonstandard_Analysis document_files "root.tex" session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" + theories NSPrimes -session "HOL-Mirabelle" in Mirabelle = HOL + - theories Mirabelle_Test - -session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" + - options [timeout = 60] - theories Ex +session "HOL-Mirabelle-ex" in "Tools/Mirabelle" = HOL + + description "Some arbitrary small test case for Mirabelle." + options [timeout = 60, mirabelle_actions = "arith"] + sessions + "HOL-Analysis" + theories + "HOL-Analysis.Inner_Product" session "HOL-SMT_Examples" (timing) in SMT_Examples = HOL + options [quick_and_dirty] sessions "HOL-Library" theories Boogie SMT_Examples SMT_Word_Examples SMT_Examples_Verit SMT_Tests_Verit theories [condition = Z3_INSTALLED] SMT_Tests session "HOL-SPARK" in "SPARK" = HOL + sessions "HOL-Library" theories SPARK session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" + directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt" theories "Gcd/Greatest_Common_Divisor" "Liseq/Longest_Increasing_Subsequence" "RIPEMD-160/F" "RIPEMD-160/Hash" "RIPEMD-160/K_L" "RIPEMD-160/K_R" "RIPEMD-160/R_L" "RIPEMD-160/Round" "RIPEMD-160/R_R" "RIPEMD-160/S_L" "RIPEMD-160/S_R" "Sqrt/Sqrt" export_files (in ".") "*:**.prv" session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" + options [show_question_marks = false] sessions "HOL-Library" "HOL-SPARK-Examples" theories Example_Verification VC_Principles Reference Complex_Types document_theories "HOL-SPARK-Examples.Greatest_Common_Divisor" document_files "complex_types.ads" "complex_types_app.adb" "complex_types_app.ads" "Gcd.adb" "Gcd.ads" "intro.tex" "loop_invariant.adb" "loop_invariant.ads" "root.bib" "root.tex" "Simple_Gcd.adb" "Simple_Gcd.ads" session "HOL-Mutabelle" in Mutabelle = HOL + sessions "HOL-Library" theories MutabelleExtra session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = HOL + sessions "HOL-Library" theories Quickcheck_Examples Quickcheck_Lattice_Examples Completeness Quickcheck_Interfaces Quickcheck_Nesting_Example theories [condition = ISABELLE_GHC] Hotel_Example Quickcheck_Narrowing_Examples session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" + description " Author: Cezary Kaliszyk and Christian Urban " theories DList Quotient_FSet Quotient_Int Quotient_Message Lift_FSet Lift_Set Lift_Fun Quotient_Rat Lift_DList Int_Pow Lifting_Code_Dt_Test session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL + sessions "HOL-Library" theories Examples Predicate_Compile_Tests Predicate_Compile_Quickcheck_Examples Specialisation_Examples IMP_1 IMP_2 (* FIXME since 21-Jul-2011 Hotel_Example_Small_Generator *) IMP_3 IMP_4 theories [condition = ISABELLE_SWIPL] Code_Prolog_Examples Context_Free_Grammar_Example Hotel_Example_Prolog Lambda_Example List_Examples theories [condition = ISABELLE_SWIPL, quick_and_dirty] Reg_Exp_Example session "HOL-Types_To_Sets" in Types_To_Sets = HOL + description " Experimental extension of Higher-Order Logic to allow translation of types to sets. " directories "Examples" theories Types_To_Sets "Examples/Prerequisites" "Examples/Finite" "Examples/T2_Spaces" "Examples/Unoverload_Def" "Examples/Linear_Algebra_On" session HOLCF (main timing) in HOLCF = HOL + description " Author: Franz Regensburger Author: Brian Huffman HOLCF -- a semantic extension of HOL by the LCF logic. " sessions "HOL-Library" theories HOLCF (global) document_files "root.tex" session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF + theories Domain_ex Fixrec_ex New_Domain document_files "root.tex" session "HOLCF-Library" in "HOLCF/Library" = HOLCF + theories HOLCF_Library HOL_Cpo session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF + description " IMP -- A WHILE-language and its Semantics. This is the HOLCF-based denotational semantics of a simple WHILE-language. " sessions "HOL-IMP" theories HoareEx document_files "isaverbatimwrite.sty" "root.tex" "root.bib" session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" + description " Miscellaneous examples for HOLCF. " theories Dnat Dagstuhl Focus_ex Fix2 Hoare Concurrency_Monad Loop Powerdomain_ex Domain_Proofs Letrec Pattern_Match session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" + description \ FOCUS: a theory of stream-processing functions Isabelle/HOLCF. For introductions to FOCUS, see "The Design of Distributed Systems - An Introduction to FOCUS" http://www4.in.tum.de/publ/html.php?e=2 "Specification and Refinement of a Buffer of Length One" http://www4.in.tum.de/publ/html.php?e=15 "Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321 \ theories Fstreams FOCUS Buffer_adm session IOA (timing) in "HOLCF/IOA" = HOLCF + description " Author: Olaf Müller Copyright 1997 TU München A formalization of I/O automata in HOLCF. The distribution contains simulation relations, temporal logic, and an abstraction theory. Everything is based upon a domain-theoretic model of finite and infinite sequences. " theories Abstraction session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA + description " Author: Olaf Müller The Alternating Bit Protocol performed in I/O-Automata: combining IOA with Model Checking. Theory Correctness contains the proof of the abstraction from unbounded channels to finite ones. File Check.ML contains a simple ModelChecker prototype checking Spec against the finite version of the ABP-protocol. " theories Correctness Spec session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA + description " Author: Tobias Nipkow & Konrad Slind A network transmission protocol, performed in the I/O automata formalization by Olaf Müller. " theories Overview Correctness session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA + description " Author: Olaf Müller Memory storage case study. " theories Correctness session "IOA-ex" in "HOLCF/IOA/ex" = IOA + description " Author: Olaf Müller " theories TrivEx TrivEx2 diff --git a/src/HOL/Mirabelle/Tools/mirabelle.ML b/src/HOL/Tools/Mirabelle/mirabelle.ML rename from src/HOL/Mirabelle/Tools/mirabelle.ML rename to src/HOL/Tools/Mirabelle/mirabelle.ML --- a/src/HOL/Mirabelle/Tools/mirabelle.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle.ML @@ -1,223 +1,241 @@ (* Title: HOL/Mirabelle/Tools/mirabelle.ML Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Makarius *) signature MIRABELLE = sig - (*configuration*) - val logfile : string Config.T - val timeout : int Config.T - val start_line : int Config.T - val end_line : int Config.T - (*core*) - type init_action = int -> theory -> theory - type done_args = {last: Toplevel.state, log: string -> unit} - type done_action = int -> done_args -> unit - type run_args = {pre: Proof.state, post: Toplevel.state option, - timeout: Time.time, log: string -> unit, pos: Position.T, name: string} - type run_action = int -> run_args -> unit - type action = init_action * run_action * done_action - val catch : (int -> string) -> run_action -> run_action - val catch_result : (int -> string) -> 'a -> (int -> run_args -> 'a) -> - int -> run_args -> 'a - val register : action -> theory -> theory - val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state -> - unit + val print_name: string -> string + val print_properties: Properties.T -> string + type context = {tag: string, arguments: Properties.T, timeout: Time.time, theory: theory} + type command = {name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state} + val command_result: command -> XML.body -> XML.tree + val print_exn: exn -> string + val theory_action: binding -> (context -> command list -> XML.body) -> theory -> theory + val command_action: binding -> (context -> command -> string) -> theory -> theory (*utility functions*) val can_apply : Time.time -> (Proof.context -> int -> tactic) -> Proof.state -> bool val theorems_in_proof_term : theory -> thm -> thm list - val theorems_of_sucessful_proof : Toplevel.state option -> thm list - val get_setting : (string * string) list -> string * string -> string - val get_int_setting : (string * string) list -> string * int -> int - val get_bool_setting : (string * string) list -> string * bool -> bool + val theorems_of_sucessful_proof: Toplevel.state -> thm list + val get_argument : (string * string) list -> string * string -> string + val get_int_argument : (string * string) list -> string * int -> int + val get_bool_argument : (string * string) list -> string * bool -> bool val cpu_time : ('a -> 'b) -> 'a -> 'b * int end - - structure Mirabelle : MIRABELLE = struct -(* Mirabelle configuration *) +(** Mirabelle core **) -val logfile = Attrib.setup_config_string \<^binding>\mirabelle_logfile\ (K "") -val timeout = Attrib.setup_config_int \<^binding>\mirabelle_timeout\ (K 30) -val start_line = Attrib.setup_config_int \<^binding>\mirabelle_start_line\ (K 0) -val end_line = Attrib.setup_config_int \<^binding>\mirabelle_end_line\ (K ~1) +(* concrete syntax *) + +val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords \<^theory>); + +val print_name = Token.print_name keywords; +val print_properties = Token.print_properties keywords; + +fun print_action name [] = name + | print_action name arguments = name ^ " " ^ print_properties arguments; + +fun read_actions str = + Token.read_body keywords + (Parse.enum ";" (Parse.name -- Sledgehammer_Commands.parse_params)) + (Symbol_Pos.explode0 str); -(* Mirabelle core *) +(* actions *) -type init_action = int -> theory -> theory -type done_args = {last: Toplevel.state, log: string -> unit} -type done_action = int -> done_args -> unit -type run_args = {pre: Proof.state, post: Toplevel.state option, - timeout: Time.time, log: string -> unit, pos: Position.T, name: string} -type run_action = int -> run_args -> unit -type action = init_action * run_action * done_action +type command = {name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}; +type context = {tag: string, arguments: Properties.T, timeout: Time.time, theory: theory}; -structure Actions = Theory_Data +structure Data = Theory_Data ( - type T = (int * run_action * done_action) list - val empty = [] - val extend = I - fun merge data = Library.merge (K true) data (* FIXME potential data loss because of (K true) *) -) + type T = (context -> command list -> XML.body) Name_Space.table; + val empty = Name_Space.empty_table "mirabelle_action"; + val extend = I; + val merge = Name_Space.merge_tables; +); + +fun theory_action binding action thy = + let val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming); + in thy |> Data.map (#2 o Name_Space.define context true (binding, action)) end; + +fun apply_action index name arguments timeout commands thy = + let + val action = #2 (Name_Space.check (Context.Theory thy) (Data.get thy) (name, Position.none)); + val tag = "#" ^ Value.print_int index ^ " " ^ name ^ ": "; + val context = {tag = tag, arguments = arguments, timeout = timeout, theory = thy}; + val export_body = action context commands; + val export_head = + XML.Elem (("action", (Markup.nameN, name) :: arguments), + [XML.Text (print_action name arguments)]); + val export_path = Path.binding0 (Path.basic "mirabelle" + Path.basic (Value.print_int index)); + in Export.export thy export_path (export_head :: export_body) end; -fun exn_log tag id e = tag id ^ "exception:\n" ^ General.exnMessage e - -fun catch tag f id (args: run_args) = f id args - handle exn => - if Exn.is_interrupt exn then Exn.reraise exn else #log args (exn_log tag id exn) +(* command action *) -fun catch_result tag default f id (args: run_args) = f id args - handle exn => - if Exn.is_interrupt exn then Exn.reraise exn else (#log args (exn_log tag id exn); default) +fun command_result ({name, pos, ...}: command) body = + XML.Elem (("command", (Markup.nameN, name) :: Position.properties_of pos), body); -fun register (init, run, done) thy = - let val id = length (Actions.get thy) + 1 - in - thy - |> init id - |> Actions.map (cons (id, run, done)) - end +fun print_exn exn = + (case exn of + Timeout.TIMEOUT _ => "timeout" + | ERROR msg => "error: " ^ msg + | exn => "exception:\n" ^ General.exnMessage exn); + +fun command_action binding action = + let + fun apply context command = + let val s = + action context command handle exn => + if Exn.is_interrupt exn then Exn.reraise exn + else #tag context ^ print_exn exn; + in + if s = "" then NONE + else SOME (command_result command [XML.Text s]) end; + in theory_action binding (map_filter o apply) end; + + +(* theory line range *) local -fun log thy s = - let fun append_to n = if n = "" then K () else File.append (Path.explode n) - in append_to (Config.get_global thy logfile) (s ^ "\n") end - (* FIXME: with multithreading and parallel proofs enabled, we might need to - encapsulate this inside a critical section *) - -fun log_sep thy = log thy "------------------" +val theory_name = + Scan.many1 (Symbol_Pos.symbol #> (fn s => Symbol.not_eof s andalso s <> "[")) + >> Symbol_Pos.content; -fun apply_actions thy pos name info (pre, post, time) actions = - let - fun apply f = f {pre=pre, post=post, timeout=time, log=log thy, pos=pos, name=name} - fun run (id, run, _) = (apply (run id); log_sep thy) - in (log thy info; log_sep thy; List.app run actions) end - -fun in_range _ _ NONE = true - | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r)) - -fun only_within_range thy pos f x = - let val l = Config.get_global thy start_line and r = Config.get_global thy end_line - in if in_range l r (Position.line_of pos) then f x else () end +val line = Symbol_Pos.scan_nat >> (Symbol_Pos.content #> Value.parse_nat); +val end_line = Symbol_Pos.$$ ":" |-- line; +val range = Symbol_Pos.$$ "[" |-- line -- Scan.option end_line --| Symbol_Pos.$$ "]"; in -fun run_actions tr pre post = - let - val thy = Proof.theory_of pre - val pos = Toplevel.pos_of tr - val name = Toplevel.name_of tr - val st = (pre, post, Time.fromSeconds (Config.get_global thy timeout)) +fun read_theory_range str = + (case Scan.read Symbol_Pos.stopper (theory_name -- Scan.option range) (Symbol_Pos.explode0 str) of + SOME res => res + | NONE => error ("Malformed specification of theory line range: " ^ quote str)); - val str0 = string_of_int o the_default 0 - val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) - val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):" - in - only_within_range thy pos (apply_actions thy pos name info st) (Actions.get thy) - end +end; -fun done_actions st = +fun check_theories strs = let - val thy = Toplevel.theory_of st - val _ = log thy "\n\n"; - in - thy - |> Actions.get - |> List.app (fn (id, _, done) => done id {last=st, log=log thy}) - end - -end + val theories = map read_theory_range strs; + fun get_theory name = + if null theories then SOME NONE + else get_first (fn (a, b) => if a = name then SOME b else NONE) theories; + fun check_line NONE _ = false + | check_line _ NONE = true + | check_line (SOME NONE) _ = true + | check_line (SOME (SOME (line, NONE))) (SOME i) = line <= i + | check_line (SOME (SOME (line, SOME end_line))) (SOME i) = line <= i andalso i <= end_line; + fun check_pos range = check_line range o Position.line_of; + in check_pos o get_theory end; -val whitelist = ["apply", "by", "proof"] -fun step_hook tr pre post = - (* FIXME: might require wrapping into "interruptible" *) - if can (Proof.assert_backward o Toplevel.proof_of) pre andalso - member (op =) whitelist (Toplevel.name_of tr) - then run_actions tr (Toplevel.proof_of pre) (SOME post) - else if not (Toplevel.is_toplevel pre) andalso Toplevel.is_toplevel post - then done_actions pre - else () (* FIXME: add theory_hook here *) +(* presentation hook *) +val whitelist = ["apply", "by", "proof"]; + +val _ = + Theory.setup (Thy_Info.add_presentation (fn context => fn thy => + let + val {options, adjust_pos, segments, ...} = context; + val mirabelle_timeout = Options.seconds options \<^system_option>\mirabelle_timeout\; + val mirabelle_actions = Options.string options \<^system_option>\mirabelle_actions\; + val mirabelle_theories = Options.string options \<^system_option>\mirabelle_theories\; + + val actions = + (case read_actions mirabelle_actions of + SOME actions => actions + | NONE => error ("Failed to parse mirabelle_actions: " ^ quote mirabelle_actions)); + val check = check_theories (space_explode "," mirabelle_theories); + val commands = + segments |> map_filter (fn {command = tr, prev_state = st, state = st', ...} => + let + val name = Toplevel.name_of tr; + val pos = adjust_pos (Toplevel.pos_of tr); + in + if can (Proof.assert_backward o Toplevel.proof_of) st andalso + member (op =) whitelist name andalso + check (Context.theory_long_name thy) pos + then SOME {name = name, pos = pos, pre = Toplevel.proof_of st, post = st'} + else NONE + end); + + fun apply (i, (name, arguments)) () = + apply_action (i + 1) name arguments mirabelle_timeout commands thy; + in if null commands then () else fold_index apply actions () end)); (* Mirabelle utility functions *) fun can_apply time tac st = let - val {context = ctxt, facts, goal} = Proof.goal st - val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt) + val {context = ctxt, facts, goal} = Proof.goal st; + val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt); in (case try (Timeout.apply time (Seq.pull o full_tac)) goal of SOME (SOME _) => true | _ => false) - end + end; local fun fold_body_thms f = let fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) => fn (x, seen) => if Inttab.defined seen i then (x, seen) else let - val name = Proofterm.thm_node_name thm_node - val prop = Proofterm.thm_node_prop thm_node - val body = Future.join (Proofterm.thm_node_body thm_node) - val (x', seen') = app (n + (if name = "" then 0 else 1)) body - (x, Inttab.update (i, ()) seen) - in (x' |> n = 0 ? f (name, prop, body), seen') end) - in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end + val name = Proofterm.thm_node_name thm_node; + val prop = Proofterm.thm_node_prop thm_node; + val body = Future.join (Proofterm.thm_node_body thm_node); + val (x', seen') = + app (n + (if name = "" then 0 else 1)) body + (x, Inttab.update (i, ()) seen); + in (x' |> n = 0 ? f (name, prop, body), seen') end); + in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end; in fun theorems_in_proof_term thy thm = let - val all_thms = Global_Theory.all_thms_of thy true - fun collect (s, _, _) = if s <> "" then insert (op =) s else I - fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE - fun resolve_thms names = map_filter (member_of names) all_thms - in - resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) - end - -end + val all_thms = Global_Theory.all_thms_of thy true; + fun collect (s, _, _) = if s <> "" then insert (op =) s else I; + fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE; + fun resolve_thms names = map_filter (member_of names) all_thms; + in resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) end; -fun theorems_of_sucessful_proof state = - (case state of +end; + +fun theorems_of_sucessful_proof st = + (case try Toplevel.proof_of st of NONE => [] - | SOME st => - if not (Toplevel.is_proof st) then [] - else - theorems_in_proof_term (Toplevel.theory_of st) (#goal (Proof.goal (Toplevel.proof_of st)))) + | SOME prf => theorems_in_proof_term (Proof.theory_of prf) (#goal (Proof.goal prf))); -fun get_setting settings (key, default) = - the_default default (AList.lookup (op =) settings key) +fun get_argument arguments (key, default) = + the_default default (AList.lookup (op =) arguments key); -fun get_int_setting settings (key, default) = - (case Option.map Int.fromString (AList.lookup (op =) settings key) of +fun get_int_argument arguments (key, default) = + (case Option.map Int.fromString (AList.lookup (op =) arguments key) of SOME (SOME i) => i | SOME NONE => error ("bad option: " ^ key) - | NONE => default) + | NONE => default); -fun get_bool_setting settings (key, default) = - (case Option.map Bool.fromString (AList.lookup (op =) settings key) of +fun get_bool_argument arguments (key, default) = + (case Option.map Bool.fromString (AList.lookup (op =) arguments key) of SOME (SOME i) => i | SOME NONE => error ("bad option: " ^ key) - | NONE => default) + | NONE => default); fun cpu_time f x = let val ({cpu, ...}, y) = Timing.timing f x - in (y, Time.toMilliseconds cpu) end + in (y, Time.toMilliseconds cpu) end; end diff --git a/src/HOL/Tools/Mirabelle/mirabelle.scala b/src/HOL/Tools/Mirabelle/mirabelle.scala new file mode 100644 --- /dev/null +++ b/src/HOL/Tools/Mirabelle/mirabelle.scala @@ -0,0 +1,264 @@ +/* Title: HOL/Tools/Mirabelle/mirabelle.scala + Author: Makarius + +Isabelle/Scala front-end for Mirabelle. +*/ + +package isabelle.mirabelle + +import isabelle._ + + +object Mirabelle +{ + /* actions and options */ + + def action_names(): List[String] = + { + val Pattern = """Mirabelle action: "(\w+)".*""".r + (for { + file <- + File.find_files(Path.explode("~~/src/HOL/Tools/Mirabelle").file, + pred = _.getName.endsWith(".ML")) + line <- split_lines(File.read(file)) + name <- line match { case Pattern(a) => Some(a) case _ => None } + } yield name).sorted + } + + def sledgehammer_options(): List[String] = + { + val Pattern = """val .*K *= *"(.*)" *\(\*(.*)\*\)""".r + split_lines(File.read(Path.explode("~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML"))). + flatMap(line => line match { case Pattern(a, b) => Some (a + b) case _ => None }) + } + + + /* exported content */ + + val separator = "------------------\n" + + def mirabelle_path(index: Int): String = "mirabelle/" + index + + object Action + { + def get(export_name: String, xml: XML.Tree): Action = + xml match { + case XML.Elem(Markup("action", (Markup.NAME, name) :: arguments), body) => + Action(name, arguments, body) + case _ => + error("Expected action in export " + quote(export_name) + "\nmalformed XML: " + xml) + } + } + case class Action(name: String, arguments: Properties.T, body: XML.Body) + { + def print: String = XML.content(body) + } + + object Command + { + def get(export_name: String, xml: XML.Tree): Command = + xml match { + case XML.Elem(Markup("command", (Markup.NAME, name) :: props), result) => + Command(name, props.filter(Markup.position_property), result) + case _ => + error("Expected command in export " + quote(export_name) + "\nmalformed XML: " + xml) + } + } + sealed case class Command(name: String, pos: Properties.T, result: XML.Body) + { + def print_head: String = + { + val line = Position.Line.get(pos) + val offset = Position.Offset.get(pos) + val loc = line.toString + ":" + offset.toString + "at " + loc + " (" + name + "):\n" + } + def print_body: String = Pretty.string_of(result) + def print: String = "\n\n" + print_head + separator + print_body + } + + + /* main mirabelle */ + + def mirabelle( + options: Options, + actions: List[String], + output_dir: Path, + theories: List[String] = Nil, + selection: Sessions.Selection = Sessions.Selection.empty, + progress: Progress = new Progress, + dirs: List[Path] = Nil, + select_dirs: List[Path] = Nil, + numa_shuffling: Boolean = false, + max_jobs: Int = 1, + verbose: Boolean = false): Build.Results = + { + val build_options = + options + "parallel_presentation=false" + + ("mirabelle_actions=" + actions.mkString(";")) + + ("mirabelle_theories=" + theories.mkString(",")) + + val build_results = + Build.build(build_options, clean_build = true, + selection = selection, progress = progress, dirs = dirs, select_dirs = select_dirs, + numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = verbose) + + if (build_results.ok) { + val structure = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs) + val store = Sessions.store(build_options) + + using(store.open_database_context())(db_context => + { + var seen_theories = Set.empty[String] + for { + session <- structure.imports_selection(selection).iterator + session_hierarchy = structure.hierarchy(session) + theories <- db_context.input_database(session)((db, a) => Some(store.read_theories(db, a))) + theory <- theories + if !seen_theories(theory) + index <- 1 to actions.length + export <- db_context.read_export(session_hierarchy, theory, mirabelle_path(index)) + body = export.uncompressed_yxml + if body.nonEmpty + } { + seen_theories += theory + val export_name = Export.compound_name(theory, mirabelle_path(index)) + val (action, commands) = + (Action.get(export_name, body.head), body.tail.map(Command.get(export_name, _))) + val dir = Isabelle_System.make_directory(output_dir + Path.basic(theory)) + val log_file = dir + Path.basic("mirabelle" + index).log + progress.echo("Writing " + log_file) + File.write(log_file, terminate_lines(action.print :: commands.map(_.print))) + } + }) + } + + build_results + } + + + /* Isabelle tool wrapper */ + + val default_output_dir: Path = Path.explode("mirabelle") + + val isabelle_tool = Isabelle_Tool("mirabelle", "testing tool for automated proof tools", + Scala_Project.here, args => + { + val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")) + + var actions: List[String] = Nil + var base_sessions: List[String] = Nil + var select_dirs: List[Path] = Nil + var numa_shuffling = false + var output_dir = default_output_dir + var requirements = false + var theories: List[String] = Nil + var exclude_session_groups: List[String] = Nil + var all_sessions = false + var dirs: List[Path] = Nil + var session_groups: List[String] = Nil + var max_jobs = 1 + var options = Options.init(opts = build_options) + var verbose = false + var exclude_sessions: List[String] = Nil + + val default_timeout = options.seconds("mirabelle_timeout") + + val getopts = Getopts(""" +Usage: isabelle mirabelle [OPTIONS] [SESSIONS ...] + + Options are: + -A ACTION add to list of actions + -B NAME include session NAME and all descendants + -D DIR include session directory and select its sessions + -N cyclic shuffling of NUMA CPU nodes (performance tuning) + -O DIR output directory for log files (default: """ + default_output_dir + """, + -R refer to requirements of selected sessions + -T THEORY theory restriction: NAME or NAME[LINE:END_LINE] + -X NAME exclude sessions from group NAME and all descendants + -a select all sessions + -d DIR include session directory + -g NAME select session group NAME + -j INT maximum number of parallel jobs (default 1) + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -t SECONDS timeout for each action (default """ + default_timeout + """) + -v verbose + -x NAME exclude session NAME and all descendants + + Apply the given actions at all theories and proof steps of the + specified sessions. + + The absence of theory restrictions (option -T) means to check all + theories fully. Otherwise only the named theories are checked. + + Each ACTION is either of the form NAME or NAME [OPTION, ...] + following Isabelle/Isar outer syntax. + + Available actions are:""" + action_names().mkString("\n ", "\n ", "") + """ + + For the ACTION "sledgehammer", the following OPTIONs are available:""" + + sledgehammer_options().mkString("\n ", "\n ", "\n"), + "A:" -> (arg => actions = actions ::: List(arg)), + "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), + "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), + "N" -> (_ => numa_shuffling = true), + "O:" -> (arg => output_dir = Path.explode(arg)), + "R" -> (_ => requirements = true), + "T:" -> (arg => theories = theories ::: List(arg)), + "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), + "a" -> (_ => all_sessions = true), + "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), + "g:" -> (arg => session_groups = session_groups ::: List(arg)), + "j:" -> (arg => max_jobs = Value.Int.parse(arg)), + "o:" -> (arg => options = options + arg), + "t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)), + "v" -> (_ => verbose = true), + "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) + + val sessions = getopts(args) + + if (actions.isEmpty) error("Missing actions (option -A)") + + val progress = new Console_Progress(verbose = verbose) + + val start_date = Date.now() + + if (verbose) { + progress.echo("Started at " + Build_Log.print_date(start_date)) + } + + val results = + progress.interrupt_handler { + mirabelle(options, actions, output_dir, + theories = theories, + selection = Sessions.Selection( + requirements = requirements, + all_sessions = all_sessions, + base_sessions = base_sessions, + exclude_session_groups = exclude_session_groups, + exclude_sessions = exclude_sessions, + session_groups = session_groups, + sessions = sessions), + progress = progress, + dirs = dirs, + select_dirs = select_dirs, + numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling), + max_jobs = max_jobs, + verbose = verbose) + } + + val end_date = Date.now() + val elapsed_time = end_date.time - start_date.time + + if (verbose) { + progress.echo("\nFinished at " + Build_Log.print_date(end_date)) + } + + val total_timing = + results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _). + copy(elapsed = elapsed_time) + progress.echo(total_timing.message_resources) + + sys.exit(results.rc) + }) +} diff --git a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML rename from src/HOL/Mirabelle/Tools/mirabelle_arith.ML rename to src/HOL/Tools/Mirabelle/mirabelle_arith.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML @@ -1,21 +1,17 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_arith.ML Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Makarius + +Mirabelle action: "arith". *) -structure Mirabelle_Arith : MIRABELLE_ACTION = +structure Mirabelle_Arith: sig end = struct -fun arith_tag id = "#" ^ string_of_int id ^ " arith: " - -fun init _ = I -fun done _ _ = () - -fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) = - if Mirabelle.can_apply timeout Arith_Data.arith_tac pre - then log (arith_tag id ^ "succeeded") - else () - handle Timeout.TIMEOUT _ => log (arith_tag id ^ "timeout") - -fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done) +val _ = + Theory.setup (Mirabelle.command_action \<^binding>\arith\ + (fn {timeout, ...} => fn {pre, ...} => + if Mirabelle.can_apply timeout Arith_Data.arith_tac pre + then "succeeded" else "")); end diff --git a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML rename from src/HOL/Mirabelle/Tools/mirabelle_metis.ML rename to src/HOL/Tools/Mirabelle/mirabelle_metis.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML @@ -1,35 +1,23 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_metis.ML Author: Jasmin Blanchette and Sascha Boehme, TU Munich + +Mirabelle action: "metis". *) -structure Mirabelle_Metis : MIRABELLE_ACTION = +structure Mirabelle_Metis: sig end = struct -fun metis_tag id = "#" ^ string_of_int id ^ " metis: " - -fun init _ = I -fun done _ _ = () - -fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) = - let - val thms = Mirabelle.theorems_of_sucessful_proof post - val names = map Thm.get_name_hint thms - val add_info = if null names then I else suffix (":\n" ^ commas names) - - val facts = map #1 (Facts.props (Proof_Context.facts_of (Proof.context_of pre))) - - fun metis ctxt = - Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt - (thms @ facts) - in - (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") - |> prefix (metis_tag id) - |> add_info - |> log - end - handle Timeout.TIMEOUT _ => log (metis_tag id ^ "timeout") - | ERROR msg => log (metis_tag id ^ "error: " ^ msg) - -fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done) +val _ = + Theory.setup (Mirabelle.command_action \<^binding>\metis\ + (fn {timeout, ...} => fn {pre, post, ...} => + let + val thms = Mirabelle.theorems_of_sucessful_proof post; + val names = map Thm.get_name_hint thms; + val facts = map #1 (Facts.props (Proof_Context.facts_of (Proof.context_of pre))); + fun metis ctxt = Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt (thms @ facts); + in + (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") + |> not (null names) ? suffix (":\n" ^ commas names) + end)); end diff --git a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML b/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML rename from src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML rename to src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML @@ -1,28 +1,23 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Author: Jasmin Blanchette and Sascha Boehme, TU Munich + +Mirabelle action: "quickcheck". *) -structure Mirabelle_Quickcheck : MIRABELLE_ACTION = +structure Mirabelle_Quickcheck: sig end = struct -fun qc_tag id = "#" ^ string_of_int id ^ " quickcheck: " - -fun init _ = I -fun done _ _ = () - -fun run args id ({pre, timeout, log, ...}: Mirabelle.run_args) = - let - val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst - val quickcheck = Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key args)) 1 - in - (case Timeout.apply timeout quickcheck pre of - NONE => log (qc_tag id ^ "no counterexample") - | SOME _ => log (qc_tag id ^ "counterexample found")) - end - handle Timeout.TIMEOUT _ => log (qc_tag id ^ "timeout") - | ERROR msg => log (qc_tag id ^ "error: " ^ msg) - -fun invoke args = - Mirabelle.register (init, Mirabelle.catch qc_tag (run args), done) +val _ = + Theory.setup (Mirabelle.command_action \<^binding>\quickcheck\ + (fn {arguments, timeout, ...} => fn {pre, ...} => + let + val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst; + val quickcheck = + Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key arguments)) 1; + in + (case Timeout.apply timeout quickcheck pre of + NONE => "no counterexample" + | SOME _ => "counterexample found") + end)); end diff --git a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML rename from src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML rename to src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML @@ -1,658 +1,660 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich + +Mirabelle action: "sledgehammer". *) structure Mirabelle_Sledgehammer : MIRABELLE_ACTION = struct (*To facilitate synching the description of Mirabelle Sledgehammer parameters (in ../lib/Tools/mirabelle) with the parameters actually used by this interface, the former extracts PARAMETER and DESCRIPTION from code below which has this pattern (provided it appears in a single line): val .*K = "PARAMETER" (*DESCRIPTION*) *) (* NOTE: Do not forget to update the Sledgehammer documentation to reflect changes here. *) val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*) val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*) val fact_filterK = "fact_filter" (*=STRING: fact filter*) val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*) val isar_proofsK = "isar_proofs" (*=SMART_BOOL: enable Isar proof generation*) val keepK = "keep" (*=PATH: path where to keep temporary files created by sledgehammer*) val lam_transK = "lam_trans" (*=STRING: lambda translation scheme*) val max_callsK = "max_calls" (*=NUM: max. no. of calls to sledgehammer*) val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*) val max_mono_itersK = "max_mono_iters" (*=NUM: max. iterations of monomorphiser*) val max_new_mono_instancesK = "max_new_mono_instances" (*=NUM: max. new monomorphic instances*) val max_relevantK = "max_relevant" (*=NUM: max. relevant clauses to use*) val minimizeK = "minimize" (*=BOOL: instruct sledgehammer to run its minimizer*) val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*) val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (ie. using metis/smt)*) val proverK = "prover" (*=STRING: name of the external prover to call*) val prover_timeoutK = "prover_timeout" (*=TIME: timeout for invoked ATP (seconds of process time)*) val sliceK = "slice" (*=BOOL: allow sledgehammer-level strategy-scheduling*) val smt_proofsK = "smt_proofs" (*=BOOL: enable SMT proof generation*) val strictK = "strict" (*=BOOL: run in strict mode*) val strideK = "stride" (*=NUM: run every nth goal*) val term_orderK = "term_order" (*=STRING: term order (in E)*) val type_encK = "type_enc" (*=STRING: type encoding scheme*) val uncurried_aliasesK = "uncurried_aliases" (*=SMART_BOOL: use fresh function names to alias curried applications*) fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " fun proof_method_tag meth id = "#" ^ string_of_int id ^ " " ^ (!meth) ^ " (sledgehammer): " val separator = "-----" (*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*) (*defaults used in this Mirabelle action*) val preplay_timeout_default = "1" val lam_trans_default = "smart" val uncurried_aliases_default = "smart" val fact_filter_default = "smart" val type_enc_default = "smart" val strict_default = "false" val stride_default = 1 val max_facts_default = "smart" val slice_default = "true" val max_calls_default = 10000000 val check_trivial_default = false (*If a key is present in args then augment a list with its pair*) (*This is used to avoid fixing default values at the Mirabelle level, and instead use the default values of the tool (Sledgehammer in this case).*) fun available_parameter args key label list = let val value = AList.lookup (op =) args key in if is_some value then (label, the value) :: list else list end datatype sh_data = ShData of { calls: int, success: int, nontriv_calls: int, nontriv_success: int, lemmas: int, max_lems: int, time_isa: int, time_prover: int, time_prover_fail: int} datatype re_data = ReData of { calls: int, success: int, nontriv_calls: int, nontriv_success: int, proofs: int, time: int, timeout: int, lemmas: int * int * int, posns: (Position.T * bool) list } fun make_sh_data (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, time_prover,time_prover_fail) = ShData{calls=calls, success=success, nontriv_calls=nontriv_calls, nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, time_isa=time_isa, time_prover=time_prover, time_prover_fail=time_prover_fail} fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time, timeout,lemmas,posns) = ReData{calls=calls, success=success, nontriv_calls=nontriv_calls, nontriv_success=nontriv_success, proofs=proofs, time=time, timeout=timeout, lemmas=lemmas, posns=posns} val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0) val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), []) fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail}) = (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, posns) datatype data = Data of { sh: sh_data, re_u: re_data (* proof method with unminimized set of lemmas *) } fun make_data (sh, re_u) = Data {sh=sh, re_u=re_u} val empty_data = make_data (empty_sh_data, empty_re_data) fun map_sh_data f (Data {sh, re_u}) = let val sh' = make_sh_data (f (tuple_of_sh_data sh)) in make_data (sh', re_u) end fun map_re_data f (Data {sh, re_u}) = let val f' = make_re_data o f o tuple_of_re_data val re_u' = f' re_u in make_data (sh, re_u') end fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); val inc_sh_calls = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) val inc_sh_success = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) val inc_sh_nontriv_calls = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) val inc_sh_nontriv_success = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) fun inc_sh_lemmas n = map_sh_data (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail)) fun inc_sh_max_lems n = map_sh_data (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail)) fun inc_sh_time_isa t = map_sh_data (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail)) fun inc_sh_time_prover t = map_sh_data (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail)) fun inc_sh_time_prover_fail t = map_sh_data (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t)) val inc_proof_method_calls = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) val inc_proof_method_success = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) val inc_proof_method_nontriv_calls = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns)) val inc_proof_method_nontriv_success = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns)) val inc_proof_method_proofs = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns)) fun inc_proof_method_time t = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) val inc_proof_method_timeout = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns)) fun inc_proof_method_lemmas n = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) fun inc_proof_method_posns pos = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) val str0 = string_of_int o the_default 0 local val str = string_of_int val str3 = Real.fmt (StringCvt.FIX (SOME 3)) fun percentage a b = string_of_int (a * 100 div b) fun time t = Real.fromInt t / 1000.0 fun avg_time t n = if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 fun log_sh_data log (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) = (log ("Total number of sledgehammer calls: " ^ str calls); log ("Number of successful sledgehammer calls: " ^ str success); log ("Number of sledgehammer lemmas: " ^ str lemmas); log ("Max number of sledgehammer lemmas: " ^ str max_lems); log ("Success rate: " ^ percentage success calls ^ "%"); log ("Total number of nontrivial sledgehammer calls: " ^ str nontriv_calls); log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success); log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa)); log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_prover)); log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail)); log ("Average time for sledgehammer calls (Isabelle): " ^ str3 (avg_time time_isa calls)); log ("Average time for successful sledgehammer calls (ATP): " ^ str3 (avg_time time_prover success)); log ("Average time for failed sledgehammer calls (ATP): " ^ str3 (avg_time time_prover_fail (calls - success))) ) fun str_of_pos (pos, triv) = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^ (if triv then "[T]" else "") fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls, re_nontriv_success, re_proofs, re_time, re_timeout, (lemmas, lems_sos, lems_max), re_posns) = (log ("Total number of " ^ tag ^ "proof method calls: " ^ str re_calls); log ("Number of successful " ^ tag ^ "proof method calls: " ^ str re_success ^ " (proof: " ^ str re_proofs ^ ")"); log ("Number of " ^ tag ^ "proof method timeouts: " ^ str re_timeout); log ("Success rate: " ^ percentage re_success sh_calls ^ "%"); log ("Total number of nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_calls); log ("Number of successful nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_success ^ " (proof: " ^ str re_proofs ^ ")"); log ("Number of successful " ^ tag ^ "proof method lemmas: " ^ str lemmas); log ("SOS of successful " ^ tag ^ "proof method lemmas: " ^ str lems_sos); log ("Max number of successful " ^ tag ^ "proof method lemmas: " ^ str lems_max); log ("Total time for successful " ^ tag ^ "proof method calls: " ^ str3 (time re_time)); log ("Average time for successful " ^ tag ^ "proof method calls: " ^ str3 (avg_time re_time re_success)); if tag="" then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns)) else () ) in fun log_data id log (Data {sh, re_u}) = let val ShData {calls=sh_calls, ...} = sh fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else () fun log_re tag m = log_re_data log tag sh_calls (tuple_of_re_data m) fun log_proof_method (tag1, m1) = app_if m1 (fn () => (log_re tag1 m1; log "")) in if sh_calls > 0 then (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n"); log_sh_data log (tuple_of_sh_data sh); log ""; log_proof_method ("", re_u)) else () end end (* Warning: we implicitly assume single-threaded execution here *) val data = Unsynchronized.ref ([] : (int * data) list) fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy) fun done id ({log, ...}: Mirabelle.done_args) = AList.lookup (op =) (!data) id |> Option.map (log_data id log) |> K () fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ()) fun get_prover_name thy args = let fun default_prover_name () = hd (#provers (Sledgehammer_Commands.default_params thy [])) handle List.Empty => error "No ATP available" in (case AList.lookup (op =) args proverK of SOME name => name | NONE => default_prover_name ()) end fun get_prover ctxt name params goal = let val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (Thm.prop_of goal) in Sledgehammer_Prover_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal learn name end type stature = ATP_Problem_Generate.stature fun is_good_line s = (String.isSubstring " ms)" s orelse String.isSubstring " s)" s) andalso not (String.isSubstring "(> " s) andalso not (String.isSubstring ", > " s) andalso not (String.isSubstring "may fail" s) (* Fragile hack *) fun proof_method_from_msg args msg = (case AList.lookup (op =) args proof_methodK of SOME name => if name = "smart" then if exists is_good_line (split_lines msg) then "none" else "fail" else name | NONE => if exists is_good_line (split_lines msg) then "none" (* trust the preplayed proof *) else if String.isSubstring "metis (" msg then msg |> Substring.full |> Substring.position "metis (" |> snd |> Substring.position ")" |> fst |> Substring.string |> suffix ")" else if String.isSubstring "metis" msg then "metis" else "smt") local datatype sh_result = SH_OK of int * int * (string * stature) list | SH_FAIL of int * int | SH_ERROR fun run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans uncurried_aliases e_selection_heuristic term_order force_sos hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st = let val thy = Proof.theory_of st val {context = ctxt, facts = chained_ths, goal} = Proof.goal st val i = 1 fun set_file_name (SOME dir) = Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix ("prob_" ^ str0 (Position.line_of pos) ^ "__") #> Config.put SMT_Config.debug_files (dir ^ "/" ^ Name.desymbolize (SOME false) (ATP_Util.timestamp ()) ^ "_" ^ serial_string ()) | set_file_name NONE = I val st' = st |> Proof.map_context (set_file_name dir #> (Option.map (Config.put Sledgehammer_ATP_Systems.e_selection_heuristic) e_selection_heuristic |> the_default I) #> (Option.map (Config.put Sledgehammer_ATP_Systems.term_order) term_order |> the_default I) #> (Option.map (Config.put Sledgehammer_ATP_Systems.force_sos) force_sos |> the_default I)) val params as {max_facts, minimize, preplay_timeout, ...} = Sledgehammer_Commands.default_params thy ([(* ("verbose", "true"), *) ("fact_filter", fact_filter), ("type_enc", type_enc), ("strict", strict), ("lam_trans", lam_trans |> the_default lam_trans_default), ("uncurried_aliases", uncurried_aliases |> the_default uncurried_aliases_default), ("max_facts", max_facts), ("slice", slice), ("timeout", string_of_int timeout), ("preplay_timeout", preplay_timeout)] |> isar_proofsLST |> smt_proofsLST |> minimizeLST (*don't confuse the two minimization flags*) |> max_new_mono_instancesLST |> max_mono_itersLST) val default_max_facts = Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt val time_limit = (case hard_timeout of NONE => I | SOME secs => Timeout.apply (Time.fromSeconds secs)) fun failed failure = ({outcome = SOME failure, used_facts = [], used_from = [], preferred_methss = (Sledgehammer_Proof_Methods.Auto_Method, []), run_time = Time.zeroTime, message = K ""}, ~1) val ({outcome, used_facts, preferred_methss, run_time, message, ...} : Sledgehammer_Prover.prover_result, time_isa) = time_limit (Mirabelle.cpu_time (fn () => let val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover_name val keywords = Thy_Header.get_keywords' ctxt val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val facts = Sledgehammer_Fact.nearly_all_facts ctxt ho_atp Sledgehammer_Fact.no_fact_override keywords css_table chained_ths hyp_ts concl_t val factss = facts |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name (the_default default_max_facts max_facts) Sledgehammer_Fact.no_fact_override hyp_ts concl_t |> tap (fn factss => "Line " ^ str0 (Position.line_of pos) ^ ": " ^ Sledgehammer.string_of_factss factss |> writeln) val prover = get_prover ctxt prover_name params goal val problem = {comment = "", state = st', goal = goal, subgoal = i, subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss, found_proof = I} in prover params problem end)) () handle Timeout.TIMEOUT _ => failed ATP_Proof.TimedOut | Fail "inappropriate" => failed ATP_Proof.Inappropriate val time_prover = run_time |> Time.toMilliseconds val msg = message (fn () => Sledgehammer.play_one_line_proof minimize preplay_timeout used_facts st' i preferred_methss) in (case outcome of NONE => (msg, SH_OK (time_isa, time_prover, used_facts)) | SOME _ => (msg, SH_FAIL (time_isa, time_prover))) end handle ERROR msg => ("error: " ^ msg, SH_ERROR) in fun run_sledgehammer trivial args proof_method named_thms id ({pre=st, log, pos, ...}: Mirabelle.run_args) = let val thy = Proof.theory_of st val triv_str = if trivial then "[T] " else "" val _ = change_data id inc_sh_calls val _ = if trivial then () else change_data id inc_sh_nontriv_calls val prover_name = get_prover_name thy args val fact_filter = AList.lookup (op =) args fact_filterK |> the_default fact_filter_default val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default val strict = AList.lookup (op =) args strictK |> the_default strict_default val max_facts = (case AList.lookup (op =) args max_factsK of SOME max => max | NONE => (case AList.lookup (op =) args max_relevantK of SOME max => max | NONE => max_facts_default)) val slice = AList.lookup (op =) args sliceK |> the_default slice_default val lam_trans = AList.lookup (op =) args lam_transK val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK val e_selection_heuristic = AList.lookup (op =) args e_selection_heuristicK val term_order = AList.lookup (op =) args term_orderK val force_sos = AList.lookup (op =) args force_sosK |> Option.map (curry (op <>) "false") val dir = AList.lookup (op =) args keepK val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) (* always use a hard timeout, but give some slack so that the automatic minimizer has a chance to do its magic *) val preplay_timeout = AList.lookup (op =) args preplay_timeoutK |> the_default preplay_timeout_default val isar_proofsLST = available_parameter args isar_proofsK "isar_proofs" val smt_proofsLST = available_parameter args smt_proofsK "smt_proofs" val minimizeLST = available_parameter args minimizeK "minimize" val max_new_mono_instancesLST = available_parameter args max_new_mono_instancesK max_new_mono_instancesK val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK val hard_timeout = SOME (4 * timeout) val (msg, result) = run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans uncurried_aliases e_selection_heuristic term_order force_sos hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st in (case result of SH_OK (time_isa, time_prover, names) => let fun get_thms (name, stature) = try (Sledgehammer_Util.thms_of_name (Proof.context_of st)) name |> Option.map (pair (name, stature)) in change_data id inc_sh_success; if trivial then () else change_data id inc_sh_nontriv_success; change_data id (inc_sh_lemmas (length names)); change_data id (inc_sh_max_lems (length names)); change_data id (inc_sh_time_isa time_isa); change_data id (inc_sh_time_prover time_prover); proof_method := proof_method_from_msg args msg; named_thms := SOME (map_filter get_thms names); log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg) end | SH_FAIL (time_isa, time_prover) => let val _ = change_data id (inc_sh_time_isa time_isa) val _ = change_data id (inc_sh_time_prover_fail time_prover) in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)) end end fun override_params prover type_enc timeout = [("provers", prover), ("max_facts", "0"), ("type_enc", type_enc), ("strict", "true"), ("slice", "false"), ("timeout", timeout |> Time.toSeconds |> string_of_int)] fun run_proof_method trivial full name meth named_thms id ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = let fun do_method named_thms ctxt = let val ref_of_str = (* FIXME proper wrapper for parser combinators *) suffix ";" #> Token.explode (Thy_Header.get_keywords' ctxt) Position.none #> Parse.thm #> fst val thms = named_thms |> maps snd val facts = named_thms |> map (ref_of_str o fst o fst) val fact_override = {add = facts, del = [], only = true} fun my_timeout time_slice = timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal fun sledge_tac time_slice prover type_enc = Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt (override_params prover type_enc (my_timeout time_slice)) fact_override [] in if !meth = "sledgehammer_tac" then sledge_tac 0.2 ATP_Proof.vampireN "mono_native" ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??" ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native" ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??" ORELSE' SMT_Solver.smt_tac ctxt thms else if !meth = "smt" then SMT_Solver.smt_tac ctxt thms else if full then Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms else if String.isPrefix "metis (" (!meth) then let val (type_encs, lam_trans) = !meth |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start |> filter Token.is_proper |> tl |> Metis_Tactic.parse_metis_options |> fst |>> the_default [ATP_Proof_Reconstruct.partial_typesN] ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end else if !meth = "metis" then Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms else if !meth = "none" then K all_tac else if !meth = "fail" then K no_tac else (warning ("Unknown method " ^ quote (!meth)); K no_tac) end fun apply_method named_thms = Mirabelle.can_apply timeout (do_method named_thms) st fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" | with_time (true, t) = (change_data id inc_proof_method_success; if trivial then () else change_data id inc_proof_method_nontriv_success; change_data id (inc_proof_method_lemmas (length named_thms)); change_data id (inc_proof_method_time t); change_data id (inc_proof_method_posns (pos, trivial)); if name = "proof" then change_data id inc_proof_method_proofs else (); "succeeded (" ^ string_of_int t ^ ")") fun timed_method named_thms = (with_time (Mirabelle.cpu_time apply_method named_thms), true) handle Timeout.TIMEOUT _ => (change_data id inc_proof_method_timeout; ("timeout", false)) | ERROR msg => ("error: " ^ msg, false) val _ = log separator val _ = change_data id inc_proof_method_calls val _ = if trivial then () else change_data id inc_proof_method_nontriv_calls in named_thms |> timed_method |>> log o prefix (proof_method_tag meth id) |> snd end val try_timeout = seconds 5.0 (* crude hack *) val num_sledgehammer_calls = Unsynchronized.ref 0 val remaining_stride = Unsynchronized.ref stride_default fun sledgehammer_action args = let val stride = Mirabelle.get_int_setting args (strideK, stride_default) val max_calls = Mirabelle.get_int_setting args (max_callsK, max_calls_default) val check_trivial = Mirabelle.get_bool_setting args (check_trivialK, check_trivial_default) in fn id => fn (st as {pre, name, log, ...}: Mirabelle.run_args) => let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then () else if !remaining_stride > 1 then (* We still have some steps to do *) (remaining_stride := !remaining_stride - 1; log "Skipping because of stride") else (* This was the last step, now run the action *) let val _ = remaining_stride := stride val _ = num_sledgehammer_calls := !num_sledgehammer_calls + 1 in if !num_sledgehammer_calls > max_calls then log "Skipping because max number of calls reached" else let val meth = Unsynchronized.ref "" val named_thms = Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) val trivial = if check_trivial then Try0.try0 (SOME try_timeout) ([], [], [], []) pre handle Timeout.TIMEOUT _ => false else false fun apply_method () = (Mirabelle.catch_result (proof_method_tag meth) false (run_proof_method trivial false name meth (these (!named_thms))) id st; ()) in Mirabelle.catch sh_tag (run_sledgehammer trivial args meth named_thms) id st; if is_some (!named_thms) then apply_method () else () end end end end fun invoke args = Mirabelle.register (init, sledgehammer_action args, done) end diff --git a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML rename from src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML rename to src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML @@ -1,178 +1,180 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Author: Jasmin Blanchette, TU Munich + +Mirabelle action: "sledgehammer_filter". *) structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION = struct fun get args name default_value = case AList.lookup (op =) args name of SOME value => Value.parse_real value | NONE => default_value fun extract_relevance_fudge args {local_const_multiplier, worse_irrel_freq, higher_order_irrel_weight, abs_rel_weight, abs_irrel_weight, theory_const_rel_weight, theory_const_irrel_weight, chained_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus, local_bonus, assum_bonus, chained_bonus, max_imperfect, max_imperfect_exp, threshold_divisor, ridiculous_threshold} = {local_const_multiplier = get args "local_const_multiplier" local_const_multiplier, worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq, higher_order_irrel_weight = get args "higher_order_irrel_weight" higher_order_irrel_weight, abs_rel_weight = get args "abs_rel_weight" abs_rel_weight, abs_irrel_weight = get args "abs_irrel_weight" abs_irrel_weight, theory_const_rel_weight = get args "theory_const_rel_weight" theory_const_rel_weight, theory_const_irrel_weight = get args "theory_const_irrel_weight" theory_const_irrel_weight, chained_const_irrel_weight = get args "chained_const_irrel_weight" chained_const_irrel_weight, intro_bonus = get args "intro_bonus" intro_bonus, elim_bonus = get args "elim_bonus" elim_bonus, simp_bonus = get args "simp_bonus" simp_bonus, local_bonus = get args "local_bonus" local_bonus, assum_bonus = get args "assum_bonus" assum_bonus, chained_bonus = get args "chained_bonus" chained_bonus, max_imperfect = get args "max_imperfect" max_imperfect, max_imperfect_exp = get args "max_imperfect_exp" max_imperfect_exp, threshold_divisor = get args "threshold_divisor" threshold_divisor, ridiculous_threshold = get args "ridiculous_threshold" ridiculous_threshold} structure Prooftab = Table(type key = int * int val ord = prod_ord int_ord int_ord) val proof_table = Unsynchronized.ref (Prooftab.empty: string list list Prooftab.table) val num_successes = Unsynchronized.ref ([] : (int * int) list) val num_failures = Unsynchronized.ref ([] : (int * int) list) val num_found_proofs = Unsynchronized.ref ([] : (int * int) list) val num_lost_proofs = Unsynchronized.ref ([] : (int * int) list) val num_found_facts = Unsynchronized.ref ([] : (int * int) list) val num_lost_facts = Unsynchronized.ref ([] : (int * int) list) fun get id c = the_default 0 (AList.lookup (op =) (!c) id) fun add id c n = c := (case AList.lookup (op =) (!c) id of SOME m => AList.update (op =) (id, m + n) (!c) | NONE => (id, n) :: !c) fun init proof_file _ thy = let fun do_line line = (case line |> space_explode ":" of [line_num, offset, proof] => SOME (apply2 (the o Int.fromString) (line_num, offset), proof |> space_explode " " |> filter_out (curry (op =) "")) | _ => NONE) val proofs = File.read (Path.explode proof_file) val proof_tab = proofs |> space_explode "\n" |> map_filter do_line |> AList.coalesce (op =) |> Prooftab.make in proof_table := proof_tab; thy end fun percentage a b = if b = 0 then "N/A" else string_of_int (a * 100 div b) fun percentage_alt a b = percentage a (a + b) fun done id ({log, ...} : Mirabelle.done_args) = if get id num_successes + get id num_failures > 0 then (log ""; log ("Number of overall successes: " ^ string_of_int (get id num_successes)); log ("Number of overall failures: " ^ string_of_int (get id num_failures)); log ("Overall success rate: " ^ percentage_alt (get id num_successes) (get id num_failures) ^ "%"); log ("Number of found proofs: " ^ string_of_int (get id num_found_proofs)); log ("Number of lost proofs: " ^ string_of_int (get id num_lost_proofs)); log ("Proof found rate: " ^ percentage_alt (get id num_found_proofs) (get id num_lost_proofs) ^ "%"); log ("Number of found facts: " ^ string_of_int (get id num_found_facts)); log ("Number of lost facts: " ^ string_of_int (get id num_lost_facts)); log ("Fact found rate: " ^ percentage_alt (get id num_found_facts) (get id num_lost_facts) ^ "%")) else () val default_prover = ATP_Proof.eN (* arbitrary ATP *) fun with_index (i, s) = s ^ "@" ^ string_of_int i fun action args id ({pre, pos, log, ...} : Mirabelle.run_args) = case (Position.line_of pos, Position.offset_of pos) of (SOME line_num, SOME offset) => (case Prooftab.lookup (!proof_table) (line_num, offset) of SOME proofs => let val thy = Proof.theory_of pre val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre val prover = AList.lookup (op =) args "prover" |> the_default default_prover val params as {max_facts, ...} = Sledgehammer_Commands.default_params thy args val default_max_facts = Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover val relevance_fudge = extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge val subgoal = 1 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover val keywords = Thy_Header.get_keywords' ctxt val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val facts = Sledgehammer_Fact.nearly_all_facts ctxt ho_atp Sledgehammer_Fact.no_fact_override keywords css_table chained_ths hyp_ts concl_t |> Sledgehammer_Fact.drop_duplicate_facts |> Sledgehammer_MePo.mepo_suggested_facts ctxt params (the_default default_max_facts max_facts) (SOME relevance_fudge) hyp_ts concl_t |> map (fst o fst) val (found_facts, lost_facts) = flat proofs |> sort_distinct string_ord |> map (fn fact => (find_index (curry (op =) fact) facts, fact)) |> List.partition (curry (op <=) 0 o fst) |>> sort (prod_ord int_ord string_ord) ||> map snd val found_proofs = filter (forall (member (op =) facts)) proofs val n = length found_proofs val _ = if n = 0 then (add id num_failures 1; log "Failure") else (add id num_successes 1; add id num_found_proofs n; log ("Success (" ^ string_of_int n ^ " of " ^ string_of_int (length proofs) ^ " proofs)")) val _ = add id num_lost_proofs (length proofs - n) val _ = add id num_found_facts (length found_facts) val _ = add id num_lost_facts (length lost_facts) val _ = if null found_facts then () else let val found_weight = Real.fromInt (fold (fn (n, _) => Integer.add (n * n)) found_facts 0) / Real.fromInt (length found_facts) |> Math.sqrt |> Real.ceil in log ("Found facts (among " ^ string_of_int (length facts) ^ ", weight " ^ string_of_int found_weight ^ "): " ^ commas (map with_index found_facts)) end val _ = if null lost_facts then () else log ("Lost facts (among " ^ string_of_int (length facts) ^ "): " ^ commas lost_facts) in () end | NONE => log "No known proof") | _ => () val proof_fileK = "proof_file" fun invoke args = let val (pf_args, other_args) = args |> List.partition (curry (op =) proof_fileK o fst) val proof_file = (case pf_args of [] => error "No \"proof_file\" specified" | (_, s) :: _ => s) in Mirabelle.register (init proof_file, action other_args, done) end end; (* Workaround to keep the "mirabelle.pl" script happy *) structure Mirabelle_Sledgehammer_filter = Mirabelle_Sledgehammer_Filter; diff --git a/src/HOL/Mirabelle/Tools/mirabelle_try0.ML b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML rename from src/HOL/Mirabelle/Tools/mirabelle_try0.ML rename to src/HOL/Tools/Mirabelle/mirabelle_try0.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_try0.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML @@ -1,23 +1,17 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_try0.ML Author: Jasmin Blanchette, TU Munich + Author: Makarius + +Mirabelle action: "try0". *) -structure Mirabelle_Try0 : MIRABELLE_ACTION = +structure Mirabelle_Try0 : sig end = struct -fun try0_tag id = "#" ^ string_of_int id ^ " try0: " - -fun init _ = I -fun done _ _ = () - -fun times_ten time = Time.fromMilliseconds (10 * Time.toMilliseconds time) - -fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) = - if Timeout.apply (times_ten timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre - then log (try0_tag id ^ "succeeded") - else () - handle Timeout.TIMEOUT _ => log (try0_tag id ^ "timeout") - -fun invoke _ = Mirabelle.register (init, Mirabelle.catch try0_tag run, done) +val _ = + Theory.setup (Mirabelle.command_action \<^binding>\try0\ + (fn {timeout, ...} => fn {pre, ...} => + if Timeout.apply (Time.scale 10.0 timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre + then "succeeded" else "")); end diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML @@ -1,412 +1,414 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_commands.ML Author: Jasmin Blanchette, TU Muenchen Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax. *) signature SLEDGEHAMMER_COMMANDS = sig type params = Sledgehammer_Prover.params val provers : string Unsynchronized.ref val default_params : theory -> (string * string) list -> params + val parse_params: (string * string) list parser end; structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS = struct open ATP_Util open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_ATP_Systems open Sledgehammer_Prover open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh open Sledgehammer val cvc4N = "cvc4" val veritN = "verit" val z3N = "z3" val runN = "run" val supported_proversN = "supported_provers" val refresh_tptpN = "refresh_tptp" (** Sledgehammer commands **) fun add_fact_override ns : fact_override = {add = ns, del = [], only = false} fun del_fact_override ns : fact_override = {add = [], del = ns, only = false} fun only_fact_override ns : fact_override = {add = ns, del = [], only = true} fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) = {add = #add r1 @ #add r2, del = #del r1 @ #del r2, only = #only r1 andalso #only r2} fun merge_fact_overrides rs = fold merge_fact_override_pairwise rs (only_fact_override []) (*** parameters ***) val provers = Unsynchronized.ref "" type raw_param = string * string list val default_default_params = [("debug", "false"), ("verbose", "false"), ("overlord", "false"), ("spy", "false"), ("type_enc", "smart"), ("strict", "false"), ("lam_trans", "smart"), ("uncurried_aliases", "smart"), ("learn", "true"), ("fact_filter", "smart"), ("max_facts", "smart"), ("fact_thresholds", "0.45 0.85"), ("max_mono_iters", "smart"), ("max_new_mono_instances", "smart"), ("isar_proofs", "smart"), ("compress", "smart"), ("try0", "true"), ("smt_proofs", "true"), ("slice", "true"), ("minimize", "true"), ("preplay_timeout", "1")] val alias_params = [("prover", ("provers", [])), (* undocumented *) ("dont_preplay", ("preplay_timeout", ["0"])), ("dont_compress", ("compress", ["1"])), ("isar_proof", ("isar_proofs", [])) (* legacy *)] val negated_alias_params = [("no_debug", "debug"), ("quiet", "verbose"), ("no_overlord", "overlord"), ("dont_spy", "spy"), ("non_strict", "strict"), ("no_uncurried_aliases", "uncurried_aliases"), ("dont_learn", "learn"), ("no_isar_proofs", "isar_proofs"), ("dont_slice", "slice"), ("dont_minimize", "minimize"), ("dont_try0", "try0"), ("no_smt_proofs", "smt_proofs")] val property_dependent_params = ["provers", "timeout"] fun is_known_raw_param s = AList.defined (op =) default_default_params s orelse AList.defined (op =) alias_params s orelse AList.defined (op =) negated_alias_params s orelse member (op =) property_dependent_params s orelse s = "expect" fun is_prover_list ctxt s = (case space_explode " " s of ss as _ :: _ => forall (is_prover_supported ctxt) ss | _ => false) fun unalias_raw_param (name, value) = (case AList.lookup (op =) alias_params name of SOME (name', []) => (name', value) | SOME (param' as (name', _)) => if value <> ["false"] then param' else error ("Parameter " ^ quote name ^ " cannot be set to \"false\" (cf. " ^ quote name' ^ ")") | NONE => (case AList.lookup (op =) negated_alias_params name of SOME name' => (name', (case value of ["false"] => ["true"] | ["true"] => ["false"] | [] => ["false"] | _ => value)) | NONE => (name, value))) val any_type_enc = type_enc_of_string Strict "erased" (* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts =" can be omitted. For the last four, this is a secret feature. *) fun normalize_raw_param ctxt = unalias_raw_param #> (fn (name, value) => if is_known_raw_param name then (name, value) else if null value then if is_prover_list ctxt name then ("provers", [name]) else if can (type_enc_of_string Strict) name then ("type_enc", [name]) else if can (trans_lams_of_string ctxt any_type_enc) name then ("lam_trans", [name]) else if member (op =) fact_filters name then ("fact_filter", [name]) else if is_some (Int.fromString name) then ("max_facts", [name]) else error ("Unknown parameter: " ^ quote name) else error ("Unknown parameter: " ^ quote name)) (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are read correctly. *) val implode_param = strip_spaces_except_between_idents o space_implode " " (* FIXME: use "Generic_Data" *) structure Data = Theory_Data ( type T = raw_param list val empty = default_default_params |> map (apsnd single) val extend = I fun merge data : T = AList.merge (op =) (K true) data ) fun remotify_prover_if_supported_and_not_already_remote ctxt name = if String.isPrefix remote_prefix name then SOME name else let val remote_name = remote_prefix ^ name in if is_prover_supported ctxt remote_name then SOME remote_name else NONE end fun remotify_prover_if_not_installed ctxt name = if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name else remotify_prover_if_supported_and_not_already_remote ctxt name (* The first ATP of the list is used by Auto Sledgehammer. *) fun default_provers_param_value mode ctxt = [cvc4N] @ (if is_vampire_noncommercial_license_accepted () = SOME false then [] else [vampireN]) @ [z3N, eN, spassN, veritN] |> map_filter (remotify_prover_if_not_installed ctxt) (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *) |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0)) |> implode_param fun set_default_raw_param param thy = let val ctxt = Proof_Context.init_global thy in thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param)) end fun default_raw_params mode thy = let val ctxt = Proof_Context.init_global thy in Data.get thy |> fold (AList.default (op =)) [("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]), ("timeout", let val timeout = Options.default_int \<^system_option>\sledgehammer_timeout\ in [if timeout <= 0 then "none" else string_of_int timeout] end)] end fun extract_params mode default_params override_params = let val raw_params = rev override_params @ rev default_params val lookup = Option.map implode_param o AList.lookup (op =) raw_params val lookup_string = the_default "" o lookup fun general_lookup_bool option default_value name = (case lookup name of SOME s => parse_bool_option option name s | NONE => default_value) val lookup_bool = the o general_lookup_bool false (SOME false) fun lookup_time name = (case lookup name of SOME s => parse_time name s | NONE => Time.zeroTime) fun lookup_int name = (case lookup name of NONE => 0 | SOME s => (case Int.fromString s of SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value"))) fun lookup_real name = (case lookup name of NONE => 0.0 | SOME s => (case Real.fromString s of SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value"))) fun lookup_real_pair name = (case lookup name of NONE => (0.0, 0.0) | SOME s => (case s |> space_explode " " |> map Real.fromString of [SOME r1, SOME r2] => (r1, r2) | _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \ \values (e.g., \"0.6 0.95\")"))) fun lookup_option lookup' name = (case lookup name of SOME "smart" => NONE | _ => SOME (lookup' name)) val debug = mode <> Auto_Try andalso lookup_bool "debug" val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") val overlord = lookup_bool "overlord" val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd val type_enc = if mode = Auto_Try then NONE else (case lookup_string "type_enc" of "smart" => NONE | s => (type_enc_of_string Strict s; SOME s)) val strict = mode = Auto_Try orelse lookup_bool "strict" val lam_trans = lookup_option lookup_string "lam_trans" val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" val learn = lookup_bool "learn" val fact_filter = lookup_option lookup_string "fact_filter" |> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf) val max_facts = lookup_option lookup_int "max_facts" val fact_thresholds = lookup_real_pair "fact_thresholds" val max_mono_iters = lookup_option lookup_int "max_mono_iters" val max_new_mono_instances = lookup_option lookup_int "max_new_mono_instances" val isar_proofs = lookup_option lookup_bool "isar_proofs" val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress") val try0 = lookup_bool "try0" val smt_proofs = lookup_bool "smt_proofs" val slice = mode <> Auto_Try andalso lookup_bool "slice" val minimize = lookup_bool "minimize" val timeout = lookup_time "timeout" val preplay_timeout = lookup_time "preplay_timeout" val expect = lookup_string "expect" in {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end fun get_params mode = extract_params mode o default_raw_params mode fun default_params thy = get_params Normal thy o map (apsnd single) val silence_state = Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false) (* Sledgehammer the given subgoal *) val default_learn_prover_timeout = 2.0 fun hammer_away override_params writeln_result subcommand opt_i fact_override state0 = let (* We generally want chained facts to be picked up by the relevance filter, because it can then give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs, verbose output, machine learning). However, if the fact is available by no other means (not even backticks), as "f" would be in "using f unfolding f'" after unfolding, we have no choice but to insert it into the state as an additional hypothesis. *) val {facts = chained0, ...} = Proof.goal state0 val (inserts, keep_chained) = if null chained0 orelse #only fact_override then (chained0, []) else let val ctxt0 = Proof.context_of state0 in List.partition (is_useful_unnamed_local_fact ctxt0) chained0 end val state = state0 |> (if null inserts then I else Proof.refine_insert inserts #> Proof.set_facts keep_chained) |> silence_state val thy = Proof.theory_of state val ctxt = Proof.context_of state val override_params = override_params |> map (normalize_raw_param ctxt) in if subcommand = runN then let val i = the_default 1 opt_i in ignore (run_sledgehammer (get_params Normal thy override_params) Normal writeln_result i fact_override state) end else if subcommand = supported_proversN then supported_provers ctxt else if subcommand = unlearnN then mash_unlearn ctxt else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse subcommand = relearn_isarN orelse subcommand = relearn_proverN then (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt else (); mash_learn ctxt (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *) (get_params Normal thy ([("timeout", [string_of_real default_learn_prover_timeout]), ("slice", ["false"])] @ override_params @ [("preplay_timeout", ["0"])])) fact_override (#facts (Proof.goal state)) (subcommand = learn_proverN orelse subcommand = relearn_proverN)) else if subcommand = refresh_tptpN then refresh_systems_on_tptp () else error ("Unknown subcommand: " ^ quote subcommand) end fun string_of_raw_param (key, values) = key ^ (case implode_param values of "" => "" | value => " = " ^ value) val parse_query_bang = \<^keyword>\?\ || \<^keyword>\!\ || \<^keyword>\!!\ val parse_key = Scan.repeat1 (Parse.embedded || parse_query_bang) >> implode_param val parse_value = Scan.repeat1 (Parse.name || Parse.float_number || parse_query_bang) val parse_param = parse_key -- Scan.optional (\<^keyword>\=\ |-- parse_value) [] -val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] +val parse_raw_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] +val parse_params = parse_raw_params >> map (apsnd implode_param) val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm) val parse_fact_override_chunk = (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override) || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override) || (parse_fact_refs >> only_fact_override) val parse_fact_override = Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides)) no_fact_override val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer\ "search for first-order proof using automatic theorem provers" - (Scan.optional Parse.name runN -- parse_params + (Scan.optional Parse.name runN -- parse_raw_params -- parse_fact_override -- Scan.option Parse.nat >> (fn (((subcommand, params), fact_override), opt_i) => Toplevel.keep_proof (hammer_away params NONE subcommand opt_i fact_override o Toplevel.proof_of))) val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer_params\ "set and display the default parameters for Sledgehammer" - (parse_params >> (fn params => + (parse_raw_params >> (fn params => Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => writeln ("Default parameters for Sledgehammer:\n" ^ (case rev (default_raw_params Normal thy) of [] => "none" | params => params |> map string_of_raw_param |> sort_strings |> cat_lines)))))) fun try_sledgehammer auto state = let val thy = Proof.theory_of state val mode = if auto then Auto_Try else Try val i = 1 in run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state) end val _ = Try.tool_setup (sledgehammerN, (40, \<^system_option>\auto_sledgehammer\, try_sledgehammer)) val _ = Query_Operation.register {name = sledgehammerN, pri = 0} (fn {state = st, args, writeln_result, ...} => (case try Toplevel.proof_of st of SOME state => let val [provers_arg, isar_proofs_arg, try0_arg] = args val override_params = ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @ [("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]), ("try0", [try0_arg]), ("debug", ["false"]), ("verbose", ["false"]), ("overlord", ["false"])]); in hammer_away override_params (SOME writeln_result) runN NONE no_fact_override state end | NONE => error "Unknown proof context")) end; diff --git a/src/HOL/Tools/etc/options b/src/HOL/Tools/etc/options --- a/src/HOL/Tools/etc/options +++ b/src/HOL/Tools/etc/options @@ -1,48 +1,60 @@ (* :mode=isabelle-options: *) section "Automatically tried tools" public option auto_time_start : real = 1.0 -- "initial delay for automatically tried tools (seconds)" public option auto_time_limit : real = 2.0 -- "time limit for automatically tried tools (seconds > 0)" public option auto_nitpick : bool = false -- "run Nitpick automatically" public option auto_sledgehammer : bool = false -- "run Sledgehammer automatically" public option auto_methods : bool = false -- "try standard proof methods automatically" public option auto_quickcheck : bool = true -- "run Quickcheck automatically" public option auto_solve_direct : bool = true -- "run solve_direct automatically" section "Miscellaneous Tools" public option sledgehammer_provers : string = "cvc4 z3 spass e remote_vampire" -- "provers for Sledgehammer (separated by blanks)" public option sledgehammer_timeout : int = 30 -- "provers will be interrupted after this time (in seconds)" public option vampire_noncommercial : string = "unknown" -- "status of Vampire activation for noncommercial use (yes, no, unknown)" public option SystemOnTPTP : string = "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply" -- "URL for SystemOnTPTP service" public option MaSh : string = "sml" -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)" public option kodkod_scala : bool = true -- "invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process)" public option kodkod_max_threads : int = 0 -- "default max_threads for Nitpick/Kodkod (0: maximum of Java/Scala platform)" + + +section "Mirabelle" + +option mirabelle_timeout : real = 30 + -- "default timeout for Mirabelle actions" + +option mirabelle_actions : string = "" + -- "Mirabelle actions (outer syntax, separated by semicolons)" + +option mirabelle_theories : string = "" + -- "Mirabelle theories (names with optional line range, separated by commas)" diff --git a/src/Pure/General/path.scala b/src/Pure/General/path.scala --- a/src/Pure/General/path.scala +++ b/src/Pure/General/path.scala @@ -1,312 +1,313 @@ /* Title: Pure/General/path.scala Author: Makarius Algebra of file-system paths: basic POSIX notation, extended by named roots (e.g. //foo) and variables (e.g. $BAR). */ package isabelle import java.io.{File => JFile} import scala.util.matching.Regex object Path { /* path elements */ sealed abstract class Elem private case class Root(name: String) extends Elem private case class Basic(name: String) extends Elem private case class Variable(name: String) extends Elem private case object Parent extends Elem private def err_elem(msg: String, s: String): Nothing = error(msg + " path element " + quote(s)) private val illegal_elem = Set("", "~", "~~", ".", "..") private val illegal_char = "/\\$:\"'<>|?*" private def check_elem(s: String): String = if (illegal_elem.contains(s)) err_elem("Illegal", s) else { for (c <- s) { if (c.toInt < 32) err_elem("Illegal control character " + c.toInt + " in", s) if (illegal_char.contains(c)) err_elem("Illegal character " + quote(c.toString) + " in", s) } s } private def root_elem(s: String): Elem = Root(check_elem(s)) private def basic_elem(s: String): Elem = Basic(check_elem(s)) private def variable_elem(s: String): Elem = Variable(check_elem(s)) private def apply_elem(y: Elem, xs: List[Elem]): List[Elem] = (y, xs) match { case (Root(_), _) => List(y) case (Parent, Root(_) :: _) => xs case (Parent, Basic(_) :: rest) => rest case _ => y :: xs } private def norm_elems(elems: List[Elem]): List[Elem] = elems.foldRight(List.empty[Elem])(apply_elem) private def implode_elem(elem: Elem, short: Boolean): String = elem match { case Root("") => "" case Root(s) => "//" + s case Basic(s) => s case Variable("USER_HOME") if short => "~" case Variable("ISABELLE_HOME") if short => "~~" case Variable(s) => "$" + s case Parent => ".." } private def squash_elem(elem: Elem): String = elem match { case Root("") => "ROOT" case Root(s) => "SERVER_" + s case Basic(s) => s case Variable(s) => s case Parent => "PARENT" } /* path constructors */ val current: Path = new Path(Nil) val root: Path = new Path(List(Root(""))) def named_root(s: String): Path = new Path(List(root_elem(s))) def make(elems: List[String]): Path = new Path(elems.reverse.map(basic_elem)) def basic(s: String): Path = new Path(List(basic_elem(s))) def variable(s: String): Path = new Path(List(variable_elem(s))) val parent: Path = new Path(List(Parent)) val USER_HOME: Path = variable("USER_HOME") val ISABELLE_HOME: Path = variable("ISABELLE_HOME") /* explode */ def explode(str: String): Path = { def explode_elem(s: String): Elem = try { if (s == "..") Parent else if (s == "~") Variable("USER_HOME") else if (s == "~~") Variable("ISABELLE_HOME") else if (s.startsWith("$")) variable_elem(s.substring(1)) else basic_elem(s) } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in " + quote(str)) } val ss = space_explode('/', str) val r = ss.takeWhile(_.isEmpty).length val es = ss.dropWhile(_.isEmpty) val (roots, raw_elems) = if (r == 0) (Nil, es) else if (r == 1) (List(Root("")), es) else if (es.isEmpty) (List(Root("")), Nil) else (List(root_elem(es.head)), es.tail) val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem) new Path(norm_elems(elems reverse_::: roots)) } def is_wellformed(str: String): Boolean = try { explode(str); true } catch { case ERROR(_) => false } def is_valid(str: String): Boolean = try { explode(str).expand; true } catch { case ERROR(_) => false } def split(str: String): List[Path] = space_explode(':', str).filterNot(_.isEmpty).map(explode) /* encode */ val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode)) /* reserved names */ private val reserved_windows: Set[String] = Set("CON", "PRN", "AUX", "NUL", "COM1", "COM2", "COM3", "COM4", "COM5", "COM6", "COM7", "COM8", "COM9", "LPT1", "LPT2", "LPT3", "LPT4", "LPT5", "LPT6", "LPT7", "LPT8", "LPT9") def is_reserved(name: String): Boolean = Long_Name.explode(name).exists(a => reserved_windows.contains(Word.uppercase(a))) /* case-insensitive names */ def check_case_insensitive(paths: List[Path]): Unit = { val table = paths.foldLeft(Multi_Map.empty[String, String]) { case (tab, path) => val name = path.expand.implode tab.insert(Word.lowercase(name), name) } val collisions = (for { (_, coll) <- table.iterator_list if coll.length > 1 } yield coll).toList.flatten if (collisions.nonEmpty) { error(("Collision of file names due case-insensitivity:" :: collisions).mkString("\n ")) } } } final class Path private(protected val elems: List[Path.Elem]) // reversed elements { override def hashCode: Int = elems.hashCode override def equals(that: Any): Boolean = that match { case other: Path => elems == other.elems case _ => false } def is_current: Boolean = elems.isEmpty def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root] def is_root: Boolean = elems match { case List(Path.Root(_)) => true case _ => false } def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false } def starts_basic: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Basic] def +(other: Path): Path = new Path(other.elems.foldRight(elems)(Path.apply_elem)) /* implode */ private def gen_implode(short: Boolean): String = elems match { case Nil => "." case List(Path.Root("")) => "/" case _ => elems.map(Path.implode_elem(_, short)).reverse.mkString("/") } def implode: String = gen_implode(false) def implode_short: String = gen_implode(true) override def toString: String = quote(implode) /* base element */ private def split_path: (Path, String) = elems match { case Path.Basic(s) :: xs => (new Path(xs), s) case _ => error("Cannot split path into dir/base: " + toString) } def dir: Path = split_path._1 def base: Path = new Path(List(Path.Basic(split_path._2))) def ext(e: String): Path = if (e == "") this else { val (prfx, s) = split_path prfx + Path.basic(s + "." + e) } def xz: Path = ext("xz") def xml: Path = ext("xml") def html: Path = ext("html") def tex: Path = ext("tex") def pdf: Path = ext("pdf") def thy: Path = ext("thy") def tar: Path = ext("tar") def gz: Path = ext("gz") + def log: Path = ext("log") def backup: Path = { val (prfx, s) = split_path prfx + Path.basic(s + "~") } def backup2: Path = { val (prfx, s) = split_path prfx + Path.basic(s + "~~") } def platform_exe: Path = if (Platform.is_windows) ext("exe") else this private val Ext = new Regex("(.*)\\.([^.]*)") def split_ext: (Path, String) = { val (prefix, base) = split_path base match { case Ext(b, e) => (prefix + Path.basic(b), e) case _ => (prefix + Path.basic(base), "") } } def drop_ext: Path = split_ext._1 def get_ext: String = split_ext._2 def squash: Path = new Path(elems.map(elem => Path.Basic(Path.squash_elem(elem)))) /* expand */ def expand_env(env: Map[String, String]): Path = { def eval(elem: Path.Elem): List[Path.Elem] = elem match { case Path.Variable(s) => val path = Path.explode(Isabelle_System.getenv_strict(s, env)) if (path.elems.exists(_.isInstanceOf[Path.Variable])) error("Illegal path variable nesting: " + s + "=" + path.toString) else path.elems case x => List(x) } new Path(Path.norm_elems(elems.flatMap(eval))) } def expand: Path = expand_env(Isabelle_System.settings()) def file_name: String = expand.base.implode /* implode wrt. given directories */ def implode_symbolic: String = { val directories = Library.space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse val full_name = expand.implode directories.view.flatMap(a => try { val b = Path.explode(a).expand.implode if (full_name == b) Some(a) else { Library.try_unprefix(b + "/", full_name) match { case Some(name) => Some(a + "/" + name) case None => None } } } catch { case ERROR(_) => None }).headOption.getOrElse(implode) } def position: Position.T = Position.File(implode_symbolic) /* platform files */ def file: JFile = File.platform_file(this) def is_file: Boolean = file.isFile def is_dir: Boolean = file.isDirectory def absolute_file: JFile = File.absolute(file) def canonical_file: JFile = File.canonical(file) def absolute: Path = File.path(absolute_file) def canonical: Path = File.path(canonical_file) } diff --git a/src/Pure/Isar/token.ML b/src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML +++ b/src/Pure/Isar/token.ML @@ -1,798 +1,802 @@ (* Title: Pure/Isar/token.ML Author: Markus Wenzel, TU Muenchen Outer token syntax for Isabelle/Isar. *) signature TOKEN = sig datatype kind = (*immediate source*) Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat | Float | Space | (*delimited content*) String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option | (*special content*) Error of string | EOF val str_of_kind: kind -> string type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T} type T type src = T list type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring} datatype value = Source of src | Literal of bool * Markup.T | Name of name_value * morphism | Typ of typ | Term of term | Fact of string option * thm list | Attribute of morphism -> attribute | Declaration of declaration | Files of file Exn.result list val pos_of: T -> Position.T val adjust_offsets: (int -> int option) -> T -> T val eof: T val is_eof: T -> bool val not_eof: T -> bool val stopper: T Scan.stopper val kind_of: T -> kind val is_kind: kind -> T -> bool val is_command: T -> bool val keyword_with: (string -> bool) -> T -> bool val is_command_modifier: T -> bool val ident_with: (string -> bool) -> T -> bool val is_proper: T -> bool val is_comment: T -> bool val is_informal_comment: T -> bool val is_formal_comment: T -> bool val is_document_marker: T -> bool val is_ignored: T -> bool val is_begin_ignore: T -> bool val is_end_ignore: T -> bool val is_error: T -> bool val is_space: T -> bool val is_blank: T -> bool val is_newline: T -> bool val range_of: T list -> Position.range val core_range_of: T list -> Position.range val content_of: T -> string val source_of: T -> string val input_of: T -> Input.source val inner_syntax_of: T -> string val keyword_markup: bool * Markup.T -> string -> Markup.T val completion_report: T -> Position.report_text list val reports: Keyword.keywords -> T -> Position.report_text list val markups: Keyword.keywords -> T -> Markup.T list val unparse: T -> string val print: T -> string val text_of: T -> string * string val file_source: file -> Input.source val get_files: T -> file Exn.result list val put_files: file Exn.result list -> T -> T val get_value: T -> value option val reports_of_value: T -> Position.report list val name_value: name_value -> value val get_name: T -> name_value option val declare_maxidx: T -> Proof.context -> Proof.context val map_facts: (string option -> thm list -> thm list) -> T -> T val trim_context_src: src -> src val transform: morphism -> T -> T val init_assignable: T -> T val assign: value option -> T -> T val evaluate: ('a -> value) -> (T -> 'a) -> T -> 'a val closure: T -> T val pretty_value: Proof.context -> T -> Pretty.T val name_of_src: src -> string * Position.T val args_of_src: src -> T list val checked_src: src -> bool val check_src: Proof.context -> (Proof.context -> 'a Name_Space.table) -> src -> src * 'a val pretty_src: Proof.context -> src -> Pretty.T val ident_or_symbolic: string -> bool val read_cartouche: Symbol_Pos.T list -> T val tokenize: Keyword.keywords -> {strict: bool} -> Symbol_Pos.T list -> T list val explode: Keyword.keywords -> Position.T -> string -> T list val explode0: Keyword.keywords -> string -> T list val print_name: Keyword.keywords -> string -> string + val print_properties: Keyword.keywords -> Properties.T -> string val make: (int * int) * string -> Position.T -> T * Position.T val make_string: string * Position.T -> T val make_int: int -> T list val make_src: string * Position.T -> T list -> src type 'a parser = T list -> 'a * T list type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list) val read_body: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a option val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context end; structure Token: TOKEN = struct (** tokens **) (* token kind *) datatype kind = (*immediate source*) Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat | Float | Space | (*delimited content*) String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option | (*special content*) Error of string | EOF; val str_of_kind = fn Command => "command" | Keyword => "keyword" | Ident => "identifier" | Long_Ident => "long identifier" | Sym_Ident => "symbolic identifier" | Var => "schematic variable" | Type_Ident => "type variable" | Type_Var => "schematic type variable" | Nat => "natural number" | Float => "floating-point number" | Space => "white space" | String => "quoted string" | Alt_String => "back-quoted string" | Verbatim => "verbatim text" | Cartouche => "text cartouche" | Comment NONE => "informal comment" | Comment (SOME _) => "formal comment" | Error _ => "bad input" | EOF => "end-of-input"; val immediate_kinds = Vector.fromList [Command, Keyword, Ident, Long_Ident, Sym_Ident, Var, Type_Ident, Type_Var, Nat, Float, Space]; val delimited_kind = (fn String => true | Alt_String => true | Verbatim => true | Cartouche => true | Comment _ => true | _ => false); (* datatype token *) (*The value slot assigns an (optional) internal value to a token, usually as a side-effect of special scanner setup (see also args.ML). Note that an assignable ref designates an intermediate state of internalization -- it is NOT meant to persist.*) type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}; type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring}; datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot and slot = Slot | Value of value option | Assignable of value option Unsynchronized.ref and value = Source of T list | Literal of bool * Markup.T | Name of name_value * morphism | Typ of typ | Term of term | Fact of string option * thm list | (*optional name for dynamic fact, i.e. fact "variable"*) Attribute of morphism -> attribute | Declaration of declaration | Files of file Exn.result list; type src = T list; (* position *) fun pos_of (Token ((_, (pos, _)), _, _)) = pos; fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos; fun adjust_offsets adjust (Token ((x, range), y, z)) = Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z); (* stopper *) fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot); val eof = mk_eof Position.none; fun is_eof (Token (_, (EOF, _), _)) = true | is_eof _ = false; val not_eof = not o is_eof; val stopper = Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof; (* kind of token *) fun kind_of (Token (_, (k, _), _)) = k; fun is_kind k (Token (_, (k', _), _)) = k = k'; val is_command = is_kind Command; fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x | keyword_with _ _ = false; val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "qualified"); fun ident_with pred (Token (_, (Ident, x), _)) = pred x | ident_with _ _ = false; fun is_ignored (Token (_, (Space, _), _)) = true | is_ignored (Token (_, (Comment NONE, _), _)) = true | is_ignored _ = false; fun is_proper (Token (_, (Space, _), _)) = false | is_proper (Token (_, (Comment _, _), _)) = false | is_proper _ = true; fun is_comment (Token (_, (Comment _, _), _)) = true | is_comment _ = false; fun is_informal_comment (Token (_, (Comment NONE, _), _)) = true | is_informal_comment _ = false; fun is_formal_comment (Token (_, (Comment (SOME _), _), _)) = true | is_formal_comment _ = false; fun is_document_marker (Token (_, (Comment (SOME Comment.Marker), _), _)) = true | is_document_marker _ = false; fun is_begin_ignore (Token (_, (Comment NONE, "<"), _)) = true | is_begin_ignore _ = false; fun is_end_ignore (Token (_, (Comment NONE, ">"), _)) = true | is_end_ignore _ = false; fun is_error (Token (_, (Error _, _), _)) = true | is_error _ = false; (* blanks and newlines -- space tokens obey lines *) fun is_space (Token (_, (Space, _), _)) = true | is_space _ = false; fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x) | is_blank _ = false; fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x | is_newline _ = false; (* range of tokens *) fun range_of (toks as tok :: _) = let val pos' = end_pos_of (List.last toks) in Position.range (pos_of tok, pos') end | range_of [] = Position.no_range; val core_range_of = drop_prefix is_ignored #> drop_suffix is_ignored #> range_of; (* token content *) fun content_of (Token (_, (_, x), _)) = x; fun source_of (Token ((source, _), _, _)) = source; fun input_of (Token ((source, range), (kind, _), _)) = Input.source (delimited_kind kind) source range; fun inner_syntax_of tok = let val x = content_of tok in if YXML.detect x then x else Syntax.implode_input (input_of tok) end; (* markup reports *) local val token_kind_markup = fn Var => (Markup.var, "") | Type_Ident => (Markup.tfree, "") | Type_Var => (Markup.tvar, "") | String => (Markup.string, "") | Alt_String => (Markup.alt_string, "") | Verbatim => (Markup.verbatim, "") | Cartouche => (Markup.cartouche, "") | Comment _ => (Markup.comment, "") | Error msg => (Markup.bad (), msg) | _ => (Markup.empty, ""); fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), "")); fun command_markups keywords x = if Keyword.is_theory_end keywords x then [Markup.keyword2 |> Markup.keyword_properties] else (if Keyword.is_proof_asm keywords x then [Markup.keyword3] else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper] else [Markup.keyword1]) |> map Markup.command_properties; in fun keyword_markup (important, keyword) x = if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter; fun completion_report tok = if is_kind Keyword tok then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok)) else []; fun reports keywords tok = if is_command tok then keyword_reports tok (command_markups keywords (content_of tok)) else if is_kind Keyword tok then keyword_reports tok [keyword_markup (false, Markup.keyword2 |> Markup.keyword_properties) (content_of tok)] else let val pos = pos_of tok; val (m, text) = token_kind_markup (kind_of tok); val delete = #2 (Symbol_Pos.explode_delete (source_of tok, pos)); in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) delete end; fun markups keywords = map (#2 o #1) o reports keywords; end; (* unparse *) fun unparse (Token (_, (kind, x), _)) = (case kind of String => Symbol_Pos.quote_string_qq x | Alt_String => Symbol_Pos.quote_string_bq x | Verbatim => enclose "{*" "*}" x | Cartouche => cartouche x | Comment NONE => enclose "(*" "*)" x | EOF => "" | _ => x); fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok); fun text_of tok = let val k = str_of_kind (kind_of tok); val ms = markups Keyword.empty_keywords tok; val s = unparse tok; in if s = "" then (k, "") else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ Markup.markups ms s, "") else (k, Markup.markups ms s) end; (** associated values **) (* inlined file content *) fun file_source (file: file) = let val text = cat_lines (#lines file); val end_pos = fold Position.advance (Symbol.explode text) (#pos file); in Input.source true text (Position.range (#pos file, end_pos)) end; fun get_files (Token (_, _, Value (SOME (Files files)))) = files | get_files _ = []; fun put_files [] tok = tok | put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files))) | put_files _ tok = raise Fail ("Cannot put inlined files here" ^ Position.here (pos_of tok)); (* access values *) fun get_value (Token (_, _, Value v)) = v | get_value _ = NONE; fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v))) | map_value _ tok = tok; (* reports of value *) fun get_assignable_value (Token (_, _, Assignable r)) = ! r | get_assignable_value (Token (_, _, Value v)) = v | get_assignable_value _ = NONE; fun reports_of_value tok = (case get_assignable_value tok of SOME (Literal markup) => let val pos = pos_of tok; val x = content_of tok; in if Position.is_reported pos then map (pair pos) (keyword_markup markup x :: Completion.suppress_abbrevs x) else [] end | _ => []); (* name value *) fun name_value a = Name (a, Morphism.identity); fun get_name tok = (case get_assignable_value tok of SOME (Name (a, _)) => SOME a | _ => NONE); (* maxidx *) fun declare_maxidx tok = (case get_value tok of SOME (Source src) => fold declare_maxidx src | SOME (Typ T) => Variable.declare_maxidx (Term.maxidx_of_typ T) | SOME (Term t) => Variable.declare_maxidx (Term.maxidx_of_term t) | SOME (Fact (_, ths)) => fold (Variable.declare_maxidx o Thm.maxidx_of) ths | SOME (Attribute _) => I (* FIXME !? *) | SOME (Declaration decl) => (fn ctxt => let val ctxt' = Context.proof_map (Morphism.form decl) ctxt in Variable.declare_maxidx (Variable.maxidx_of ctxt') ctxt end) | _ => I); (* fact values *) fun map_facts f = map_value (fn v => (case v of Source src => Source (map (map_facts f) src) | Fact (a, ths) => Fact (a, f a ths) | _ => v)); val trim_context_src = (map o map_facts) (K (map Thm.trim_context)); (* transform *) fun transform phi = map_value (fn v => (case v of Source src => Source (map (transform phi) src) | Literal _ => v | Name (a, psi) => Name (a, psi $> phi) | Typ T => Typ (Morphism.typ phi T) | Term t => Term (Morphism.term phi t) | Fact (a, ths) => Fact (a, Morphism.fact phi ths) | Attribute att => Attribute (Morphism.transform phi att) | Declaration decl => Declaration (Morphism.transform phi decl) | Files _ => v)); (* static binding *) (*1st stage: initialize assignable slots*) fun init_assignable tok = (case tok of Token (x, y, Slot) => Token (x, y, Assignable (Unsynchronized.ref NONE)) | Token (_, _, Value _) => tok | Token (_, _, Assignable r) => (r := NONE; tok)); (*2nd stage: assign values as side-effect of scanning*) fun assign v tok = (case tok of Token (x, y, Slot) => Token (x, y, Value v) | Token (_, _, Value _) => tok | Token (_, _, Assignable r) => (r := v; tok)); fun evaluate mk eval arg = let val x = eval arg in (assign (SOME (mk x)) arg; x) end; (*3rd stage: static closure of final values*) fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v) | closure tok = tok; (* pretty *) fun pretty_value ctxt tok = (case get_value tok of SOME (Literal markup) => let val x = content_of tok in Pretty.mark_str (keyword_markup markup x, x) end | SOME (Name ({print, ...}, _)) => Pretty.quote (Pretty.mark_str (print ctxt)) | SOME (Typ T) => Syntax.pretty_typ ctxt T | SOME (Term t) => Syntax.pretty_term ctxt t | SOME (Fact (_, ths)) => Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.cartouche o Thm.pretty_thm ctxt) ths)) | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok)); (* src *) fun dest_src ([]: src) = raise Fail "Empty token source" | dest_src (head :: args) = (head, args); fun name_of_src src = let val head = #1 (dest_src src); val name = (case get_name head of SOME {name, ...} => name | NONE => content_of head); in (name, pos_of head) end; val args_of_src = #2 o dest_src; fun pretty_src ctxt src = let val (head, args) = dest_src src; val prt_name = (case get_name head of SOME {print, ...} => Pretty.mark_str (print ctxt) | NONE => Pretty.str (content_of head)); in Pretty.block (Pretty.breaks (Pretty.quote prt_name :: map (pretty_value ctxt) args)) end; fun checked_src (head :: _) = is_some (get_name head) | checked_src [] = true; fun check_src ctxt get_table src = let val (head, args) = dest_src src; val table = get_table ctxt; in (case get_name head of SOME {name, ...} => (src, Name_Space.get table name) | NONE => let val pos = pos_of head; val (name, x) = Name_Space.check (Context.Proof ctxt) table (content_of head, pos); val _ = Context_Position.report ctxt pos Markup.operator; val kind = Name_Space.kind_of (Name_Space.space_of_table table); fun print ctxt' = Name_Space.markup_extern ctxt' (Name_Space.space_of_table (get_table ctxt')) name; val value = name_value {name = name, kind = kind, print = print}; val head' = closure (assign (SOME value) head); in (head' :: args, x) end) end; (** scanners **) open Basic_Symbol_Pos; val err_prefix = "Outer lexical error: "; fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); (* scan symbolic idents *) val scan_symid = Scan.many1 (Symbol.is_symbolic_char o Symbol_Pos.symbol) || Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single; fun is_symid str = (case try Symbol.explode str of SOME [s] => Symbol.is_symbolic s orelse Symbol.is_symbolic_char s | SOME ss => forall Symbol.is_symbolic_char ss | _ => false); fun ident_or_symbolic "begin" = false | ident_or_symbolic ":" = true | ident_or_symbolic "::" = true | ident_or_symbolic s = Symbol_Pos.is_identifier s orelse is_symid s; (* scan verbatim text *) val scan_verb = $$$ "*" --| Scan.ahead (~$$ "}") || Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s) >> single; val scan_verbatim = Scan.ahead ($$ "{" -- $$ "*") |-- !!! "unclosed verbatim text" ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") -- (Scan.repeats scan_verb -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos))); val recover_verbatim = $$$ "{" @@@ $$$ "*" @@@ Scan.repeats scan_verb; (* scan cartouche *) val scan_cartouche = Symbol_Pos.scan_pos -- ((Symbol_Pos.scan_cartouche err_prefix >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos); (* scan space *) fun space_symbol (s, _) = Symbol.is_blank s andalso s <> "\n"; val scan_space = Scan.many1 space_symbol @@@ Scan.optional ($$$ "\n") [] || Scan.many space_symbol @@@ $$$ "\n"; (* scan comment *) val scan_comment = Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body err_prefix -- Symbol_Pos.scan_pos); (** token sources **) local fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2; fun token k ss = Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot); fun token_range k (pos1, (ss, pos2)) = Token (Symbol_Pos.implode_range (pos1, pos2) ss, (k, Symbol_Pos.content ss), Slot); fun scan_token keywords = !!! "bad input" (Symbol_Pos.scan_string_qq err_prefix >> token_range String || Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String || scan_verbatim >> token_range Verbatim || scan_cartouche >> token_range Cartouche || scan_comment >> token_range (Comment NONE) || Comment.scan_outer >> (fn (k, ss) => token (Comment (SOME k)) ss) || scan_space >> token Space || (Scan.max token_leq (Scan.max token_leq (Scan.literal (Keyword.major_keywords keywords) >> pair Command) (Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword)) (Lexicon.scan_longid >> pair Long_Ident || Lexicon.scan_id >> pair Ident || Lexicon.scan_var >> pair Var || Lexicon.scan_tid >> pair Type_Ident || Lexicon.scan_tvar >> pair Type_Var || Symbol_Pos.scan_float >> pair Float || Symbol_Pos.scan_nat >> pair Nat || scan_symid >> pair Sym_Ident) >> uncurry token)); fun recover msg = (Symbol_Pos.recover_string_qq || Symbol_Pos.recover_string_bq || recover_verbatim || Symbol_Pos.recover_cartouche || Symbol_Pos.recover_comment || Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single) >> (single o token (Error msg)); in fun make_source keywords {strict} = let val scan_strict = Scan.bulk (scan_token keywords); val scan = if strict then scan_strict else Scan.recover scan_strict recover; in Source.source Symbol_Pos.stopper scan end; fun read_cartouche syms = (case Scan.read Symbol_Pos.stopper (scan_cartouche >> token_range Cartouche) syms of SOME tok => tok | NONE => error ("Single cartouche expected" ^ Position.here (#1 (Symbol_Pos.range syms)))); end; (* explode *) fun tokenize keywords strict syms = Source.of_list syms |> make_source keywords strict |> Source.exhaust; fun explode keywords pos text = Symbol_Pos.explode (text, pos) |> tokenize keywords {strict = false}; fun explode0 keywords = explode keywords Position.none; -(* print name in parsable form *) +(* print names in parsable form *) fun print_name keywords name = ((case explode keywords Position.none name of [tok] => not (member (op =) [Ident, Long_Ident, Sym_Ident, Nat] (kind_of tok)) | _ => true) ? Symbol_Pos.quote_string_qq) name; +fun print_properties keywords = + map (apply2 (print_name keywords) #> (fn (a, b) => a ^ " = " ^ b)) #> commas #> enclose "[" "]"; + (* make *) fun make ((k, n), s) pos = let val pos' = Position.advance_offsets n pos; val range = Position.range (pos, pos'); val tok = if 0 <= k andalso k < Vector.length immediate_kinds then Token ((s, range), (Vector.sub (immediate_kinds, k), s), Slot) else (case explode Keyword.empty_keywords pos s of [tok] => tok | _ => Token ((s, range), (Error (err_prefix ^ "exactly one token expected"), s), Slot)) in (tok, pos') end; fun make_string (s, pos) = let val Token ((x, _), y, z) = #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none); val pos' = Position.no_range_position pos; in Token ((x, (pos', pos')), y, z) end; val make_int = explode Keyword.empty_keywords Position.none o signed_string_of_int; fun make_src a args = make_string a :: args; (** parsers **) type 'a parser = T list -> 'a * T list; type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list); (* read body -- e.g. antiquotation source *) fun read_body keywords scan = tokenize (Keyword.no_command_keywords keywords) {strict = true} #> filter is_proper #> Scan.read stopper scan; fun read_antiq keywords scan (syms, pos) = (case read_body keywords scan syms of SOME x => x | NONE => error ("Malformed antiquotation" ^ Position.here pos)); (* wrapped syntax *) fun syntax_generic scan src context = let val (name, pos) = name_of_src src; val old_reports = maps reports_of_value src; val args1 = map init_assignable (args_of_src src); fun reported_text () = if Context_Position.reports_enabled_generic context then let val new_reports = maps (reports_of_value o closure) args1 in if old_reports <> new_reports then map (fn (p, m) => Position.reported_text p m "") new_reports else [] end else []; in (case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of (SOME x, (context', [])) => let val _ = Output.report (reported_text ()) in (x, context') end | (_, (context', args2)) => let val print_name = (case get_name (hd src) of NONE => quote name | SOME {kind, print, ...} => let val ctxt' = Context.proof_of context'; val (markup, xname) = print ctxt'; in plain_words kind ^ " " ^ quote (Markup.markup markup xname) end); val print_args = if null args2 then "" else ":\n " ^ space_implode " " (map print args2); in error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^ Markup.markup_report (implode (reported_text ()))) end) end; fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof; end; type 'a parser = 'a Token.parser; type 'a context_parser = 'a Token.context_parser; diff --git a/src/Pure/Isar/toplevel.ML b/src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML +++ b/src/Pure/Isar/toplevel.ML @@ -1,801 +1,786 @@ (* Title: Pure/Isar/toplevel.ML Author: Markus Wenzel, TU Muenchen Isabelle/Isar toplevel transactions. *) signature TOPLEVEL = sig exception UNDEF type state val init_toplevel: unit -> state val theory_toplevel: theory -> state val is_toplevel: state -> bool val is_theory: state -> bool val is_proof: state -> bool val is_skipped_proof: state -> bool val level: state -> int val previous_theory_of: state -> theory option val context_of: state -> Proof.context val generic_theory_of: state -> generic_theory val theory_of: state -> theory val proof_of: state -> Proof.state val proof_position_of: state -> int val is_end_theory: state -> bool val end_theory: Position.T -> state -> theory val presentation_context: state -> Proof.context val presentation_state: Proof.context -> state val pretty_context: state -> Pretty.T list val pretty_state: state -> Pretty.T list val string_of_state: state -> string val pretty_abstract: state -> Pretty.T type transition val empty: transition val name_of: transition -> string val pos_of: transition -> Position.T val timing_of: transition -> Time.time val type_error: transition -> string val name: string -> transition -> transition val position: Position.T -> transition -> transition val markers: Input.source list -> transition -> transition val timing: Time.time -> transition -> transition val init_theory: (unit -> theory) -> transition -> transition val is_init: transition -> bool val modify_init: (unit -> theory) -> transition -> transition val exit: transition -> transition val keep: (state -> unit) -> transition -> transition val keep': (bool -> state -> unit) -> transition -> transition val keep_proof: (state -> unit) -> transition -> transition val is_ignored: transition -> bool val ignored: Position.T -> transition val malformed: Position.T -> string -> transition val generic_theory: (generic_theory -> generic_theory) -> transition -> transition val theory': (bool -> theory -> theory) -> transition -> transition val theory: (theory -> theory) -> transition -> transition val begin_main_target: bool -> (theory -> local_theory) -> transition -> transition val end_main_target: transition -> transition val begin_nested_target: (Context.generic -> local_theory) -> transition -> transition val end_nested_target: transition -> transition val local_theory': (bool * Position.T) option -> (xstring * Position.T) option -> (bool -> local_theory -> local_theory) -> transition -> transition val local_theory: (bool * Position.T) option -> (xstring * Position.T) option -> (local_theory -> local_theory) -> transition -> transition val present_local_theory: (xstring * Position.T) option -> (state -> unit) -> transition -> transition val local_theory_to_proof': (bool * Position.T) option -> (xstring * Position.T) option -> (bool -> local_theory -> Proof.state) -> transition -> transition val local_theory_to_proof: (bool * Position.T) option -> (xstring * Position.T) option -> (local_theory -> Proof.state) -> transition -> transition val theory_to_proof: (theory -> Proof.state) -> transition -> transition val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition val forget_proof: transition -> transition val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition val proof: (Proof.state -> Proof.state) -> transition -> transition val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition val skip_proof: (unit -> unit) -> transition -> transition val skip_proof_open: transition -> transition val skip_proof_close: transition -> transition val exec_id: Document_ID.exec -> transition -> transition val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b - val add_hook: (transition -> state -> state -> unit) -> unit val transition: bool -> transition -> state -> state * (exn * string) option val command_errors: bool -> transition -> state -> Runtime.error list * state option val command_exception: bool -> transition -> state -> state val reset_theory: state -> state option val reset_proof: state -> state option val reset_notepad: state -> state option val fork_presentation: transition -> transition * transition type result val join_results: result -> (state * transition * state) list val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state end; structure Toplevel: TOPLEVEL = struct (** toplevel state **) exception UNDEF = Runtime.UNDEF; (* datatype node *) datatype node = Toplevel (*toplevel outside of theory body*) | Theory of generic_theory (*global or local theory*) | Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory) (*proof node, finish, original theory*) | Skipped_Proof of int * (generic_theory * generic_theory); (*proof depth, resulting theory, original theory*) val theory_node = fn Theory gthy => SOME gthy | _ => NONE; val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE; val skipped_proof_node = fn Skipped_Proof _ => true | _ => false; fun cases_node f _ _ Toplevel = f () | cases_node _ g _ (Theory gthy) = g gthy | cases_node _ _ h (Proof (prf, _)) = h (Proof_Node.current prf) | cases_node _ g _ (Skipped_Proof (_, (gthy, _))) = g gthy; fun cases_proper_node g h = cases_node (fn () => raise UNDEF) g h; val get_theory = cases_node (K NONE) (SOME o Context.theory_of) (SOME o Proof.theory_of); (* datatype state *) type node_presentation = node * Proof.context; fun init_presentation () = Proof_Context.init_global (Theory.get_pure_bootstrap ()); fun node_presentation node = (node, cases_node init_presentation Context.proof_of Proof.context_of node); datatype state = State of node_presentation * theory option; (*current node with presentation context, previous theory*) fun node_of (State ((node, _), _)) = node; fun previous_theory_of (State (_, prev_thy)) = prev_thy; fun init_toplevel () = State (node_presentation Toplevel, NONE); fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), NONE); fun level state = (case node_of state of Toplevel => 0 | Theory _ => 0 | Proof (prf, _) => Proof.level (Proof_Node.current prf) | Skipped_Proof (d, _) => d + 1); (*different notion of proof depth!*) fun str_of_state state = (case node_of state of Toplevel => (case previous_theory_of state of NONE => "at top level" | SOME thy => "at top level, result theory " ^ quote (Context.theory_name thy)) | Theory (Context.Theory _) => "in theory mode" | Theory (Context.Proof _) => "in local theory mode" | Proof _ => "in proof mode" | Skipped_Proof _ => "in skipped proof mode"); (* current node *) fun is_toplevel state = (case node_of state of Toplevel => true | _ => false); fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state)); fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state)); fun is_skipped_proof state = not (is_toplevel state) andalso skipped_proof_node (node_of state); fun proper_node_of state = if is_toplevel state then raise UNDEF else node_of state; fun proper_node_case f g state = cases_proper_node f g (proper_node_of state); val context_of = proper_node_case Context.proof_of Proof.context_of; val generic_theory_of = proper_node_case I (Context.Proof o Proof.context_of); val theory_of = proper_node_case Context.theory_of Proof.theory_of; val proof_of = proper_node_case (fn _ => error "No proof state") I; fun proof_position_of state = (case proper_node_of state of Proof (prf, _) => Proof_Node.position prf | _ => ~1); fun is_end_theory (State ((Toplevel, _), SOME _)) = true | is_end_theory _ = false; fun end_theory _ (State ((Toplevel, _), SOME thy)) = thy | end_theory pos _ = error ("Malformed theory" ^ Position.here pos); (* presentation context *) structure Presentation_State = Proof_Data ( type T = state option; fun init _ = NONE; ); fun presentation_context0 (State ((_, pr_ctxt), _)) = pr_ctxt; fun presentation_context (state as State (current, _)) = presentation_context0 state |> Presentation_State.put (SOME (State (current, NONE))); fun presentation_state ctxt = (case Presentation_State.get ctxt of NONE => State (node_presentation (Theory (Context.Proof ctxt)), NONE) | SOME state => state); (* print state *) fun pretty_context state = if is_toplevel state then [] else let val gthy = (case node_of state of Toplevel => raise Match | Theory gthy => gthy | Proof (_, (_, gthy)) => gthy | Skipped_Proof (_, (_, gthy)) => gthy); val lthy = Context.cases Named_Target.theory_init I gthy; in Local_Theory.pretty lthy end; fun pretty_state state = (case node_of state of Toplevel => [] | Theory _ => [] | Proof (prf, _) => Proof.pretty_state (Proof_Node.current prf) | Skipped_Proof (d, _) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]); val string_of_state = pretty_state #> Pretty.chunks #> Pretty.string_of; fun pretty_abstract state = Pretty.str (""); val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_abstract); (** toplevel transitions **) (* primitive transitions *) datatype trans = (*init theory*) Init of unit -> theory | (*formal exit of theory*) Exit | (*peek at state*) Keep of bool -> state -> unit | (*node transaction and presentation*) Transaction of (bool -> node -> node_presentation) * (state -> unit); local exception FAILURE of state * exn; fun apply f g node = let val node_pr = node_presentation node; val context = cases_proper_node I (Context.Proof o Proof.context_of) node; fun state_error e node_pr' = (State (node_pr', get_theory node), e); val (result, err) = node |> Runtime.controlled_execution (SOME context) f |> state_error NONE handle exn => state_error (SOME exn) node_pr; in (case err of NONE => tap g result | SOME exn => raise FAILURE (result, exn)) end; fun apply_tr int trans state = (case (trans, node_of state) of (Init f, Toplevel) => Runtime.controlled_execution NONE (fn () => State (node_presentation (Theory (Context.Theory (f ()))), NONE)) () | (Exit, node as Theory (Context.Theory thy)) => let val State ((node', pr_ctxt), _) = node |> apply (fn _ => node_presentation (Theory (Context.Theory (tap Thm.expose_theory (Theory.end_theory thy))))) (K ()); in State ((Toplevel, pr_ctxt), get_theory node') end | (Keep f, node) => Runtime.controlled_execution (try generic_theory_of state) (fn () => (f int state; State (node_presentation node, previous_theory_of state))) () | (Transaction _, Toplevel) => raise UNDEF | (Transaction (f, g), node) => apply (fn x => f int x) g node | _ => raise UNDEF); fun apply_union _ [] state = raise FAILURE (state, UNDEF) | apply_union int (tr :: trs) state = apply_union int trs state handle Runtime.UNDEF => apply_tr int tr state | FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state | exn as FAILURE _ => raise exn | exn => raise FAILURE (state, exn); fun apply_markers name markers (state as State ((node, pr_ctxt), prev_thy)) = let val state' = Runtime.controlled_execution (try generic_theory_of state) (fn () => State ((node, fold (Document_Marker.evaluate name) markers pr_ctxt), prev_thy)) (); in (state', NONE) end handle exn => (state, SOME exn); in fun apply_trans int name markers trans state = (apply_union int trans state |> apply_markers name markers) handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn); end; (* datatype transition *) datatype transition = Transition of {name: string, (*command name*) pos: Position.T, (*source position*) markers: Input.source list, (*semantic document markers*) timing: Time.time, (*prescient timing information*) trans: trans list}; (*primitive transitions (union)*) fun make_transition (name, pos, markers, timing, trans) = Transition {name = name, pos = pos, markers = markers, timing = timing, trans = trans}; fun map_transition f (Transition {name, pos, markers, timing, trans}) = make_transition (f (name, pos, markers, timing, trans)); val empty = make_transition ("", Position.none, [], Time.zeroTime, []); (* diagnostics *) fun name_of (Transition {name, ...}) = name; fun pos_of (Transition {pos, ...}) = pos; fun timing_of (Transition {timing, ...}) = timing; fun command_msg msg tr = msg ^ "command " ^ quote (Markup.markup Markup.keyword1 (name_of tr)) ^ Position.here (pos_of tr); fun at_command tr = command_msg "At " tr; fun type_error tr = command_msg "Bad context for " tr; (* modify transitions *) fun name name = map_transition (fn (_, pos, markers, timing, trans) => (name, pos, markers, timing, trans)); fun position pos = map_transition (fn (name, _, markers, timing, trans) => (name, pos, markers, timing, trans)); fun markers markers = map_transition (fn (name, pos, _, timing, trans) => (name, pos, markers, timing, trans)); fun timing timing = map_transition (fn (name, pos, markers, _, trans) => (name, pos, markers, timing, trans)); fun add_trans tr = map_transition (fn (name, pos, markers, timing, trans) => (name, pos, markers, timing, tr :: trans)); val reset_trans = map_transition (fn (name, pos, markers, timing, _) => (name, pos, markers, timing, [])); (* basic transitions *) fun init_theory f = add_trans (Init f); fun is_init (Transition {trans = [Init _], ...}) = true | is_init _ = false; fun modify_init f tr = if is_init tr then init_theory f (reset_trans tr) else tr; val exit = add_trans Exit; val keep' = add_trans o Keep; fun present_transaction f g = add_trans (Transaction (f, g)); fun transaction f = present_transaction f (K ()); fun transaction0 f = present_transaction (node_presentation oo f) (K ()); fun keep f = add_trans (Keep (fn _ => f)); fun keep_proof f = keep (fn st => if is_proof st then f st else if is_skipped_proof st then () else warning "No proof state"); fun is_ignored tr = name_of tr = ""; fun ignored pos = empty |> name "" |> position pos |> keep (fn _ => ()); fun malformed pos msg = empty |> name "" |> position pos |> keep (fn _ => error msg); (* theory transitions *) fun generic_theory f = transaction (fn _ => (fn Theory gthy => node_presentation (Theory (f gthy)) | _ => raise UNDEF)); fun theory' f = transaction (fn int => (fn Theory (Context.Theory thy) => let val thy' = thy |> Sign.new_group |> f int |> Sign.reset_group; in node_presentation (Theory (Context.Theory thy')) end | _ => raise UNDEF)); fun theory f = theory' (K f); fun begin_main_target begin f = transaction (fn _ => (fn Theory (Context.Theory thy) => let val lthy = f thy; val gthy = if begin then Context.Proof lthy else Target_Context.end_named_cmd lthy; val _ = (case Local_Theory.pretty lthy of [] => () | prts => Output.state (Pretty.string_of (Pretty.chunks prts))); in (Theory gthy, lthy) end | _ => raise UNDEF)); val end_main_target = transaction (fn _ => (fn Theory (Context.Proof lthy) => (Theory (Target_Context.end_named_cmd lthy), lthy) | _ => raise UNDEF)); fun begin_nested_target f = transaction0 (fn _ => (fn Theory gthy => let val lthy' = f gthy; in Theory (Context.Proof lthy') end | _ => raise UNDEF)); val end_nested_target = transaction (fn _ => (fn Theory (Context.Proof lthy) => (case try Target_Context.end_nested_cmd lthy of SOME gthy' => (Theory gthy', lthy) | NONE => raise UNDEF) | _ => raise UNDEF)); fun restricted_context (SOME (strict, scope)) = Proof_Context.map_naming (Name_Space.restricted strict scope) | restricted_context NONE = I; fun local_theory' restricted target f = present_transaction (fn int => (fn Theory gthy => let val (finish, lthy) = Target_Context.switch_named_cmd target gthy; val lthy' = lthy |> restricted_context restricted |> Local_Theory.new_group |> f int |> Local_Theory.reset_group; in (Theory (finish lthy'), lthy') end | _ => raise UNDEF)) (K ()); fun local_theory restricted target f = local_theory' restricted target (K f); fun present_local_theory target = present_transaction (fn _ => (fn Theory gthy => let val (finish, lthy) = Target_Context.switch_named_cmd target gthy; in (Theory (finish lthy), lthy) end | _ => raise UNDEF)); (* proof transitions *) fun end_proof f = transaction (fn int => (fn Proof (prf, (finish, _)) => let val state = Proof_Node.current prf in if can (Proof.assert_bottom true) state then let val ctxt' = f int state; val gthy' = finish ctxt'; in (Theory gthy', ctxt') end else raise UNDEF end | Skipped_Proof (0, (gthy, _)) => node_presentation (Theory gthy) | _ => raise UNDEF)); local fun begin_proof init_proof = transaction0 (fn int => (fn Theory gthy => let val (finish, prf) = init_proof int gthy; val document = Options.default_string "document"; val skip = (document = "" orelse document = "false") andalso Goal.skip_proofs_enabled (); val schematic_goal = try Proof.schematic_goal prf; val _ = if skip andalso schematic_goal = SOME true then warning "Cannot skip proof of schematic goal statement" else (); in if skip andalso schematic_goal = SOME false then Skipped_Proof (0, (finish (Proof.global_skip_proof true prf), gthy)) else Proof (Proof_Node.init prf, (finish, gthy)) end | _ => raise UNDEF)); in fun local_theory_to_proof' restricted target f = begin_proof (fn int => fn gthy => let val (finish, lthy) = Target_Context.switch_named_cmd target gthy; val prf = lthy |> restricted_context restricted |> Local_Theory.new_group |> f int; in (finish o Local_Theory.reset_group, prf) end); fun local_theory_to_proof restricted target f = local_theory_to_proof' restricted target (K f); fun theory_to_proof f = begin_proof (fn _ => fn gthy => (Context.Theory o Sign.reset_group o Sign.change_check o Proof_Context.theory_of, (case gthy of Context.Theory thy => f (Sign.new_group thy) | _ => raise UNDEF))); end; val forget_proof = transaction0 (fn _ => (fn Proof (prf, (_, orig_gthy)) => if Proof.is_notepad (Proof_Node.current prf) then raise UNDEF else Theory orig_gthy | Skipped_Proof (_, (_, orig_gthy)) => Theory orig_gthy | _ => raise UNDEF)); fun proofs' f = transaction0 (fn int => (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x) | skip as Skipped_Proof _ => skip | _ => raise UNDEF)); fun proof' f = proofs' ((Seq.single o Seq.Result) oo f); val proofs = proofs' o K; val proof = proof' o K; (* skipped proofs *) fun actual_proof f = transaction0 (fn _ => (fn Proof (prf, x) => Proof (f prf, x) | _ => raise UNDEF)); fun skip_proof f = transaction0 (fn _ => (fn skip as Skipped_Proof _ => (f (); skip) | _ => raise UNDEF)); val skip_proof_open = transaction0 (fn _ => (fn Skipped_Proof (d, x) => Skipped_Proof (d + 1, x) | _ => raise UNDEF)); val skip_proof_close = transaction0 (fn _ => (fn Skipped_Proof (0, (gthy, _)) => Theory gthy | Skipped_Proof (d, x) => Skipped_Proof (d - 1, x) | _ => raise UNDEF)); (** toplevel transactions **) (* runtime position *) fun exec_id id (tr as Transition {pos, ...}) = let val put_id = Position.put_id (Document_ID.print id) in position (put_id pos) tr end; fun setmp_thread_position (Transition {pos, ...}) f x = Position.setmp_thread_data pos f x; -(* post-transition hooks *) - -local - val hooks = - Synchronized.var "Toplevel.hooks" ([]: (transition -> state -> state -> unit) list); -in - -fun add_hook hook = Synchronized.change hooks (cons hook); -fun get_hooks () = Synchronized.value hooks; - -end; - - (* apply transitions *) local fun app int (tr as Transition {name, markers, trans, ...}) = setmp_thread_position tr (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int name markers trans) ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn)); in fun transition int tr st = let val (st', opt_err) = Context.setmp_generic_context (try (Context.Proof o presentation_context0) st) (fn () => app int tr st) (); val opt_err' = opt_err |> Option.map (fn Runtime.EXCURSION_FAIL exn_info => exn_info | exn => (Runtime.exn_context (try context_of st) exn, at_command tr)); - val _ = get_hooks () |> List.app (fn f => ignore \<^try>\f tr st st'\); in (st', opt_err') end; end; (* managed commands *) fun command_errors int tr st = (case transition int tr st of (st', NONE) => ([], SOME st') | (_, SOME (exn, _)) => (Runtime.exn_messages exn, NONE)); fun command_exception int tr st = (case transition int tr st of (st', NONE) => st' | (_, SOME (exn, info)) => if Exn.is_interrupt exn then Exn.reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)); val command = command_exception false; (* reset state *) local fun reset_state check trans st = if check st then NONE else #2 (command_errors false (trans empty) st); in val reset_theory = reset_state is_theory forget_proof; val reset_proof = reset_state is_proof (transaction0 (fn _ => (fn Theory gthy => Skipped_Proof (0, (gthy, gthy)) | _ => raise UNDEF))); val reset_notepad = reset_state (fn st => (case try proof_of st of SOME state => not (Proof.is_notepad state) orelse can Proof.end_notepad state | NONE => true)) (proof Proof.reset_notepad); end; (* scheduled proof result *) datatype result = Result of transition * state | Result_List of result list | Result_Future of result future; fun join_results result = let fun add (tr, st') res = (case res of [] => [(init_toplevel (), tr, st')] | (_, _, st) :: _ => (st, tr, st') :: res); fun acc (Result r) = add r | acc (Result_List rs) = fold acc rs | acc (Result_Future x) = acc (Future.join x); in rev (acc result []) end; local structure Result = Proof_Data ( type T = result; fun init _ = Result_List []; ); val get_result = Result.get o Proof.context_of; val put_result = Proof.map_context o Result.put; fun timing_estimate elem = let val trs = tl (Thy_Element.flat_element elem) in fold (fn tr => fn t => timing_of tr + t) trs Time.zeroTime end; fun future_proofs_enabled estimate st = (case try proof_of st of NONE => false | SOME state => not (Proofterm.proofs_enabled ()) andalso not (Proof.is_relevant state) andalso (if can (Proof.assert_bottom true) state then Future.proofs_enabled 1 else Future.proofs_enabled 2 orelse Future.proofs_enabled_timing estimate)); val empty_markers = markers []; val empty_trans = reset_trans #> keep (K ()); in fun fork_presentation tr = (tr |> empty_markers, tr |> empty_trans); fun atom_result keywords tr st = let val st' = if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then let val (tr1, tr2) = fork_presentation tr; val _ = Execution.fork {name = "Toplevel.diag", pos = pos_of tr, pri = ~1} (fn () => command tr1 st); in command tr2 st end else command tr st; in (Result (tr, st'), st') end; fun element_result keywords (Thy_Element.Element (tr, NONE)) st = atom_result keywords tr st | element_result keywords (elem as Thy_Element.Element (head_tr, SOME element_rest)) st = let val (head_result, st') = atom_result keywords head_tr st; val (body_elems, end_tr) = element_rest; val estimate = timing_estimate elem; in if not (future_proofs_enabled estimate st') then let val proof_trs = maps Thy_Element.flat_element body_elems @ [end_tr]; val (proof_results, st'') = fold_map (atom_result keywords) proof_trs st'; in (Result_List (head_result :: proof_results), st'') end else let val (end_tr1, end_tr2) = fork_presentation end_tr; val finish = Context.Theory o Proof_Context.theory_of; val future_proof = Proof.future_proof (fn state => Execution.fork {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1} (fn () => let val State ((Proof (prf, (_, orig_gthy)), _), prev_thy) = st'; val node' = Proof (Proof_Node.apply (K state) prf, (finish, orig_gthy)); val (results, result_state) = State (node_presentation node', prev_thy) |> fold_map (element_result keywords) body_elems ||> command end_tr1; in (Result_List results, presentation_context0 result_state) end)) #> (fn (res, state') => state' |> put_result (Result_Future res)); val forked_proof = proof (future_proof #> (fn state => state |> Proof.local_done_proof |> put_result (get_result state))) o end_proof (fn _ => future_proof #> (fn state => state |> Proof.global_done_proof |> Result.put (get_result state))); val st'' = st' |> command (head_tr |> reset_trans |> forked_proof); val end_st = st'' |> command end_tr2; val end_result = Result (end_tr, end_st); val result = Result_List [head_result, Result.get (presentation_context0 st''), end_result]; in (result, end_st) end end; end; end; diff --git a/src/Pure/System/isabelle_tool.scala b/src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala +++ b/src/Pure/System/isabelle_tool.scala @@ -1,234 +1,235 @@ /* Title: Pure/System/isabelle_tool.scala Author: Makarius Author: Lars Hupel Isabelle system tools: external executables or internal Scala functions. */ package isabelle import java.net.URLClassLoader import scala.reflect.runtime.universe import scala.tools.reflect.{ToolBox, ToolBoxError} object Isabelle_Tool { /* Scala source tools */ abstract class Body extends Function[List[String], Unit] private def compile(path: Path): Body = { def err(msg: String): Nothing = cat_error(msg, "The error(s) above occurred in Isabelle/Scala tool " + path) val source = File.read(path) val class_loader = new URLClassLoader(Array(), getClass.getClassLoader) val tool_box = universe.runtimeMirror(class_loader).mkToolBox() try { val tree = tool_box.parse(source) val module = try { tree.asInstanceOf[universe.ModuleDef] } catch { case _: java.lang.ClassCastException => err("Source does not describe a module (Scala object)") } tool_box.compile(universe.Ident(tool_box.define(module)))() match { case body: Body => body case _ => err("Ill-typed source: Isabelle_Tool.Body expected") } } catch { case e: ToolBoxError => if (tool_box.frontEnd.hasErrors) { val infos = tool_box.frontEnd.infos.toList val msgs = infos.map(info => "Error in line " + info.pos.line + ":\n" + info.msg) err(msgs.mkString("\n")) } else err(e.toString) } } /* external tools */ private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS")) private def is_external(dir: Path, file_name: String): Boolean = { val file = (dir + Path.explode(file_name)).file try { file.isFile && file.canRead && (file_name.endsWith(".scala") || file.canExecute) && !file_name.endsWith("~") && !file_name.endsWith(".orig") } catch { case _: SecurityException => false } } private def find_external(name: String): Option[List[String] => Unit] = dirs().collectFirst({ case dir if is_external(dir, name + ".scala") => compile(dir + Path.explode(name + ".scala")) case dir if is_external(dir, name) => (args: List[String]) => { val tool = dir + Path.explode(name) val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args)) sys.exit(result.print_stdout.rc) } }) /* internal tools */ private lazy val internal_tools: List[Isabelle_Tool] = Isabelle_System.make_services(classOf[Isabelle_Scala_Tools]).flatMap(_.tools) private def find_internal(name: String): Option[List[String] => Unit] = internal_tools.collectFirst({ case tool if tool.name == name => args => Command_Line.tool { tool.body(args) } }) /* list tools */ abstract class Entry { def name: String def position: Properties.T def description: String def print: String = description match { case "" => name case descr => name + " - " + descr } } sealed case class External(name: String, path: Path) extends Entry { def position: Properties.T = Position.File(path.absolute.implode) def description: String = { val Pattern = """.*\bDESCRIPTION: *(.*)""".r split_lines(File.read(path)).collectFirst({ case Pattern(s) => s }) getOrElse "" } } def external_tools(): List[External] = { for { dir <- dirs() if dir.is_dir file_name <- File.read_dir(dir) if is_external(dir, file_name) } yield { val path = dir + Path.explode(file_name) val name = Library.perhaps_unsuffix(".scala", file_name) External(name, path) } } def isabelle_tools(): List[Entry] = (external_tools() ::: internal_tools).sortBy(_.name) object Isabelle_Tools extends Scala.Fun_String("isabelle_tools") { val here = Scala_Project.here def apply(arg: String): String = if (arg.nonEmpty) error("Bad argument: " + quote(arg)) else { val result = isabelle_tools().map(entry => (entry.name, entry.position)) val body = { import XML.Encode._; list(pair(string, properties))(result) } YXML.string_of_body(body) } } /* command line entry point */ def main(args: Array[String]): Unit = { Command_Line.tool { args.toList match { case Nil | List("-?") => val tool_descriptions = isabelle_tools().map(_.print) Getopts(""" Usage: isabelle TOOL [ARGS ...] Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help. Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage() case tool_name :: tool_args => find_external(tool_name) orElse find_internal(tool_name) match { case Some(tool) => tool(tool_args) case None => error("Unknown Isabelle tool: " + quote(tool_name)) } } } } } sealed case class Isabelle_Tool( name: String, description: String, here: Scala_Project.Here, body: List[String] => Unit) extends Isabelle_Tool.Entry { def position: Position.T = here.position } class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) extends Isabelle_System.Service class Tools extends Isabelle_Scala_Tools( Build.isabelle_tool, Build_Docker.isabelle_tool, Build_Job.isabelle_tool, Doc.isabelle_tool, Dump.isabelle_tool, Export.isabelle_tool, ML_Process.isabelle_tool, Mercurial.isabelle_tool, Mkroot.isabelle_tool, Logo.isabelle_tool, Options.isabelle_tool, Phabricator.isabelle_tool1, Phabricator.isabelle_tool2, Phabricator.isabelle_tool3, Phabricator.isabelle_tool4, Presentation.isabelle_tool, Profiling_Report.isabelle_tool, Server.isabelle_tool, Sessions.isabelle_tool, Scala_Project.isabelle_tool, Update.isabelle_tool, Update_Cartouches.isabelle_tool, Update_Comments.isabelle_tool, Update_Header.isabelle_tool, Update_Then.isabelle_tool, Update_Theorems.isabelle_tool, + isabelle.mirabelle.Mirabelle.isabelle_tool, isabelle.vscode.TextMate_Grammar.isabelle_tool, isabelle.vscode.Language_Server.isabelle_tool) class Admin_Tools extends Isabelle_Scala_Tools( Build_CSDP.isabelle_tool, Build_Cygwin.isabelle_tool, Build_Doc.isabelle_tool, Build_E.isabelle_tool, Build_Fonts.isabelle_tool, Build_JCEF.isabelle_tool, Build_JDK.isabelle_tool, Build_JEdit.isabelle_tool, Build_PolyML.isabelle_tool1, Build_PolyML.isabelle_tool2, Build_SPASS.isabelle_tool, Build_SQLite.isabelle_tool, Build_Status.isabelle_tool, Build_Vampire.isabelle_tool, Build_VeriT.isabelle_tool, Build_Zipperposition.isabelle_tool, Check_Sources.isabelle_tool, Components.isabelle_tool, isabelle.vscode.Build_VSCode.isabelle_tool) diff --git a/src/Pure/Thy/thy_info.ML b/src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML +++ b/src/Pure/Thy/thy_info.ML @@ -1,475 +1,483 @@ (* Title: Pure/Thy/thy_info.ML Author: Makarius Global theory info database, with auto-loading according to theory and file dependencies, and presentation of theory documents. *) signature THY_INFO = sig type presentation_context = {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, segments: Thy_Output.segment list} val adjust_pos_properties: presentation_context -> Position.T -> Properties.T val apply_presentation: presentation_context -> theory -> unit val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory val get_names: unit -> string list val lookup_theory: string -> theory option val get_theory: string -> theory val master_directory: string -> Path.T val remove_thy: string -> unit val use_theories: Options.T -> string -> (string * Position.T) list -> unit val use_thy: string -> unit val script_thy: Position.T -> string -> theory -> theory val register_thy: theory -> unit val finish: unit -> unit end; structure Thy_Info: THY_INFO = struct (** theory presentation **) (* artefact names *) fun document_name ext thy = Path.explode_binding0 ("document/" ^ Context.theory_name thy ^ "." ^ ext); val document_tex_name = document_name "tex"; (* hook for consolidated theory *) type presentation_context = {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, segments: Thy_Output.segment list}; fun adjust_pos_properties (context: presentation_context) pos = Position.offset_properties_of (#adjust_pos context pos) @ Position.id_properties_of pos; structure Presentation = Theory_Data ( type T = ((presentation_context -> theory -> unit) * stamp) list; val empty = []; val extend = I; fun merge data : T = Library.merge (eq_snd op =) data; ); +fun sequential_presentation options = + not (Options.bool options \<^system_option>\parallel_presentation\); + fun apply_presentation (context: presentation_context) thy = - ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy)); + Par_List.map' + {name = "apply_presentation", sequential = sequential_presentation (#options context)} + (fn (f, _) => f context thy) (Presentation.get thy) + |> ignore; fun add_presentation f = Presentation.map (cons (f, stamp ())); val _ = Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => if exists (Toplevel.is_skipped_proof o #state) segments then () else let val body = Thy_Output.present_thy options thy segments; in if Options.string options "document" = "false" then () else let val thy_name = Context.theory_name thy; val document_tex_name = document_tex_name thy; val latex = Latex.isabelle_body thy_name body; val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; in Export.export thy document_tex_name (XML.blob output) end end)); (** thy database **) (* messages *) val show_path = space_implode " via " o map quote; fun cycle_msg names = "Cyclic dependency of " ^ show_path names; (* derived graph operations *) fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess)); fun new_entry name parents entry = String_Graph.new_node (name, entry) #> add_deps name parents; (* global thys *) type deps = {master: (Path.T * SHA1.digest), (*master dependencies for thy file*) imports: (string * Position.T) list}; (*source specification of imports (partially qualified)*) fun make_deps master imports : deps = {master = master, imports = imports}; fun master_dir_deps (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d); local val global_thys = Synchronized.var "Thy_Info.thys" (String_Graph.empty: (deps option * theory option) String_Graph.T); in fun get_thys () = Synchronized.value global_thys; fun change_thys f = Synchronized.change global_thys f; end; fun get_names () = String_Graph.topological_order (get_thys ()); (* access thy *) fun lookup thys name = try (String_Graph.get_node thys) name; fun lookup_thy name = lookup (get_thys ()) name; fun get thys name = (case lookup thys name of SOME thy => thy | NONE => error ("Theory loader: nothing known about theory " ^ quote name)); fun get_thy name = get (get_thys ()) name; (* access deps *) val lookup_deps = Option.map #1 o lookup_thy; val master_directory = master_dir_deps o #1 o get_thy; (* access theory *) fun lookup_theory name = (case lookup_thy name of SOME (_, SOME theory) => SOME theory | _ => NONE); fun get_theory name = (case lookup_theory name of SOME theory => theory | _ => error ("Theory loader: undefined entry for theory " ^ quote name)); val get_imports = Resources.imports_of o get_theory; (** thy operations **) (* remove *) fun remove name thys = (case lookup thys name of NONE => thys | SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name) | SOME _ => let val succs = String_Graph.all_succs thys [name]; val _ = writeln ("Theory loader: removing " ^ commas_quote succs); in fold String_Graph.del_node succs thys end); val remove_thy = change_thys o remove; (* update *) fun update deps theory thys = let val name = Context.theory_long_name theory; val parents = map Context.theory_long_name (Theory.parents_of theory); val thys' = remove name thys; val _ = map (get thys') parents; in new_entry name parents (SOME deps, SOME theory) thys' end; fun update_thy deps theory = change_thys (update deps theory); (* scheduling loader tasks *) datatype result = Result of {theory: theory, exec_id: Document_ID.exec, present: unit -> unit, commit: unit -> unit, weight: int}; fun theory_result theory = Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0}; fun result_theory (Result {theory, ...}) = theory; fun result_present (Result {present, ...}) = present; fun result_commit (Result {commit, ...}) = commit; fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i); fun join_theory (Result {theory, exec_id, ...}) = let val _ = Execution.join [exec_id]; val res = Exn.capture Thm.consolidate_theory theory; val exns = maps Task_Queue.group_status (Execution.peek exec_id); in res :: map Exn.Exn exns end; datatype task = Task of string list * (theory list -> result) | Finished of theory; fun task_finished (Task _) = false | task_finished (Finished _) = true; fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents; val schedule_seq = String_Graph.schedule (fn deps => fn (_, task) => (case task of Task (parents, body) => let val result = body (task_parents deps parents); val _ = Par_Exn.release_all (join_theory result); val _ = result_present result (); val _ = result_commit result (); in result_theory result end | Finished thy => thy)) #> ignore; val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks => let val futures = tasks |> String_Graph.schedule (fn deps => fn (name, task) => (case task of Task (parents, body) => (singleton o Future.forks) {name = "theory:" ^ name, group = NONE, deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true} (fn () => (case filter (not o can Future.join o #2) deps of [] => body (map (result_theory o Future.join) (task_parents deps parents)) | bad => error ("Failed to load theory " ^ quote name ^ " (unresolved " ^ commas_quote (map #1 bad) ^ ")"))) | Finished theory => Future.value (theory_result theory))); val results1 = futures |> maps (fn future => (case Future.join_result future of Exn.Res result => join_theory result | Exn.Exn exn => [Exn.Exn exn])); val results2 = futures |> map_filter (Exn.get_res o Future.join_result) |> sort result_ord - |> Par_List.map (fn result => Exn.capture (result_present result) ()); + |> Par_List.map' + {name = "present", sequential = sequential_presentation (Options.default ())} + (fn result => Exn.capture (result_present result) ()); (* FIXME more precise commit order (!?) *) val results3 = futures |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ()); (* FIXME avoid global Execution.reset (!??) *) val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ())); val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4); in () end); (* eval theory *) fun eval_thy options master_dir header text_pos text parents = let val (name, _) = #name header; val keywords = fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents (Keyword.add_keywords (#keywords header) Keyword.empty_keywords); val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text); val elements = Thy_Element.parse_elements keywords spans; val text_id = Position.copy_id text_pos Position.none; fun init () = Resources.begin_theory master_dir header parents; fun excursion () = let fun element_result span_elem (st, _) = let fun prepare span = let val tr = Position.setmp_thread_data text_id (fn () => Command.read_span keywords st master_dir init span) (); in Toplevel.timing (Resources.last_timing tr) tr end; val elem = Thy_Element.map_element prepare span_elem; val (results, st') = Toplevel.element_result keywords elem st; val pos' = Toplevel.pos_of (Thy_Element.last_element elem); in (results, (st', pos')) end; val (results, (end_state, end_pos)) = fold_map element_result elements (Toplevel.init_toplevel (), Position.none); val thy = Toplevel.end_theory end_pos end_state; in (results, thy) end; val (results, thy) = cond_timeit true ("theory " ^ quote name) excursion; fun present () = let val segments = (spans ~~ maps Toplevel.join_results results) |> map (fn (span, (st, tr, st')) => {span = span, prev_state = st, command = tr, state = st'}); val context: presentation_context = {options = options, file_pos = text_pos, adjust_pos = I, segments = segments}; in apply_presentation context thy end; in (thy, present, size text) end; (* require_thy -- checking database entries wrt. the file-system *) local fun required_by _ [] = "" | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; fun load_thy options initiators deps text (name, header_pos) keywords parents = let val {master = (thy_path, _), imports} = deps; val dir = Path.dir thy_path; val exec_id = Document_ID.make (); val id = Document_ID.print exec_id; val put_id = Position.put_id id; val _ = Execution.running Document_ID.none exec_id [] orelse raise Fail ("Failed to register execution: " ^ id); val text_pos = put_id (Path.position thy_path); val text_props = Position.properties_of text_pos; val _ = remove_thy name; val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators); val _ = Output.try_protocol_message (Markup.loading_theory name @ text_props) [XML.blob [text]]; val _ = Position.setmp_thread_data (Position.id_only id) (fn () => (parents, map #2 imports) |> ListPair.app (fn (thy, pos) => Context_Position.reports_global thy [(put_id pos, Theory.get_markup thy)])) (); val timing_start = Timing.start (); val header = Thy_Header.make (name, put_id header_pos) imports keywords; val (theory, present, weight) = eval_thy options dir header text_pos text (if name = Context.PureN then [Context.the_global_context ()] else parents); val timing_result = Timing.result timing_start; val timing_props = [Markup.theory_timing, (Markup.nameN, name)]; val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) [] fun commit () = update_thy deps theory; in Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight} end; fun check_thy_deps dir name = (case lookup_deps name of SOME NONE => (true, NONE, Position.none, get_imports name, []) | NONE => let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end | SOME (SOME {master, ...}) => let val {master = master', text = text', theory_pos = theory_pos', imports = imports', keywords = keywords'} = Resources.check_thy dir name; val deps' = SOME (make_deps master' imports', text'); val current = #2 master = #2 master' andalso (case lookup_theory name of NONE => false | SOME theory => Resources.loaded_files_current theory); in (current, deps', theory_pos', imports', keywords') end); in fun require_thys options initiators qualifier dir strs tasks = fold_map (require_thy options initiators qualifier dir) strs tasks |>> forall I and require_thy options initiators qualifier dir (s, require_pos) tasks = let val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s; in (case try (String_Graph.get_node tasks) theory_name of SOME task => (task_finished task, tasks) | NONE => let val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators); val (current, deps, theory_pos, imports, keywords) = check_thy_deps master_dir theory_name handle ERROR msg => cat_error msg ("The error(s) above occurred for theory " ^ quote theory_name ^ Position.here require_pos ^ required_by "\n" initiators); val qualifier' = Resources.theory_qualifier theory_name; val dir' = dir + master_dir_deps (Option.map #1 deps); val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports; val (parents_current, tasks') = require_thys options (theory_name :: initiators) qualifier' dir' imports tasks; val all_current = current andalso parents_current; val task = if all_current then Finished (get_theory theory_name) else (case deps of NONE => raise Fail "Malformed deps" | SOME (dep, text) => Task (parents, load_thy options initiators dep text (theory_name, theory_pos) keywords)); val tasks'' = new_entry theory_name parents task tasks'; in (all_current, tasks'') end) end; end; (* use theories *) fun use_theories options qualifier imports = let val (_, tasks) = require_thys options [] qualifier Path.current imports String_Graph.empty in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end; fun use_thy name = use_theories (Options.default ()) Resources.default_qualifier [(name, Position.none)]; (* toplevel scripting -- without maintaining database *) fun script_thy pos txt thy = let val trs = Outer_Syntax.parse_text thy (K thy) pos txt; val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs); val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ()); in Toplevel.end_theory end_pos end_state end; (* register theory *) fun register_thy theory = let val name = Context.theory_long_name theory; val {master, ...} = Resources.check_thy (Resources.master_directory theory) name; val imports = Resources.imports_of theory; in change_thys (fn thys => let val thys' = remove name thys; val _ = writeln ("Registering theory " ^ quote name); in update (make_deps master imports) theory thys' end) end; (* finish all theories *) fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry))); end; fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name); diff --git a/src/Pure/build-jars b/src/Pure/build-jars --- a/src/Pure/build-jars +++ b/src/Pure/build-jars @@ -1,326 +1,327 @@ #!/usr/bin/env bash # # Author: Makarius # # build-jars - build Isabelle/Scala # # Requires proper Isabelle settings environment. ## sources declare -a SOURCES=( src/HOL/SPARK/Tools/spark.scala src/HOL/Tools/ATP/system_on_tptp.scala + src/HOL/Tools/Mirabelle/mirabelle.scala src/HOL/Tools/Nitpick/kodkod.scala src/Pure/Admin/afp.scala src/Pure/Admin/build_csdp.scala src/Pure/Admin/build_cygwin.scala src/Pure/Admin/build_doc.scala src/Pure/Admin/build_e.scala src/Pure/Admin/build_fonts.scala src/Pure/Admin/build_history.scala src/Pure/Admin/build_jcef.scala src/Pure/Admin/build_jdk.scala src/Pure/Admin/build_jedit.scala src/Pure/Admin/build_log.scala src/Pure/Admin/build_polyml.scala src/Pure/Admin/build_release.scala src/Pure/Admin/build_spass.scala src/Pure/Admin/build_sqlite.scala src/Pure/Admin/build_status.scala src/Pure/Admin/build_vampire.scala src/Pure/Admin/build_verit.scala src/Pure/Admin/build_zipperposition.scala src/Pure/Admin/check_sources.scala src/Pure/Admin/ci_profile.scala src/Pure/Admin/components.scala src/Pure/Admin/isabelle_cronjob.scala src/Pure/Admin/isabelle_devel.scala src/Pure/Admin/jenkins.scala src/Pure/Admin/other_isabelle.scala src/Pure/Concurrent/consumer_thread.scala src/Pure/Concurrent/counter.scala src/Pure/Concurrent/delay.scala src/Pure/Concurrent/event_timer.scala src/Pure/Concurrent/future.scala src/Pure/Concurrent/isabelle_thread.scala src/Pure/Concurrent/mailbox.scala src/Pure/Concurrent/par_list.scala src/Pure/Concurrent/synchronized.scala src/Pure/GUI/color_value.scala src/Pure/GUI/desktop_app.scala src/Pure/GUI/gui.scala src/Pure/GUI/gui_thread.scala src/Pure/GUI/popup.scala src/Pure/GUI/wrap_panel.scala src/Pure/General/antiquote.scala src/Pure/General/bytes.scala src/Pure/General/cache.scala src/Pure/General/codepoint.scala src/Pure/General/comment.scala src/Pure/General/completion.scala src/Pure/General/csv.scala src/Pure/General/date.scala src/Pure/General/exn.scala src/Pure/General/file.scala src/Pure/General/file_watcher.scala src/Pure/General/graph.scala src/Pure/General/graph_display.scala src/Pure/General/graphics_file.scala src/Pure/General/http.scala src/Pure/General/json.scala src/Pure/General/linear_set.scala src/Pure/General/logger.scala src/Pure/General/long_name.scala src/Pure/General/mailman.scala src/Pure/General/mercurial.scala src/Pure/General/multi_map.scala src/Pure/General/output.scala src/Pure/General/path.scala src/Pure/General/position.scala src/Pure/General/pretty.scala src/Pure/General/properties.scala src/Pure/General/rdf.scala src/Pure/General/scan.scala src/Pure/General/sha1.scala src/Pure/General/sql.scala src/Pure/General/ssh.scala src/Pure/General/symbol.scala src/Pure/General/time.scala src/Pure/General/timing.scala src/Pure/General/untyped.scala src/Pure/General/url.scala src/Pure/General/utf8.scala src/Pure/General/uuid.scala src/Pure/General/value.scala src/Pure/General/word.scala src/Pure/General/xz.scala src/Pure/Isar/document_structure.scala src/Pure/Isar/keyword.scala src/Pure/Isar/line_structure.scala src/Pure/Isar/outer_syntax.scala src/Pure/Isar/parse.scala src/Pure/Isar/token.scala src/Pure/ML/ml_console.scala src/Pure/ML/ml_lex.scala src/Pure/ML/ml_process.scala src/Pure/ML/ml_statistics.scala src/Pure/ML/ml_syntax.scala src/Pure/PIDE/byte_message.scala src/Pure/PIDE/command.scala src/Pure/PIDE/command_span.scala src/Pure/PIDE/document.scala src/Pure/PIDE/document_id.scala src/Pure/PIDE/document_status.scala src/Pure/PIDE/editor.scala src/Pure/PIDE/headless.scala src/Pure/PIDE/line.scala src/Pure/PIDE/markup.scala src/Pure/PIDE/markup_tree.scala src/Pure/PIDE/protocol.scala src/Pure/PIDE/protocol_handlers.scala src/Pure/PIDE/protocol_message.scala src/Pure/PIDE/prover.scala src/Pure/PIDE/query_operation.scala src/Pure/PIDE/rendering.scala src/Pure/PIDE/resources.scala src/Pure/PIDE/session.scala src/Pure/PIDE/text.scala src/Pure/PIDE/xml.scala src/Pure/PIDE/yxml.scala src/Pure/ROOT.scala src/Pure/System/bash.scala src/Pure/System/command_line.scala src/Pure/System/cygwin.scala src/Pure/System/executable.scala src/Pure/System/getopts.scala src/Pure/System/isabelle_charset.scala src/Pure/System/isabelle_fonts.scala src/Pure/System/isabelle_platform.scala src/Pure/System/isabelle_process.scala src/Pure/System/isabelle_system.scala src/Pure/System/isabelle_tool.scala src/Pure/System/java_statistics.scala src/Pure/System/linux.scala src/Pure/System/mingw.scala src/Pure/System/numa.scala src/Pure/System/options.scala src/Pure/System/platform.scala src/Pure/System/posix_interrupt.scala src/Pure/System/process_result.scala src/Pure/System/progress.scala src/Pure/System/scala.scala src/Pure/System/system_channel.scala src/Pure/System/tty_loop.scala src/Pure/Thy/bibtex.scala src/Pure/Thy/export.scala src/Pure/Thy/export_theory.scala src/Pure/Thy/file_format.scala src/Pure/Thy/html.scala src/Pure/Thy/latex.scala src/Pure/Thy/presentation.scala src/Pure/Thy/sessions.scala src/Pure/Thy/thy_element.scala src/Pure/Thy/thy_header.scala src/Pure/Thy/thy_syntax.scala src/Pure/Tools/build.scala src/Pure/Tools/build_docker.scala src/Pure/Tools/build_job.scala src/Pure/Tools/check_keywords.scala src/Pure/Tools/debugger.scala src/Pure/Tools/doc.scala src/Pure/Tools/dump.scala src/Pure/Tools/fontforge.scala src/Pure/Tools/java_monitor.scala src/Pure/Tools/logo.scala src/Pure/Tools/main.scala src/Pure/Tools/mkroot.scala src/Pure/Tools/phabricator.scala src/Pure/Tools/print_operation.scala src/Pure/Tools/profiling_report.scala src/Pure/Tools/scala_project.scala src/Pure/Tools/server.scala src/Pure/Tools/server_commands.scala src/Pure/Tools/simplifier_trace.scala src/Pure/Tools/spell_checker.scala src/Pure/Tools/task_statistics.scala src/Pure/Tools/update.scala src/Pure/Tools/update_cartouches.scala src/Pure/Tools/update_comments.scala src/Pure/Tools/update_header.scala src/Pure/Tools/update_then.scala src/Pure/Tools/update_theorems.scala src/Pure/library.scala src/Pure/pure_thy.scala src/Pure/term.scala src/Pure/term_xml.scala src/Pure/thm_name.scala src/Tools/Graphview/graph_file.scala src/Tools/Graphview/graph_panel.scala src/Tools/Graphview/graphview.scala src/Tools/Graphview/layout.scala src/Tools/Graphview/main_panel.scala src/Tools/Graphview/metrics.scala src/Tools/Graphview/model.scala src/Tools/Graphview/mutator.scala src/Tools/Graphview/mutator_dialog.scala src/Tools/Graphview/mutator_event.scala src/Tools/Graphview/popups.scala src/Tools/Graphview/shapes.scala src/Tools/Graphview/tree_panel.scala src/Tools/VSCode/src/build_vscode.scala src/Tools/VSCode/src/channel.scala src/Tools/VSCode/src/dynamic_output.scala src/Tools/VSCode/src/language_server.scala src/Tools/VSCode/src/lsp.scala src/Tools/VSCode/src/preview_panel.scala src/Tools/VSCode/src/state_panel.scala src/Tools/VSCode/src/textmate_grammar.scala src/Tools/VSCode/src/vscode_model.scala src/Tools/VSCode/src/vscode_rendering.scala src/Tools/VSCode/src/vscode_resources.scala src/Tools/VSCode/src/vscode_spell_checker.scala ) ## diagnostics PRG="$(basename "$0")" function usage() { echo echo "Usage: isabelle $PRG [OPTIONS]" echo echo " Options are:" echo " -f fresh build" echo exit 1 } function fail() { echo "$1" >&2 exit 2 } [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment" ## process command line # options FRESH="" while getopts "f" OPT do case "$OPT" in f) FRESH=true ;; \?) usage ;; esac done shift $(($OPTIND - 1)) # args [ "$#" -ne 0 ] && usage ## target TARGET_DIR="lib/classes" TARGET_JAR="$TARGET_DIR/Pure.jar" TARGET_SHASUM="$TARGET_DIR/Pure.shasum" function target_shasum() { shasum -a1 -b "$TARGET_JAR" "${SOURCES[@]}" 2>/dev/null } function target_clean() { rm -rf "$TARGET_DIR" } [ -n "$FRESH" ] && target_clean ## build target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null if [ "$?" -ne 0 ]; then echo "### Building Isabelle/Scala ..." target_clean BUILD_DIR="$TARGET_DIR/build" mkdir -p "$BUILD_DIR" ( export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")" isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS \ -d "$BUILD_DIR" "${SOURCES[@]}" ) || fail "Failed to compile sources" CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider" mkdir -p "$BUILD_DIR/$(dirname "$CHARSET_SERVICE")" echo isabelle.Isabelle_Charset_Provider > "$BUILD_DIR/$CHARSET_SERVICE" cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" "$BUILD_DIR/isabelle/." cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" "$BUILD_DIR/isabelle/." isabelle_jdk jar -c -f "$(platform_path "$TARGET_JAR")" -e isabelle.Main \ -C "$BUILD_DIR" META-INF \ -C "$BUILD_DIR" isabelle || fail "Failed to produce $TARGET_JAR" rm -rf "$BUILD_DIR" target_shasum > "$TARGET_SHASUM" fi