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

Makarius makarius at sketis.net
Sat Nov 5 23:29:23 CET 2022

On 04/11/2022 20:40, Florian Haftmann wrote:
> Meanwhile in personal conversation Tobias and me finally agreed that, 
> concerning code generation itself, the best solution is to follow Achim’s 
> original proposal and put the F# serializer into the distribution.
> @Makarius – while the .NET component setup looks promising for me, I am no 
> expert in that area and I think we need your final judgement on this.

I have spent some time with the "isabelle dotnet_setup" script by Achim and 
have turned the main ideas into proper "lambda calculus for systems 
programming" (aka Scala): 

The key by Microsoft documentation is here: 

So this is our NEWS entry in Isabelle/da85bffef443:

*** System ***

* The command-line tools "isabelle dotnet_setup" and "isabelle dotnet"
support the Dotnet platform (.NET), which includes Fsharp (F#). This
works uniformly on all Isabelle OS platforms, even as cross-platform
installation: "isabelle dotnet_setup -p linux_arm,linux,macos,windows".


   isabelle dotnet_setup
   isabelle dotnet fsi
   > 1 + 1;;
   > #quit;;

The multiplatform installation script from the Dotnet project looks fairly 
robust. At least the "1 + 1" example works smoothly on all Isabelle platforms.

For the cross-platform installation of windows on linux, I have used the 
"powershell" snap of Ubuntu 22.04 LTS, just for the fun of it.

So the main remaining question for Isabelle/HOL codegen support is the proper 
spelling of "F#". I would say it is "Fsharp" for the Isar command syntax and 
"fsharp" in plain ML names.


More information about the isabelle-dev mailing list