[isabelle-dev] New Code Generator Target: F#
makarius at sketis.net
Thu Aug 25 23:54:39 CEST 2022
On 22/08/2022 12:32, Achim D. Brucker wrote:
> You might have seen my announcement on the Isabelle User's mailing list: I added F#
> as a new target language to the code generator. This includes initial system tooling
> for managing a "sandboxed" dotnet environment within Isabelle (similar to the setup
> for, e.g., OCaml). The changeset is available at (I am currently trying to update
> it to the latest Isabelle development version every couple of days):
I don't see an isolated changeset here, only a very complex history, with
branches and merges. Note that the Isabelle development model generally works
without branches (and only trivial merges): it is an easy exercise to do away
with these vices.
After some with your fork experimentation, I did manage to produce an isolated
diff like this (using your version df48d77b38f7:
hg diff --color=never -r default:feature-codegen-fsharp >
The result is attached here, for the record. So it is not that complex, after all.
> The current setup successfully passes the "bin/isabelle build -a" test on Linux (well
> tested) and Windows (infrequent, tests on a VM running Windows 10). Due to lack of
> hardware, I cannot test it on macOS (trusting the documentation from Microsoft, the
> macOS setup should work out of the box, sharing the configuration/implementation for
From my experience, macOS is never "for free". It usually works, but requires
some care and tinkering. It also require a selection of real Mac hardware for
testing: both x86_64-darwin and arm64-darwin.
Looking only briefly at your material, I did not understand where the dotnet /
F# component actually is.
De-facto, I am the universal maintainer of all multiplatform Isabelle
components. At some point, I am certainly interested to understand how F# can
be bundled, but right now is a very bad time for that --- approx. 2 weeks
before RC1 of the Isabelle2022 release.
> I consider, personally, F# to be an interesting member of the ML-family, as it provides
> a step into the world of dotnet-based frameworks and languages (as Scala opens a door
> into the world of JVM-based languages and frameworks).
That could be true, but I have not used F# or dotnet so far.
Note that in Isabelle2022 we will have the Node.js world as a newcomer, via
VSCode and Electron. At some later stage, scala.js might follow. So we already
have a lot to digest to absorb such a huge platforms eventually.
It is still unclear to me, how far this can go.
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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 18205 bytes
Desc: not available
More information about the isabelle-dev