Tracing infrastructure

[GoogleCodeExporter]

We currently have proofTrace, optionalProofTrace, simpTrace, maybe other, to 
trace things happening in the ProofState. The current behavior is mostly as 
follow: these commands are given a string that is printed on stderr when the 
ProofState goes through it. optionalProofTrace and simpTrace have some flag to 
silent them. This is all very ad-hoc.

We can attack the problem in various ways. First, it would be easy to define 
those tactics-specific tracers in a central place, with the flags at the top of 
the file, so that we can enable/disable them at will. 

Second, we might want to dump them somewhere else that stderr: with a bit of 
unsafePerformIO, we could write them down in a regular file, potentially with 
timestamps.

Ideally, this kind of infrastructure ought to be natively provided by Haskell, 
based on the SCCs. A quick look at the tracing infrastructure provided by 
Haskell shows that this might not be the case. Maybe the debugger could be of 
some use. To be explored.

Another point will be to hide those tracing equipment from the literate file. 
I've the feeling that it won't be easy.

Original issue reported on code.google.com by pedag...@gmail.com on 11 Aug 2010 at 6:39

[GoogleCodeExporter]

Original comment by pedag...@gmail.com on 11 Aug 2010 at 6:55

[GoogleCodeExporter]

As a first step, I think your first suggestion is a good one: it would be 
fairly cheap to define a single file for all the tracing commands and provide 
flags to switch them on or off at compile time. We can always add unsafe magic 
later, but since one can usually just redirect stderr to a file, I wouldn't 
prioritise it.

Would lhs2TeX formatting directives let us delete "proofTrace s" automatically, 
when building the Epitome?

Original comment by adamgundry on 12 Aug 2010 at 7:41

[GoogleCodeExporter]

I have done the cheap thing and moved the tracing commands to a single file, 
Kit/Trace.lhs. Feel free to experiment with hiding them.

Original comment by adamgundry on 18 Aug 2010 at 4:08

• Changed state: Started