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

[Achim D. Brucker]

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