[isabelle-dev] Code preprocessor tracing

Andreas Lochbihler andreas.lochbihler at inf.ethz.ch
Wed Sep 10 11:56:44 CEST 2014

Hi Florian,

Sorry for the long delay until you get an answer, but I wanted to wait until I can port my 
application from Isabelle2013-2 to 2014. The tracing facility seems to provide some basic 
means to limit the scope of the tracing. I found the two suggestions for improvement:

1. The rewriting with the simplifier can be traced, but I have not been able to activate 
it for function transformers (as, e.g., in Code_Target_Nat for 0/Suc). If tracing for 
function X is active, it might be useful to display the set of equations before and after 
the application of each function transformer.

2. Meanwhile, I really like the new simplifier tracing facility and hardly ever use the 
old [[simp_trace]]. Since the new trace offers a lot of control over the tracing, would it 
make sense to base the tracing facility on the new one?

Thanks for your efforts,

On 29/06/14 18:00, Florian Haftmann wrote:
> Hi Andreas,
> with http://isabelle.in.tum.de/repos/isabelle/rev/020cea57eaa4 I have
> provided very basic means to trace the code preprocessor.  Alas, I only
> dimly remember what your real requirements are, so feel free to comment
> on it.  Anyway, it is a starting point.
> Cheers,
> 	Florian

More information about the isabelle-dev mailing list