# HG changeset patch # User quigley # Date 1114005797 -7200 # Node ID aed221aff64299e14c1a3817f9b9662a5ed4ee77 # Parent 98af3693f6b36f199807850a237f6e03c3b1e91a Removed remaining references to Main.thy in reconstruction code. diff -r 98af3693f6b3 -r aed221aff642 bin/isabelle-process --- a/bin/isabelle-process Wed Apr 20 14:18:33 2005 +0200 +++ b/bin/isabelle-process Wed Apr 20 16:03:17 2005 +0200 @@ -1,7 +1,10 @@ #!/usr/bin/env bash # + # $Id$ + # Author: Markus Wenzel, TU Muenchen +# License: GPL (GNU GENERAL PUBLIC LICENSE) # # Isabelle process startup script. @@ -30,7 +33,6 @@ echo " -C tell ML system to copy output image" echo " -I startup Isar interaction mode" echo " -P startup Proof General interaction mode" - echo " -X startup PGIP interaction mode" echo " -c tell ML system to compress output image" echo " -e MLTEXT pass MLTEXT to the ML session" echo " -f pass 'Session.finish();' to the ML session" @@ -69,7 +71,7 @@ READONLY="" NOWRITE="" -while getopts "XCIPce:fm:qruw" OPT +while getopts "CIPce:fm:qruw" OPT do case "$OPT" in C) @@ -81,9 +83,6 @@ P) PROOFGENERAL=true ;; - X) - PGIP=true - ;; c) COMPRESS=true ;; @@ -209,9 +208,7 @@ [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT" -if [ -n "$PGIP" ]; then - MLTEXT="$MLTEXT; ProofGeneral.init_pgip $ISAR;" -elif [ -n "$PROOFGENERAL" ]; then +if [ -n "$PROOFGENERAL" ]; then MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;" elif [ "$ISAR" = true ]; then MLTEXT="$MLTEXT; Isar.main();" diff -r 98af3693f6b3 -r aed221aff642 build --- a/build Wed Apr 20 14:18:33 2005 +0200 +++ b/build Wed Apr 20 16:03:17 2005 +0200 @@ -112,6 +112,8 @@ echo " ML_HOME=$ML_HOME" echo " ML_OPTIONS=$ML_OPTIONS" echo " ML_PLATFORM=$ML_PLATFORM" + echo " ISABELLE_INTERFACE=$ISABELLE_INTERFACE" + echo "ISABELLE_OUTPUT=$ISABELLE_OUTPUT" echo echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS" fi @@ -154,6 +156,7 @@ echo "ML_HOME=$ML_HOME" echo "ML_OPTIONS=$ML_OPTIONS" echo "ML_PLATFORM=$ML_PLATFORM" + echo "ISABELLE_OUTPUT=$ISABELLE_OUTPUT" echo echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS" echo diff -r 98af3693f6b3 -r aed221aff642 etc/settings --- a/etc/settings Wed Apr 20 14:18:33 2005 +0200 +++ b/etc/settings Wed Apr 20 16:03:17 2005 +0200 @@ -120,14 +120,14 @@ ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" # Heap output location. ML system identifier is appended automatically later on. -if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then - #Isabelle build tells us to store heaps etc. within the distribution. - ISABELLE_OUTPUT="$ISABELLE_HOME/heaps" - ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info" -else +#if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then +# Isabelle build tells us to store heaps etc. within the distribution. + # ISABELLE_OUTPUT="$ISABELLE_HOME/heaps" + # ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info" +#else ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" -fi +#fi # Site settings check -- just to make it a little bit harder to copy this file! [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ @@ -181,7 +181,8 @@ ISAMODE_OPTIONS="" # Proof General path, look in a variety of places -ISABELLE_INTERFACE=$(choosefrom \ +ISABELLE_INTERFACE=$(choosefrom\ + "/homes/clq20/IsabelleCVS/isabelle/ProofGeneral/isar/interface"\ "$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \ "$ISABELLE_HOME/../ProofGeneral/isar/interface" \ "/usr/share/ProofGeneral/isar/interface" \ diff -r 98af3693f6b3 -r aed221aff642 lib/Tools/dimacs2hol --- a/lib/Tools/dimacs2hol Wed Apr 20 14:18:33 2005 +0200 +++ b/lib/Tools/dimacs2hol Wed Apr 20 16:03:17 2005 +0200 @@ -46,6 +46,6 @@ ## main #set by configure -AUTO_PERL=perl +AUTO_PERL=/usr/bin/perl "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/dimacs2hol.pl" "$@" diff -r 98af3693f6b3 -r aed221aff642 lib/Tools/latex --- a/lib/Tools/latex Wed Apr 20 14:18:33 2005 +0200 +++ b/lib/Tools/latex Wed Apr 20 16:03:17 2005 +0200 @@ -73,7 +73,7 @@ # operations #set by configure -AUTO_PERL=perl +AUTO_PERL=/usr/bin/perl function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } diff -r 98af3693f6b3 -r aed221aff642 lib/Tools/mkdir --- a/lib/Tools/mkdir Wed Apr 20 14:18:33 2005 +0200 +++ b/lib/Tools/mkdir Wed Apr 20 16:03:17 2005 +0200 @@ -1,3 +1,4 @@ + #!/usr/bin/env bash # # $Id$ @@ -285,4 +286,3 @@ EOF fi - diff -r 98af3693f6b3 -r aed221aff642 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Apr 20 14:18:33 2005 +0200 +++ b/src/HOL/IsaMakefile Wed Apr 20 16:03:17 2005 +0200 @@ -119,7 +119,7 @@ Tools/ATP/recon_transfer_proof.ML Tools/ATP/res_clasimpset.ML \ Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML Tools/ATP/modUnix.ML \ Tools/ATP/watcher.sig Tools/ATP/watcher.ML Tools/res_atp.ML\ - document/root.tex hologic.ML simpdata.ML thy_syntax.ML + ##document/root.tex hologic.ML simpdata.ML thy_syntax.ML @$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL diff -r 98af3693f6b3 -r aed221aff642 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Wed Apr 20 14:18:33 2005 +0200 +++ b/src/HOL/Tools/meson.ML Wed Apr 20 16:03:17 2005 +0200 @@ -451,11 +451,6 @@ SUBGOAL (fn (prop,_) => let val ts = Logic.strip_assums_hyp prop - - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "skolem"))) - val _ = TextIO.output(outfile, "in skolemize_tac "); - val _ = TextIO.flushOut outfile; - val _ = TextIO.closeOut outfile in EVERY1 [METAHYPS (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1 diff -r 98af3693f6b3 -r aed221aff642 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Wed Apr 20 14:18:33 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Wed Apr 20 16:03:17 2005 +0200 @@ -8,9 +8,12 @@ (*Jia: changed: isar_atp now processes entire proof context. fetch thms from delta simpset/claset*) (*Claire: changed: added actual watcher calls *) + signature RES_ATP = sig val trace_res : bool ref +val subgoals: Thm.thm list +val traceflag : bool ref val axiom_file : Path.T val hyps_file : Path.T val isar_atp : ProofContext.context * Thm.thm -> unit @@ -25,8 +28,9 @@ struct +val subgoals = []; - +val traceflag = ref true; (* used for debug *) val debug = ref false; @@ -141,7 +145,7 @@ (*********************************************************************) fun call_resolve_tac sign thms sg_term (childin, childout,pid) n = let - val thmstring = Meson.concat_with_and (map string_of_thm thms) + val thmstring = Meson.concat_with_and (map string_of_thm thms) val thm_no = length thms val _ = warning ("number of thms is : "^(string_of_int thm_no)) val _ = warning ("thmstring in call_res is: "^thmstring) @@ -157,7 +161,7 @@ val clauses = make_clauses thms val _ =( warning ("called make_clauses "))*) (*val _ = tptp_inputs clauses prob_file*) - val thmstring = Meson.concat_with_and (map string_of_thm thms) + val thmstring = Meson.concat_with_and (map string_of_thm thms) val goalstr = Sign.string_of_term sign sg_term val goalproofstring = proofstring goalstr @@ -169,6 +173,9 @@ val thmstr = implode no_returns val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n) + val axfile = (File.sysify_path axiom_file) + val hypsfile = (File.sysify_path hyps_file) + val clasimpfile = (File.sysify_path clasimp_file) val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "hellofile"))) val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring); val _ = TextIO.flushOut outfile; @@ -180,7 +187,7 @@ Watcher.callResProvers(childout, [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS", "-FullRed=0%-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", - probfile)]); + clasimpfile, axfile, hypsfile, probfile)]); (* with paramodulation *) (*Watcher.callResProvers(childout, @@ -193,36 +200,14 @@ dummy_tac end -(************************************************) -(* pass in subgoal as a term and watcher info *) -(* process subgoal into skolemized, negated form*) -(* then call call_resolve_tac to send to ATP *) -(************************************************) -(* -fun resolve_tac sg_term (childin, childout,pid) = - let val _ = warning ("in resolve_tac ") - in - SELECT_GOAL - (EVERY1 [rtac ccontr,atomize_tac,skolemize_tac, METAHYPS(fn negs => (warning ("calling call_resolve_tac next ");dummy_tac (*call_resolve_tac negs sg_term (childin, childout,pid)*)))]) - end; - -*) - - -(* Need to replace call_atp_tac_tfrees with call res_provers as it's the dummy one *) - (**********************************************************) (* write out the current subgoal as a tptp file, probN, *) (* then call dummy_tac - should be call_res_tac *) (**********************************************************) -(* should call call_res_tac here, not resolve_tac *) -(* if we take tptpinputs out it gets into call_res_tac then falls over as usual after printing out goalstring. but if we leave it in it falls over here *) -(* dummy tac vs. Doesn't call resolve_tac *) fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) = - ( warning("ths for tptp: " ^ - Meson.concat_with_and (map string_of_thm thms)); + ( warning("in call_atp_tac_tfrees"); tptp_inputs_tfrees (make_clauses thms) n tfrees; @@ -235,16 +220,14 @@ val _ = warning ("sg_term :" ^ (Sign.string_of_term sign sg_term)) in + SELECT_GOAL (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, - METAHYPS(fn negs => (warning("calling call_atp_tac_tfrees with negs" - ^ Meson.concat_with_and (map string_of_thm negs)); - call_atp_tac_tfrees sign negs n tfrees sg_term (childin, childout,pid) ))]) n st + METAHYPS(fn negs => ( call_atp_tac_tfrees sign negs n tfrees sg_term (childin, childout,pid) ))]) n st end; -fun isar_atp_g tfrees sg_term (childin, childout, pid) n = - +fun isar_atp_g tfrees sg_term (childin, childout, pid) n = ((warning("in isar_atp_g"));atp_tac_tfrees tfrees sg_term (childin, childout, pid) n); @@ -265,13 +248,15 @@ in (warning("in isar_atp_goal'")); - (warning("thmstring in isar_atp_goal: "^thmstring)); + (warning("thmstring in isar_atp_goal': "^thmstring)); isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm; isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid) end); -fun isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid) = (if (!debug) then warning (string_of_thm thm) else (isar_atp_goal' thm 1 n_subgoals tfree_lits (childin, childout, pid) )); +fun isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid) = + (if (!debug) then warning (string_of_thm thm) + else (isar_atp_goal' thm 1 n_subgoals tfree_lits (childin, childout, pid) )); (**************************************************) (* convert clauses from "assume" to conjecture. *) @@ -285,7 +270,8 @@ fun isar_atp_aux thms thm n_subgoals (childin, childout, pid) = let val tfree_lits = isar_atp_h thms in - (warning("in isar_atp_aux"));isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid) + (warning("in isar_atp_aux")); + isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid) end; (******************************************************************) @@ -294,20 +280,26 @@ (* passes all subgoals on to isar_atp_aux for further processing *) (* turns off xsymbol at start of function, restoring it at end *) (******************************************************************) - +(*FIX changed to clasimp_file *) fun isar_atp' (thms, thm) = let val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) val _= (warning ("in isar_atp'")) - val prems = prems_of thm + val prems = prems_of thm val sign = sign_of_thm thm - val thms_string = Meson.concat_with_and (map string_of_thm thms) + val thms_string = Meson.concat_with_and (map string_of_thm thms) val thmstring = string_of_thm thm - val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) + val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) (* set up variables for writing out the clasimps to a tptp file *) - val _ = write_out_clasimp (File.sysify_path axiom_file) + + (* val clause_arr = write_out_clasimp (File.sysify_path clasimp_file) clause_arr*) + (*val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) ) *) (* cq: add write out clasimps to file *) - (* cq:create watcher and pass to isar_atp_aux *) - val (childin,childout,pid) = Watcher.createWatcher() + (* cq:create watcher and pass to isar_atp_aux *) + (*val tenth_ax = fst( Array.sub(clause_arr, 10)) + val _ = (warning ("tenth axiom in array is: "^tenth_ax)) + val _ = (warning ("num_of_clauses is: "^(string_of_int (!num_of_clauses))) ) *) + + val (childin,childout,pid) = Watcher.createWatcher(thm) val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid ))) in case prems of [] => () @@ -367,6 +359,7 @@ (* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *) (* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *) (*claset file and prob file*) +(* FIX*) fun isar_local_thms (delta_cs, delta_ss_thms) = let val thms_cs = get_thms_cs delta_cs val thms_ss = get_thms_ss delta_ss_thms @@ -392,11 +385,11 @@ val sg_prems = prems_of thm val sign = sign_of_thm thm val prem_no = length sg_prems - val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems) + val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems) in (warning ("initial thm in isar_atp: "^thmstring)); (warning ("subgoals in isar_atp: "^prems_string)); - (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no))); + (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no))); (isar_local_thms (d_cs,d_ss_thms); (warning("about to call isar_atp'")); isar_atp' (prems, thm)) end; diff -r 98af3693f6b3 -r aed221aff642 src/Pure/mk --- a/src/Pure/mk Wed Apr 20 14:18:33 2005 +0200 +++ b/src/Pure/mk Wed Apr 20 16:03:17 2005 +0200 @@ -87,6 +87,9 @@ if [ -z "$RAW" ]; then ITEM="Pure" echo "Building $ITEM ..." + + echo "raw is $RAW item is $ITEM isabelle is $ISABELLE" + LOG="$LOGDIR/$ITEM" "$ISABELLE" $COPY \