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

[Tobias Nipkow]

Achim, the code generator is part of Isabelle's trusted infrastructure. Thus I 
recommend you provide your F# code generator as an AFP entry in the Tools category.

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
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5535 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220823/96013154/attachment.bin>