Re: [isabelle] Death by tracing



I spoke to Johannes about it and he agreed it would be best to just remove that output. Since I have an AFP entry in preparation that relies on approximation_tac, it would be good if this could make it into the release.

The attached patch should take care of it. (I also attached a bundle, but I never used those before so I don't know if I did it correctly)

Cheers,

Manuel


On 2016-12-06 16:43, Makarius wrote:
On 06/12/16 14:55, Lars Hupel wrote:
I noticed this problem when I proved 1024 theorems with the
âapproximationâ method, which outputs one line of tracing information
every time. Does this mean that âapproximationâ shouldn't be using
âtracingâ to output this information?
Probably not by default, or at least with the option to disable it.
Tracing is in some sense debugging, and that should have an option to
*enable* it, i.e. it should be *disabled* by default.

We have a long record of really strange effects caused by tools
producing "potentially useful output" by default. I put that phrase into
quotes, because it is a technical term of Isabelle lore.

These effects might be technical (e.g. bombing the front-end) or
psychological (e.g. tons of irrelevant messages hiding one important
message that indicates an error, which is then overlooked).


	Makarius



diff -r e61de633a3ed src/HOL/Decision_Procs/approximation.ML
--- a/src/HOL/Decision_Procs/approximation.ML   Sun Dec 04 13:47:56 2016 +0100
+++ b/src/HOL/Decision_Procs/approximation.ML   Tue Dec 06 16:42:42 2016 +0100
@@ -43,7 +43,7 @@
   end
 
 fun approximation_conv ctxt ct =
-  approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct |> tap (tracing o Syntax.string_of_term ctxt));
+  approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct);
 
 fun approximate ctxt t =
   approximation_oracle (Proof_Context.theory_of ctxt, t)

Attachment: isabelle_release_approximation.bundle
Description: Binary data



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.