>> Recently I changed the interface for invoking the compiler at runtime >> on generated code to use proof data slots rather than unsychronized >> references. The consequence is that there are a lot of non-joinable >> proof data slots laying around in the same module, cf. >> http://isabelle.in.tum.de/reports/Isabelle/rev/f6ab14e61604 > > Which are the non-joinable ones in particular? Did I overlook anything > important?
The ones in predicate_compile_core.ML. They are not used as data
storage but as storage for results of runtime evaluation, which for
technical reasons requires separate slots. Of course you could
generalize this mechanisms to permit application of combinators or such
before storing, but I would argue that runtime evaluation is fragile
enough that you do not want to make it more complicated than needed anyway.
Florian
--
Home:
http://www.in.tum.de/~haftmann
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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
