On 07/06/18 11:41, Florian Haftmann wrote:
> 
> How significant is Isabelle as an integrative platform for OCaml?

So far: insignificant.


> So I would like to focus:
> * What (upcoming) maintenance challenges are we facing?
> * Are there particular applications out there which suggest more
> integration with ocaml?

I have been thinking of why3 for Isabelle/HOL-SPARK, but with the
dependency on make, m4, gcc, the "isabelle opam" component will not make
that magically available to end-users. (We have abandomed the user-model
with "make" many years ago.)


        Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to