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