> So I would like to focus: > * What (upcoming) maintenance challenges are we facing?
There are many applications in the AFP that link generated code to larger developments. For example, Julian Brunner recently updated the CAVA model checker because it is not tested systematically (e.g. nightly), and the Isabelle formalization had diverged from the remaining code. Similarly, this also affects the "Iptables_Semantics" sessions where the other code is kept separately. I haven't recently investigated whether or not the generated code still compiles cleanly with the rest. In essence, this is a "luxury problem": People are building bigger applications with Isabelle on a wider variety of platforms, so more things need to be tested. > * Are there particular applications out there which suggest more > integration with ocaml? Simon Wimmer's timed automata formalization. I'll let him speak about the technical details. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
