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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
