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

[Makarius]

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): 
https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Pure/Tools/dotnet_setup.scala;da85bffef443

The key by Microsoft documentation is here: 
https://learn.microsoft.com/en-us/dotnet/core/tools/dotnet-install-script


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

Example:

   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.


	Makarius