[isabelle-dev] OCaml 4.06.0 drops nums.cma

[Lars Hupel]

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