From 99a272204b8840aa0e8aa29a64674f4516c5b561 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 15 Nov 2011 17:18:43 +0000 Subject: [PATCH] Fixes a bug in NnAuto: printing the statistics triggered loading of objects from the library into the environment. --- matitaB/components/ng_tactics/nnAuto.ml | 18 +++++++++++------- matitaB/matita/matitadaemon.ml | 13 ++++++++----- 2 files changed, 19 insertions(+), 12 deletions(-) diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml index 697355db2..d65fda22d 100644 --- a/matitaB/components/ng_tactics/nnAuto.ml +++ b/matitaB/components/ng_tactics/nnAuto.ml @@ -72,8 +72,12 @@ let print_stat status tbl = let vcompare (_,v1) (_,v2) = Pervasives.compare (relevance v1) (relevance v2) in let l = List.sort vcompare l in + let short_name r = + Filename.chop_extension + (Filename.basename (NReference.string_of_reference r)) + in let vstring (a,v)= - NotationPp.pp_term status (Ast.NCic (NCic.Const a)) ^ ": rel = " ^ + short_name a ^ ": rel = " ^ (string_of_float (relevance v)) ^ "; uses = " ^ (string_of_int !(v.uses)) ^ "; nom = " ^ (string_of_int !(v.nominations)) in @@ -591,7 +595,7 @@ let compare_statuses ~past ~present = List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past) ;; -(* paramodulation has only an implicit knoweledge of the symmetry of equality; +(* paramodulation has only an implicit knowledge of the symmetry of equality; hence it is in trouble in proving (a = b) = (b = a) *) let try_sym tac status g = (* put the right uri *) @@ -986,9 +990,9 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t = debug_print (lazy ("expected branching: " ^ (string_of_int res))); debug_print (lazy ("actual: branching" ^ (string_of_int diff))); (* some flexibility *) - if og_no - old_og_no > res then + if diff > res && res > 0 (* facts are never pruned *) then (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = " - ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no))); + ^ (string_of_int res) ^ " vs. " ^ (string_of_int diff))); debug_print ~depth (lazy "strange application"); None) else (incr candidate_no; Some ((!candidate_no,t),status)) @@ -1729,7 +1733,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = (* pp_th status facts; *) (* NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t -> - debug_print (lazy( + (*debug_*)print (lazy( NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^ String.concat "\n " (List.map ( status#ppterm ~metasenv:[] ~context:[] ~subst:[]) @@ -1800,10 +1804,10 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = in let s = s#set_stack stack in trace_ref := trace; - oldstatus#set_status s + oldstatus#set_status s in let s = up_to depth depth in - debug_print (print_stat status statistics); + debug_print (print_stat status statistics); debug_print(lazy ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); debug_print(lazy diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 20a1d91c9..14bcf1db6 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -407,7 +407,7 @@ let advance0 sid text = let status = status#reset_disambiguate_db () in let (st,new_statements,new_unparsed),parsed_len = try - eval_statement !include_paths (*buffer*) status (`Raw text) + eval_statement !include_paths (*buffer*) status (`Raw text) with | HExtlib.Localized (floc,e) as exn -> let x, y = HExtlib.loc_of_floc floc in @@ -758,7 +758,8 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ~status:`Internal_server_error ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" - ()); + () + ); cgi#out_channel#commit_work() ;; @@ -841,12 +842,12 @@ let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let baseuri = status#baseuri in let new_status = new MatitaEngine.status (Some uid) baseuri in prerr_endline "gototop prima della time travel"; - NCicLibrary.time_travel new_status; + (* NCicLibrary.time_travel new_status; *) prerr_endline "gototop dopo della time travel"; let new_history = [new_status] in MatitaAuthentication.set_history sid new_history; MatitaAuthentication.set_status sid new_status; - NCicLibrary.time_travel new_status; + (* NCicLibrary.time_travel new_status; *) cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" @@ -891,7 +892,9 @@ let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string body - with _ -> cgi#set_header ~status:`Internal_server_error + with e -> + prerr_endline ("error in retract: " ^ Printexc.to_string e); + cgi#set_header ~status:`Internal_server_error ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" ()); cgi#out_channel#commit_work() -- 2.39.2