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
feature-codegen-fsharp.diff.gz
Description: application/gzip
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
