[isabelle-dev] OCaml 4.06.0 drops nums.cma

Makarius makarius at sketis.net
Thu Jun 7 11:54:56 CEST 2018


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



More information about the isabelle-dev mailing list