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

[Achim D. Brucker]

Hi,

On Thu, Aug 25, 2022 at 11:54:39PM +0200, Makarius wrote:
> 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.

yes, the link goes to a "living" branch that I keep (currently) in sync with the 
development repository of Isabelle. Any isolated diff can only be static, hence, 
I thought that a branch is more convenient and a diff can easily obtained from it. 
But I am neither a hg expert not do I know all the conventions of the Isabelle 
development team.  

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

Indeed, the additions to the Isabelle code generator are not that large and also 
not that complex. F# is syntax-wise a mix of ML and Ocaml. The main challenge, so 
to speak, was that F# requires indentation for block structures. This is implemented 
in "print_fsharp_stmt" (which is based on print_ocaml_stmt) in the structure Code_ML.

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

yes, this is what I fear too (while it mostly should work, the occasional 
tinkering and testing will be needed). Sadly, I do lack access to this setup 
right now ... 

> Looking only briefly at your material, I did not understand where the dotnet
> / F# component actually is.

The dotnet component (actually, the full dotnet SDK) needs to be installed using 

isabelle dotnet_setup 

This is similar to "isabelle ghc_setup". The ghc_setup tool (in ./lib/Tools/dotnet_setup).
I did not touch the "Admin" component part. Firstly, this really only makes sense if the F# 
setup becomes integrated into the Isabelle distribution, and, secondly, the component 
registration is an area of Isabelle that I do not know well). 

Internally, the "dotnet_setup" tool obtains an installation script from a fixed domain provided 
by Microsoft (i.e., this is promised to be a stable URL by Microsoft). There are two version of 
this script: a PowerShell script for Windows and a Bash script for Linux/macOS. After downloading 
this script, the "dotnet_setup" tool executes the script to install the dotnet runtime (without user 
intervention) into $ISABELLE_DOTNET_ROOT (the current default value is 
$ISABELLE_HOME_USER/dotnet-$ISABELLE_DOTNET_VERSION). 

This is somewhat similar to the ghc/ocaml setup where stack/opam is used for installing the 
actual dotnet platform (SDK). The difference is that also the installation script is obtained
"on demand" - this seems to be recommended by Microsoft to ensure that always the latest 
dotnet installation script is used (the version of the dotnet framework/SDK that is actually
installed is fixed to the version specified in the Isabelle settings). If this is the 
best approach for an Isabelle integration or if, e.g., integrating this install script 
as a proper Isabelle component (as opam, if I understood the current setup correctly),
is something where I would love to hear your opinion on (when time permits). 

F# is one of the two first-class citizen of dotnet. Hence, as soon as the dotnet SDK 
is installed, F# is available (e.g., by invoking "dotnet fsi"). 

I hope this clarifies the questions "where the dotnet component actually is" question. 

To be clear: I did not register dotnet in Admin/components. My approach is a kind of 
"user installation", as I did not want to fiddle around with a part of the Isabelle 
repository that I do not understand well enough to do this with the necessary level
of confidence. 

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

Happy to postpone the discussion to after the Isabelle 2022 release. And, again, if 
there is a good technical setup allowing to maintain such a code generator configuration 
outside of the Isabelle main repository - happy to hear about it. 

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

I do not want to hide the truth: while dotnet/F# is a stable platform that is used in 
production, it has its own culture and tooling. The current setup only uses a tiny bit 
of it, namely "F# interactive" (the REPL, so to speak). 

Without knowing exactly how much occasional manual tinkering GHC and Ocaml require, my 
best guess is that dotnet/F# would be in a similar ball park. Microsoft offers 3 years 
of support for LTS releases of dotnet. Thus, some tinkering is required every 2-3 years 
to switch to the latest LTS release. As the code generator setup maps to the (stable) 
core of the language and does not make use of any additional libraries, this should 
still fall into the "little bit of manual tinkering" category, hopefully. 

Achim