Re: [isabelle-dev] Code preprocessor tracing
Hi Florian, Thanks for all this. 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. You are right. There are more urgent things to do. I'll keep it at the back of my head. Best, Andreas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code preprocessor tracing
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 signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code preprocessor tracing
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, Andreas 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Code preprocessor tracing
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 -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
