Tobias
On 22/08/2022 12:32, Achim D. Brucker wrote:
Dear Isabelle Developers,
(CC Makarius and Florian - to ensure that you are aware of this email, as I
assume you
are likely to be the most qualified people to advise.)
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
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).
I would appreciate your general opinion on F# as a new code generator target
and,
in particular, your opinion and recommendations on future
maintenance/development
models. I see, in principle two approaches:
1) integrating it into the main distribution of Isabelle or
2) keeping it as a separate "component" (theoretically, it could even be an AFP
entry, if users install dotnet themselves and configure the ISABELLE_DOTNET
environment variable - i.e., without the sandboxed dotnet installation)
Integrating it into the main Isabelle distribution has the advantage that the
code
generator setup for F# would "live" next to the setup for the other target
languages.
This could be beneficial for the future maintenance (if the setup for ML/OCaml
changes,
it would be obvious that F# likely needs to be updated as well) and also would
allow
for using the "ml_program_of_program" function in the structure Code_ML without
duplicating
it. The disadvantage is that it adds quite some weight to the Isabelle
distribution and
its release process (i.e., a non-trivial component, namely dotnet, would be
added).
Keeping it separate has the advantage that it does not require any changes to
the main
distribution. The disadvantage that I see is that maintenance is most likely
harder
and more error-prone (in the sense of following the Isabelle development is a
more
manual process) and installation for end-users is likely to be more
inconvenient as
well.
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).
Thanks a lot!
Best,
Achim
PS: Just to be clear - my focus is to understand how to maintain such a
component
best, and if there is interest in shipping it as a part of Isabelle
itself. My
focus is not to just "throw-it-over-the-fence" and forget it (i.e., to
off-load maintenance to somebody else).
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
