# HG changeset patch # User haftmann # Date 1246280108 -7200 # Node ID 50b307148dab4a33d33fd73624842eb39854b9e8 # Parent cc7ddda02436d5126d5df69830aa4efb55c497cc# Parent f079b174e56a0d8b537510cbd1745c57759adb64 merged diff -r f079b174e56a -r 50b307148dab Admin/build --- a/Admin/build Mon Jun 29 12:18:58 2009 +0200 +++ b/Admin/build Mon Jun 29 14:55:08 2009 +0200 @@ -8,6 +8,9 @@ PATH="/usr/local/dist/DIR/j2sdk1.5.0/bin:$PATH" PATH="/home/scala/current/bin:$PATH" +if [ -z "$SCALA_HOME" ]; then + export SCALA_HOME="$(dirname "$(dirname "$(type -p scalac)")")" +fi ## directory layout @@ -32,7 +35,7 @@ all all modules below browser graph browser (requires jdk) doc documentation (requires latex and rail) - jars JVM components (requires jdk and scala) + jars Scala/JVM components (requires scala) EOF exit 1 @@ -93,13 +96,13 @@ function build_jars () { echo "###" - echo "### Building JVM components ..." + echo "### Building Scala/JVM components ..." echo "###" - type -p scalac >/dev/null || fail "Scala compiler unavailable" + [ -z "$SCALA_HOME" ] && fail "Scala unavailable: unknown SCALA_HOME" pushd "$ISABELLE_HOME/src/Pure" >/dev/null - "$ISABELLE_TOOL" make jar || fail "Failed to build Pure.jar!" + "$ISABELLE_TOOL" make jars || fail "Failed to build isabelle-scala.jar" popd >/dev/null } diff -r f079b174e56a -r 50b307148dab Admin/makedist --- a/Admin/makedist Mon Jun 29 12:18:58 2009 +0200 +++ b/Admin/makedist Mon Jun 29 14:55:08 2009 +0200 @@ -116,7 +116,6 @@ DISTBASE="$DISTPREFIX/dist-$DISTNAME" mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; } [ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; } -[ -e "$DISTBASE/pdf/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/pdf/$DISTNAME already exists!"; } cd "$DISTBASE" mv "$DISTPREFIX/$TMP/isabelle-$IDENT" "$DISTNAME" @@ -141,7 +140,7 @@ MOVE=$(find doc-src \( -type f -a -not -type l -a -not -name isabelle_isar.pdf -a -not -name pghead.pdf -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf') mv -f $MOVE doc rm doc/Isa-logics.eps -rm doc/adaption.dvi doc/adaption.pdf doc/architecture.dvi doc/architecture.pdf +rm doc/adaptation.dvi doc/adaptation.pdf doc/architecture.dvi doc/architecture.pdf rm -rf doc-src mkdir -p contrib @@ -189,18 +188,9 @@ chmod -R g=o "$DISTNAME" chgrp -R isabelle "$DISTNAME" Isabelle -mkdir -p "pdf/$DISTNAME/doc" -mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc" - echo "$DISTNAME.tar.gz" tar -czf "$DISTNAME.tar.gz" Isabelle "$DISTNAME" -echo "${DISTNAME}_pdf.tar.gz" -tar -C pdf -czf "${DISTNAME}_pdf.tar.gz" "$DISTNAME" - -mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc" -rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf - # cleanup dist diff -r f079b174e56a -r 50b307148dab lib/scripts/SystemOnTPTP --- a/lib/scripts/SystemOnTPTP Mon Jun 29 12:18:58 2009 +0200 +++ b/lib/scripts/SystemOnTPTP Mon Jun 29 14:55:08 2009 +0200 @@ -10,20 +10,20 @@ use HTTP::Request::Common; use LWP; -my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply"; +my $SystemOnTPTPFormReplyURL = + "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply"; # default parameters my %URLParameters = ( "NoHTML" => 1, "QuietFlag" => "-q01", - "X2TPTP" => "-S", "SubmitButton" => "RunSelectedSystems", "ProblemSource" => "UPLOAD", ); #----Get format and transform options if specified my %Options; -getopts("hws:t:c:",\%Options); +getopts("hwxs:t:c:",\%Options); #----Usage sub usage() { @@ -31,6 +31,7 @@ print(" are ...\n"); print(" -h - print this help\n"); print(" -w - list available ATP systems\n"); + print(" -x - use X2TPTP to convert output of prover\n"); print(" -s - specified system to use\n"); print(" -t - CPU time limit for system\n"); print(" -c - custom command for system\n"); @@ -40,11 +41,18 @@ if (exists($Options{'h'})) { usage(); } + #----What systems flag if (exists($Options{'w'})) { $URLParameters{"SubmitButton"} = "ListSystems"; delete($URLParameters{"ProblemSource"}); } + +#----X2TPTP +if (exists($Options{'x'})) { + $URLParameters{"X2TPTP"} = "-S"; +} + #----Selected system my $System; if (exists($Options{'s'})) { @@ -86,7 +94,7 @@ my $Response = $Agent->request($Request); #catch errors / failure -if(! $Response->is_success){ +if(!$Response->is_success) { print "HTTP-Error: " . $Response->message . "\n"; exit(-1); } elsif (exists($Options{'w'})) { @@ -95,7 +103,12 @@ } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) { print "Specified System $1 does not exist\n"; exit(-1); -} elsif ($Response->content =~ /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/) { +} elsif (exists($Options{'x'}) && + $Response->content =~ + /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ && + $Response->content !~ /ERROR: Could not form TPTP format derivation/ ) +{ + # converted output: extract proof my @lines = split( /\n/, $Response->content); my $extract = ""; foreach my $line (@lines){ @@ -108,12 +121,20 @@ $extract =~ s/\s//g; $extract =~ s/\)\.cnf/\)\.\ncnf/g; + print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n"; # orientation for res_reconstruct.ML print "# SZS output start CNFRefutation.\n"; print "$extract\n"; print "# SZS output end CNFRefutation.\n"; + # can be useful for debugging; Isabelle ignores this + print "============== original response from SystemOnTPTP: ==============\n"; + print $Response->content; exit(0); -} else { +} elsif (!exists($Options{'x'})) { + # pass output directly to Isabelle + print $Response->content; + exit(0); +}else { print "Remote-script could not extract proof:\n".$Response->content; exit(-1); } diff -r f079b174e56a -r 50b307148dab src/HOL/ATP_Linkup.thy --- a/src/HOL/ATP_Linkup.thy Mon Jun 29 12:18:58 2009 +0200 +++ b/src/HOL/ATP_Linkup.thy Mon Jun 29 14:55:08 2009 +0200 @@ -115,11 +115,11 @@ text {* remote provers via SystemOnTPTP *} setup {* AtpManager.add_prover "remote_vampire" - (AtpWrapper.remote_prover "-s Vampire---9.0") *} + (AtpWrapper.remote_prover_opts 60 false "" "Vampire---9") *} setup {* AtpManager.add_prover "remote_spass" - (AtpWrapper.remote_prover "-s SPASS---3.01") *} + (AtpWrapper.remote_prover_opts 40 true "-x" "SPASS---") *} setup {* AtpManager.add_prover "remote_e" - (AtpWrapper.remote_prover "-s EP---1.0") *} + (AtpWrapper.remote_prover_opts 100 false "" "EP---") *} diff -r f079b174e56a -r 50b307148dab src/HOL/Tools/atp_wrapper.ML --- a/src/HOL/Tools/atp_wrapper.ML Mon Jun 29 12:18:58 2009 +0200 +++ b/src/HOL/Tools/atp_wrapper.ML Mon Jun 29 14:55:08 2009 +0200 @@ -23,8 +23,9 @@ val eprover_full: AtpManager.prover val spass_opts: int -> bool -> AtpManager.prover val spass: AtpManager.prover - val remote_prover_opts: int -> bool -> string -> AtpManager.prover - val remote_prover: string -> AtpManager.prover + val remote_prover_opts: int -> bool -> string -> string -> AtpManager.prover + val remote_prover: string -> string -> AtpManager.prover + val refresh_systems: unit -> unit end; structure AtpWrapper: ATP_WRAPPER = @@ -74,20 +75,16 @@ (* write out problem file and call prover *) val probfile = prob_pathname subgoalno - val fname = File.platform_path probfile - val _ = writer fname clauses - val cmdline = - if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args - else error ("Bad executable: " ^ Path.implode cmd) - val (proof, rc) = system_out (cmdline ^ " " ^ fname) + val conj_pos = writer probfile clauses + val (proof, rc) = system_out ( + if File.exists cmd then + space_implode " " ["exec", File.shell_path cmd, args, File.platform_path probfile] + else error ("Bad executable: " ^ Path.implode cmd)) (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *) val _ = - if destdir' = "" then OS.FileSys.remove fname - else - let val out = TextIO.openOut (fname ^ "_proof") - val _ = TextIO.output (out, proof) - in TextIO.closeOut out end + if destdir' = "" then File.rm probfile + else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof (* check for success and print out some information on failure *) val failure = find_failure proof @@ -95,7 +92,8 @@ val message = if is_some failure then "External prover failed." else if rc <> 0 then "External prover failed: " ^ proof - else "Try this command: " ^ produce_answer name (proof, thm_names, ctxt, th, subgoalno) + else "Try this command: " ^ + produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno) val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof) in (success, message, proof, thm_names, the_filtered_clauses) end; @@ -112,7 +110,7 @@ (ResHolClause.tptp_write_file (AtpManager.get_full_types())) command ResReconstruct.find_failure - (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp) + (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list false) timeout ax_clauses fcls name n goal; (*arbitrary ATP with TPTP input/output and problemfile as last argument*) @@ -146,7 +144,7 @@ ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout)) timeout; -val vampire_full = vampire_opts 60 false; +val vampire_full = vampire_opts_full 60 false; (* E prover *) @@ -177,7 +175,7 @@ (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout) ResReconstruct.find_failure - ResReconstruct.lemma_list_dfg + (ResReconstruct.lemma_list true) timeout ax_clauses fcls name n goal; val spass = spass_opts 40 true; @@ -185,10 +183,32 @@ (* remote prover invocation via SystemOnTPTP *) -fun remote_prover_opts max_new theory_const args timeout = - tptp_prover_opts max_new theory_const - (Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP", args ^ " -t " ^ string_of_int timeout) - timeout; +val systems = + Synchronized.var "atp_wrapper_systems" ([]: string list); + +fun get_systems () = + let + val (answer, rc) = system_out (("$ISABELLE_HOME/lib/scripts/SystemOnTPTP" |> + Path.explode |> File.shell_path) ^ " -w") + in + if rc <> 0 then error ("Get available systems from SystemOnTPTP:\n" ^ answer) + else split_lines answer + end; + +fun refresh_systems () = Synchronized.change systems (fn _ => + get_systems()); + +fun get_system prefix = Synchronized.change_result systems (fn systems => + let val systems = if null systems then get_systems() else systems + in (find_first (String.isPrefix prefix) systems, systems) end); + +fun remote_prover_opts max_new theory_const args prover_prefix timeout = + let val sys = case get_system prover_prefix of + NONE => error ("No system like " ^ quote prover_prefix ^ " at SystemOnTPTP") + | SOME sys => sys + in tptp_prover_opts max_new theory_const + (Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP", + args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout end; val remote_prover = remote_prover_opts 60 false; diff -r f079b174e56a -r 50b307148dab src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Mon Jun 29 12:18:58 2009 +0200 +++ b/src/HOL/Tools/res_atp.ML Mon Jun 29 14:55:08 2009 +0200 @@ -296,7 +296,11 @@ (*The rule subsetI is frequently omitted by the relevance filter. This could be theory data or identified with ATPset (which however is too big currently)*) -val whitelist = [subsetI]; +val whitelist_fo = [subsetI]; +(* ext has been a 'helper clause', always given to the atps. + As such it was not passed to metis, but metis does not include ext (in contrast + to the other helper_clauses *) +val whitelist_ho = [ResHolClause.ext]; (*** retrieve lemmas from clasimpset and atpset, may filter them ***) @@ -531,10 +535,12 @@ create additional clauses based on the information from extra_cls *) fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy = let - val white_thms = - filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths)) + val isFO = isFO thy goal_cls + val white_thms = filter check_named (map ResAxioms.pairname + (whitelist_fo @ (if isFO then [] else whitelist_ho) @ chain_ths)) val white_cls = ResAxioms.cnf_rules_pairs thy white_thms val extra_cls = white_cls @ extra_cls + val axcls = white_cls @ axcls val ccls = subtract_cls goal_cls extra_cls val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls val ccltms = map prop_of ccls @@ -545,7 +551,7 @@ (*TFrees in conjecture clauses; TVars in axiom clauses*) val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls) - val helper_clauses = ResHolClause.get_helper_clauses dfg thy (isFO thy goal_cls) (conjectures, extra_cls, []) + val helper_clauses = ResHolClause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, []) val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' in diff -r f079b174e56a -r 50b307148dab src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Mon Jun 29 12:18:58 2009 +0200 +++ b/src/HOL/Tools/res_clause.ML Mon Jun 29 14:55:08 2009 +0200 @@ -57,7 +57,6 @@ val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table val add_arityClause_funcs: arityClause * int Symtab.table -> int Symtab.table val init_functab: int Symtab.table - val writeln_strs: TextIO.outstream -> string list -> unit val dfg_sign: bool -> string -> string val dfg_of_typeLit: bool -> type_literal -> string val gen_dfg_cls: int * string * kind * string list * string list * string list -> string @@ -441,8 +440,6 @@ fun string_of_type_clsname (cls_id,ax_name,idx) = string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx); -fun writeln_strs os = List.app (fn s => TextIO.output (os, s)); - (**** Producing DFG files ****) diff -r f079b174e56a -r 50b307148dab src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Mon Jun 29 12:18:58 2009 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Mon Jun 29 14:55:08 2009 +0200 @@ -26,19 +26,21 @@ val strip_comb: combterm -> combterm * combterm list val literals_of_term: theory -> term -> literal list * typ list exception TOO_TRIVIAL - val make_conjecture_clauses: bool -> theory -> thm list -> clause list (* dfg thy ccls *) + val make_conjecture_clauses: bool -> theory -> thm list -> clause list val make_axiom_clauses: bool -> theory -> - (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list (* dfg thy axcls *) + (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list val get_helper_clauses: bool -> theory -> bool -> clause list * (thm * (axiom_name * clause_id)) list * string list -> clause list - val tptp_write_file: bool -> string -> - clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit - val dfg_write_file: bool -> string -> - clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit + val tptp_write_file: bool -> Path.T -> + clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> + int * int + val dfg_write_file: bool -> Path.T -> + clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> + int * int end structure ResHolClause: RES_HOL_CLAUSE = @@ -423,7 +425,7 @@ val S = if needed "c_COMBS" then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms thy [comb_S]) else [] - val other = cnf_helper_thms thy [ext,fequal_imp_equal,equal_imp_fequal] + val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal] in map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S)) end; @@ -469,59 +471,60 @@ (* tptp format *) -fun tptp_write_file t_full filename clauses = +fun tptp_write_file t_full file clauses = let val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses val (cma, cnh) = count_constants clauses val params = (t_full, cma, cnh) val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures) val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss) - val out = TextIO.openOut filename - in - List.app (curry TextIO.output out o #1 o (clause2tptp params)) axclauses; - RC.writeln_strs out tfree_clss; - RC.writeln_strs out tptp_clss; - List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses; - List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses; - List.app (curry TextIO.output out o #1 o (clause2tptp params)) helper_clauses; - TextIO.closeOut out + val _ = + File.write_list file ( + map (#1 o (clause2tptp params)) axclauses @ + tfree_clss @ + tptp_clss @ + map RC.tptp_classrelClause classrel_clauses @ + map RC.tptp_arity_clause arity_clauses @ + map (#1 o (clause2tptp params)) helper_clauses) + in (length axclauses + 1, length tfree_clss + length tptp_clss) end; (* dfg format *) -fun dfg_write_file t_full filename clauses = +fun dfg_write_file t_full file clauses = let val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses val (cma, cnh) = count_constants clauses val params = (t_full, cma, cnh) val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures) - and probname = Path.implode (Path.base (Path.explode filename)) + and probname = Path.implode (Path.base file) val axstrs = map (#1 o (clause2dfg params)) axclauses val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss) - val out = TextIO.openOut filename val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses - in - TextIO.output (out, RC.string_of_start probname); - TextIO.output (out, RC.string_of_descrip probname); - TextIO.output (out, RC.string_of_symbols - (RC.string_of_funcs funcs) - (RC.string_of_preds (cl_preds @ ty_preds))); - TextIO.output (out, "list_of_clauses(axioms,cnf).\n"); - RC.writeln_strs out axstrs; - List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses; - List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses; - RC.writeln_strs out helper_clauses_strs; - TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"); - RC.writeln_strs out tfree_clss; - RC.writeln_strs out dfg_clss; - TextIO.output (out, "end_of_list.\n\n"); - (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*) - TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n"); - TextIO.output (out, "end_problem.\n"); - TextIO.closeOut out + val _ = + File.write_list file ( + RC.string_of_start probname :: + RC.string_of_descrip probname :: + RC.string_of_symbols (RC.string_of_funcs funcs) + (RC.string_of_preds (cl_preds @ ty_preds)) :: + "list_of_clauses(axioms,cnf).\n" :: + axstrs @ + map RC.dfg_classrelClause classrel_clauses @ + map RC.dfg_arity_clause arity_clauses @ + helper_clauses_strs @ + ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @ + tfree_clss @ + dfg_clss @ + ["end_of_list.\n\n", + (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*) + "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n", + "end_problem.\n"]) + + in (length axclauses + length classrel_clauses + length arity_clauses + + length helper_clauses + 1, length tfree_clss + length dfg_clss) end; end diff -r f079b174e56a -r 50b307148dab src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Mon Jun 29 12:18:58 2009 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Mon Jun 29 14:55:08 2009 +0200 @@ -16,10 +16,11 @@ val setup: Context.theory -> Context.theory (* extracting lemma list*) val find_failure: string -> string option - val lemma_list_dfg: string -> string * string vector * Proof.context * Thm.thm * int -> string - val lemma_list_tstp: string -> string * string vector * Proof.context * Thm.thm * int -> string + val lemma_list: bool -> string -> + string * string vector * (int * int) * Proof.context * Thm.thm * int -> string (* structured proofs *) - val structured_proof: string -> string * string vector * Proof.context * Thm.thm * int -> string + val structured_proof: string -> + string * string vector * (int * int) * Proof.context * Thm.thm * int -> string end; structure ResReconstruct : RES_RECONSTRUCT = @@ -496,17 +497,17 @@ (* === EXTRACTING LEMMAS === *) (* lines have the form "cnf(108, axiom, ...", the number (108) has to be extracted)*) - fun get_step_nums_tstp proofextract = + fun get_step_nums false proofextract = let val toks = String.tokens (not o Char.isAlphaNum) fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok + | inputno ("cnf"::ntok::"negated"::"conjecture"::_) = Int.fromString ntok | inputno _ = NONE val lines = split_lines proofextract in List.mapPartial (inputno o toks) lines end - - (*String contains multiple lines. We want those of the form + (*String contains multiple lines. We want those of the form "253[0:Inp] et cetera..." A list consisting of the first number in each line is returned. *) - fun get_step_nums_dfg proofextract = + | get_step_nums true proofextract = let val toks = String.tokens (not o Char.isAlphaNum) fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok | inputno _ = NONE @@ -514,15 +515,19 @@ in List.mapPartial (inputno o toks) lines end (*extracting lemmas from tstp-output between the lines from above*) - fun extract_lemmas get_step_nums (proof, thm_names, _, _, _) = + fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) = let (* get the names of axioms from their numbers*) fun get_axiom_names thm_names step_nums = let - fun is_axiom n = n <= Vector.length thm_names + val last_axiom = Vector.length thm_names + fun is_axiom n = n <= last_axiom + fun is_conj n = n >= #1 conj_count andalso n < #1 conj_count + #2 conj_count fun getname i = Vector.sub(thm_names, i-1) in - sort_distinct string_ord (filter (fn x => x <> "??.unknown") (map getname (filter is_axiom step_nums))) + (sort_distinct string_ord (filter (fn x => x <> "??.unknown") + (map getname (filter is_axiom step_nums))), + exists is_conj step_nums) end val proofextract = get_proof_extract proof in @@ -545,22 +550,23 @@ fun sendback_metis_nochained lemmas = (Markup.markup Markup.sendback o metis_line) (nochained lemmas) - fun lemma_list_tstp name result = - let val lemmas = extract_lemmas get_step_nums_tstp result - in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas end; - fun lemma_list_dfg name result = - let val lemmas = extract_lemmas get_step_nums_dfg result - in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas end; + + fun lemma_list dfg name result = + let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result + in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^ + (if used_conj then "" + else "\nWarning: Goal is provable because context is inconsistent.") + end; (* === Extracting structured Isar-proof === *) - fun structured_proof name (result as (proof, thm_names, ctxt, goal, subgoalno)) = + fun structured_proof name (result as (proof, thm_names, conj_count, ctxt, goal, subgoalno)) = let (*Could use split_lines, but it can return blank lines...*) val lines = String.tokens (equal #"\n"); val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c) val proofextract = get_proof_extract proof val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract)) - val one_line_proof = lemma_list_tstp name result + val one_line_proof = lemma_list false name result val structured = if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then "" else decode_tstp_file cnfs ctxt goal subgoalno thm_names in diff -r f079b174e56a -r 50b307148dab src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Mon Jun 29 12:18:58 2009 +0200 +++ b/src/Pure/IsaMakefile Mon Jun 29 14:55:08 2009 +0200 @@ -121,23 +121,29 @@ General/position.scala General/scan.scala General/swing.scala \ General/symbol.scala General/xml.scala General/yxml.scala \ Isar/isar.scala Isar/isar_document.scala Isar/outer_keyword.scala \ - System/cygwin.scala System/isabelle_process.scala \ - System/isabelle_system.scala Thy/completion.scala \ - Thy/thy_header.scala Tools/isabelle_syntax.scala + System/cygwin.scala System/gui_setup.scala \ + System/isabelle_process.scala System/isabelle_system.scala \ + System/platform.scala Thy/completion.scala Thy/thy_header.scala \ + Tools/isabelle_syntax.scala -SCALA_TARGET = $(ISABELLE_HOME)/lib/classes/Pure.jar +JAR_DIR = $(ISABELLE_HOME)/lib/classes +PURE_JAR = $(JAR_DIR)/Pure.jar +FULL_JAR = $(JAR_DIR)/isabelle-scala.jar -jar: $(SCALA_TARGET) +jars: $(FULL_JAR) -$(SCALA_TARGET): $(SCALA_FILES) +$(FULL_JAR): $(SCALA_FILES) @rm -rf classes && mkdir classes - scalac -deprecation -d classes -target jvm-1.5 $(SCALA_FILES) - scaladoc -d classes $(SCALA_FILES) + "$(SCALA_HOME)/bin/scalac" -deprecation -d classes -target jvm-1.5 $(SCALA_FILES) + "$(SCALA_HOME)/bin/scaladoc" -d classes $(SCALA_FILES) @cp $(SCALA_FILES) classes/isabelle - @mkdir -p `dirname $@` - @cd classes; jar cf `jvmpath $@` isabelle + @mkdir -p "$(JAR_DIR)" + @cd classes; jar cfe `jvmpath "$(PURE_JAR)"` isabelle.GUI_Setup isabelle + @cd classes; cp "$(SCALA_HOME)/lib/scala-swing.jar" .; jar xf scala-swing.jar; \ + cp "$(SCALA_HOME)/lib/scala-library.jar" "$(FULL_JAR)"; \ + jar ufe `jvmpath $(FULL_JAR)` isabelle.GUI_Setup isabelle scala @rm -rf classes -clean-jar: - @rm -f $(SCALA_TARGET) +clean-jars: + @rm -f "$(PURE_JAR)" "$(FULL_JAR)" diff -r f079b174e56a -r 50b307148dab src/Pure/System/cygwin.scala --- a/src/Pure/System/cygwin.scala Mon Jun 29 12:18:58 2009 +0200 +++ b/src/Pure/System/cygwin.scala Mon Jun 29 14:55:08 2009 +0200 @@ -7,6 +7,7 @@ package isabelle import java.lang.reflect.Method +import java.io.File object Cygwin @@ -75,10 +76,31 @@ /* Cygwin installation */ + // old-style mount points (Cygwin 1.5) private val CYGWIN_MOUNTS = "Software\\Cygnus Solutions\\Cygwin\\mounts v2" - def cygdrive(): Option[String] = query_registry(CYGWIN_MOUNTS, "cygdrive prefix") - def root(): Option[String] = query_registry(CYGWIN_MOUNTS + "\\/", "native") + // new-style setup (Cygwin 1.7) + private val CYGWIN_SETUP1 = "Software\\Cygwin\\setup" + private val CYGWIN_SETUP2 = "Software\\Wow6432Node\\Cygwin\\setup" // !? + def config(): (String, String) = + { + query_registry(CYGWIN_SETUP1, "rootdir") match { + case Some(root) => (root, "/cygdrive") + case None => + val root = + query_registry(CYGWIN_MOUNTS + "\\/", "native") getOrElse "C:\\cygwin" + val cygdrive = + query_registry(CYGWIN_MOUNTS, "cygdrive prefix") getOrElse "cygdrive" + (root, cygdrive) + } + } + + + /* basic sanity check */ + + def check(root: String): Boolean = + new File(root + "\\bin\\bash.exe").isFile && + new File(root + "\\bin\\env.exe").isFile } diff -r f079b174e56a -r 50b307148dab src/Pure/System/gui_setup.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/gui_setup.scala Mon Jun 29 14:55:08 2009 +0200 @@ -0,0 +1,64 @@ +/* Title: Pure/System/gui_setup.scala + Author: Makarius + +GUI for basic system setup. +*/ + +package isabelle + +import javax.swing.UIManager + +import scala.swing._ +import scala.swing.event._ + + +object GUI_Setup extends GUIApplication +{ + def main(args: Array[String]) = + { + Swing.later { + UIManager.setLookAndFeel(Platform.look_and_feel) + top.pack() + top.visible = true + } + } + + def top = new MainFrame { + title = "Isabelle setup" + + // components + val text = new TextArea { + editable = false + columns = 40 + rows = 15 + xLayoutAlignment = 0.5 + } + val ok = new Button { + text = "OK" + xLayoutAlignment = 0.5 + } + contents = new BoxPanel(Orientation.Vertical) { + contents += text + contents += ok + } + + // values + if (Platform.is_windows) { + text.append("Cygwin root: " + Cygwin.config()._1 + "\n") + } + Platform.defaults match { + case None => + case Some((name, None)) => text.append("Platform: " + name + "\n") + case Some((name1, Some(name2))) => + text.append("Main platform: " + name1 + "\n") + text.append("Alternative platform: " + name2 + "\n") + } + + // reactions + listenTo(ok) + reactions += { + case ButtonClicked(`ok`) => System.exit(0) + } + } +} + diff -r f079b174e56a -r 50b307148dab src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon Jun 29 12:18:58 2009 +0200 +++ b/src/Pure/System/isabelle_system.scala Mon Jun 29 14:55:08 2009 +0200 @@ -19,42 +19,6 @@ val charset = "UTF-8" - /* platform identification */ - - val is_cygwin = System.getProperty("os.name").startsWith("Windows") - - private val X86 = new Regex("i.86|x86") - private val X86_64 = new Regex("amd64|x86_64") - private val Sparc = new Regex("sparc") - private val PPC = new Regex("PowerPC|ppc") - - private val Solaris = new Regex("SunOS|Solaris") - private val Linux = new Regex("Linux") - private val Darwin = new Regex("Mac OS X") - private val Cygwin = new Regex("Windows.*") - - val default_platform: Option[String] = - { - val name = - java.lang.System.getProperty("os.name") match { - case Solaris() => "solaris" - case Linux() => "linux" - case Darwin() => "darwin" - case Cygwin() => "cygwin" - case _ => "" - } - val arch = - java.lang.System.getProperty("os.arch") match { - case X86() | X86_64() => "x86" - case Sparc() => "sparc" - case PPC() => "ppc" - case _ => "" - } - if (arch == "" || name == "") None - else Some(arch + "-" + name) - } - - /* shell processes */ private def raw_execute(env: Map[String, String], redirect: Boolean, args: String*): Process = @@ -98,9 +62,9 @@ private val (platform_root, drive_prefix, shell_prefix) = { - if (Isabelle_System.is_cygwin) { - val root = Cygwin.root() getOrElse "C:\\cygwin" - val drive = Cygwin.cygdrive() getOrElse "/cygdrive" + if (Platform.is_windows) { + val (root, drive) = Cygwin.config() + if (!Cygwin.check(root)) error("Bad Cygwin installation: " + root) val shell = List(root + "\\bin\\bash", "-l") (root, drive, shell) } @@ -220,7 +184,7 @@ val result_path = new StringBuilder val rest = expand_path(isabelle_path) match { - case Cygdrive(drive, rest) if Isabelle_System.is_cygwin => + case Cygdrive(drive, rest) if Platform.is_windows => result_path ++= (drive + ":" + File.separator) rest case path if path.startsWith("/") => @@ -248,7 +212,7 @@ def isabelle_path(platform_path: String): String = { - if (Isabelle_System.is_cygwin) { + if (Platform.is_windows) { platform_path.replace('/', '\\') match { case Platform_Root(rest) => "/" + rest.replace('\\', '/') case Drive(letter, rest) => @@ -286,7 +250,7 @@ def execute(redirect: Boolean, args: String*): Process = { val cmdline = - if (Isabelle_System.is_cygwin) List(platform_path("/bin/env")) ++ args + if (Platform.is_windows) List(platform_path("/bin/env")) ++ args else args Isabelle_System.raw_execute(environment, redirect, cmdline: _*) } @@ -325,7 +289,7 @@ { // blocks until writer is ready val stream = - if (Isabelle_System.is_cygwin) execute(false, "cat", fifo).getInputStream + if (Platform.is_windows) execute(false, "cat", fifo).getInputStream else new FileInputStream(fifo) new BufferedReader(new InputStreamReader(stream, Isabelle_System.charset)) } diff -r f079b174e56a -r 50b307148dab src/Pure/System/platform.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/platform.scala Mon Jun 29 14:55:08 2009 +0200 @@ -0,0 +1,69 @@ +/* Title: Pure/System/platform.scala + Author: Makarius + +Raw platform identification. +*/ + +package isabelle + +import javax.swing.UIManager + +import scala.util.matching.Regex + + +object Platform +{ + /* main OS variants */ + + val is_macos = System.getProperty("os.name") == "Mac OS X" + val is_windows = System.getProperty("os.name").startsWith("Windows") + + + /* Isabelle platform identifiers */ + + private val Solaris = new Regex("SunOS|Solaris") + private val Linux = new Regex("Linux") + private val Darwin = new Regex("Mac OS X") + private val Cygwin = new Regex("Windows.*") + + private val X86 = new Regex("i.86|x86") + private val X86_64 = new Regex("amd64|x86_64") + private val Sparc = new Regex("sparc") + private val PPC = new Regex("PowerPC|ppc") + + // main default, optional 64bit variant + val defaults: Option[(String, Option[String])] = + { + (java.lang.System.getProperty("os.name") match { + case Solaris() => Some("solaris") + case Linux() => Some("linux") + case Darwin() => Some("darwin") + case Cygwin() => Some("cygwin") + case _ => None + }) match { + case Some(name) => + java.lang.System.getProperty("os.arch") match { + case X86() => Some(("x86-" + name, None)) + case X86_64() => Some(("x86-" + name, if (is_windows) None else Some("x86_64-" + name))) + case Sparc() => Some(("sparc-" + name, None)) + case PPC() => Some(("ppc-" + name, None)) + } + case None => None + } + } + + + /* Swing look-and-feel */ + + def look_and_feel(): String = + { + if (is_windows || is_macos) UIManager.getSystemLookAndFeelClassName() + else { + UIManager.getInstalledLookAndFeels().find(laf => laf.getName == "Nimbus") match { + case None => UIManager.getCrossPlatformLookAndFeelClassName() + case Some(laf) => laf.getClassName + } + } + } +} +