--- 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
}
--- 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
--- 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(" <options> 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<system> - specified system to use\n");
print(" -t<timelimit> - CPU time limit for system\n");
print(" -c<command> - 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);
}
--- 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---") *}
--- 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;
--- 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
--- 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 ****)
--- 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
--- 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
--- 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)"
--- 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
}
--- /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)
+ }
+ }
+}
+
--- 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))
}
--- /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
+ }
+ }
+ }
+}
+