Email Gateway (Jul 20 2022 at 19:14): Email Gateway (Jul 20 2022 at 19:14):From: "Achim D. Brucker" <adbrucker@0x5f.org>
Dear all,
I would like to collect feedback of an experimental implementation
of a new target language for Isabelle: F#. F# is a member of the ML
language family on the dotnet platform.
The current implementation is available as a branch ("feature-codegen-fsharp")
in a fork of Isabelle's Mercurial repository (i.e., the latest development
version):
https://hg.logicalhacking.com/isabelle/shortlog/feature-codegen-fsharp
The current implementation is "mature" enough to successfully generate code for
the "Generate_*" theory files (i.e., I tested the sessions HOL, HOL-Library, and
Imperative_HOL). Of course, it is by far not as well tested (and, due to lack of
hardware, I did not test it on OS X) as the already supported target languages.
Still, I hope it is mature enough to collect feedback and discuss its future.
To use the F# target, please follow, after cloning the Mercurial repository, the
instruction in the file "README_REPOSITORY", i.e., the standard installation for
the repository version of Isabelle. After these steps have been completed
successfully, there should be three new Isabelle tools:
isabelle dotnet_setup - install dotnet (for F# support)isabelle dotnet - invoke the dotnet CLI tool within the Isabelle environmentisabelle fsi - invoke the F# top-level within the Isabelle environmentFor using F# as a target language, you need to install dotnet using the
isabelle dotnet_setup tool. Just calling this tool, e.g., if you are in the
toplevel directory of your repository clone:
bin/isabelle dotnet_setup
will download the dotnet SDK and install it into the directory
$ISABELLE_HOME_USER/dotnet (note, this requires ca. 500MB of disk space and a
working Internet connection). After the installation of the dotnet SDK, you
should be able to use F# as a new code generator target, e.g.,
export_code gcd "F#"
There are clearly areas for improvements and open issues. For example:
F# uses indentation for block structures. To make the compiler happy, I used
Pretty.unbreakable a few times. I would be happy to learn, if there are better
ways of pretty printing languages with a rather strict requirements on
concrete syntax formatting.
Any further testing is helpful (I am sure, there are still bugs in the generated
code)
The setup tool uses an installation script (bash/powershell) for the headless
installation of dotnet. I tested it rather thoroughly on Linux and did also
some quick tests on Windows. It should work on OS X as well, but I sadly could
not test it. In general, this tooling (which is currently in the "user space"
is an area where feedback is particularly welcomed)
I am keen to learn what the best way for future maintenance is (Isabelle
component, integration into the Isabelle main distribution, etc.).
Thanks a lot!
Best,
Achim
PS: I would like to thank Florian Haftmann for the already provided
help and feedback!
Last updated: Jan 04 2025 at 20:18 UTC