Code generator: config option "code_timinger" triggers measurements of different phases of code generation. See src/HOL/ex/Code_Timing.thy for examples.
This enables a canonical way to examine performance of generated code
and corresponding computations on different levels.
In the process of implementing this a few more steps where done to
eliminate occurences of theory background certificates and a few
closures have been corrected which might be the reason for reported
unplausible timing behaviour of computations relying on the code generator.
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.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
