[isabelle-dev] Code preprocessor tracing

[Florian Haftmann]

Hi Andreas,

> 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.

See now http://isabelle.in.tum.de/reports/Isabelle/rev/d230e7075bcf

> 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?

It would definitely make sense, but at the moment I will not put any
personal effort into this.  Contributions welcome for review.

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20141006/963e44db/attachment.asc>