On 26/08/2022 01:01, Achim D. Brucker wrote:
For example, the absorption of GHC stack and OCaml opam some years ago did
not fully work out: these projects have there very own culture that does not
fully fit into Isabelle. We did not gain the stability and
self-containedness of GHC and OCaml that we were hoping for: it still
requires manual tinkering occasionally.
I do not want to hide the truth: while dotnet/F# is a stable platform that is
used in
production, it has its own culture and tooling. The current setup only uses a
tiny bit
of it, namely "F# interactive" (the REPL, so to speak).
Without knowing exactly how much occasional manual tinkering GHC and Ocaml
require, my
best guess is that dotnet/F# would be in a similar ball park. Microsoft offers
3 years
of support for LTS releases of dotnet. Thus, some tinkering is required every
2-3 years
to switch to the latest LTS release. As the code generator setup maps to the
(stable)
core of the language and does not make use of any additional libraries, this
should
still fall into the "little bit of manual tinkering" category, hopefully.
Thanks. From your explanations, I have learned many things about F# and dotnet.
Can you also say what your applications are?
Dotnet was once positioned as the next big thing, but recently we have seen
more excitement elsewhere (even by Microsoft): e.g. Node.js/Electron.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
