[isabelle-dev] New Code Generator Target: F#

[Makarius]

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):
> 
>    https://hg.logicalhacking.com/isabelle/shortlog/feature-codegen-fsharp

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 > 
feature-codegen-fsharp.diff

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

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


	Makarius
-------------- next part --------------
A non-text attachment was scrubbed...
Name: feature-codegen-fsharp.diff.gz
Type: application/gzip
Size: 18205 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220825/17eade7f/attachment-0003.gz>