[isabelle-dev] New Code Generator Target: F#
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 fsi
> 1 + 1;;
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