Thomas Gebert (May 27 2022 at 19:01): Thomas Gebert (May 27 2022 at 19:01):Hi! I'm a bit new to Isabelle, and have thoroughly enjoyed playing with the code exporter. I would like to create a backend for F# so that I might be able to use exported Isabelle code for production at at .NET stop. Is there documentation on how to do this?
Lukas Stevens (May 29 2022 at 18:12):@Tobias Nipkow Didn't you have a student working on a code export to python? In general, you would need to direct this question to Florian Haftmann who is the expert on this and unfortunately not on Zulip.
Lukas Stevens (May 29 2022 at 18:15):Furthermore, there is documentation for the code generator. And you could try to look at how it is done for other languages.
Achim Brucker (May 29 2022 at 18:20):As part of HOL-TestGen, we developed a code generator for F#. Sadly, the last Isabelle version I am sure it works with is Isabelle 2016 (maybe 2017). Re-activating it, is on my eternal to-do-list :-(. Overall, the changes required to the Ocaml target is rather small. It might even be possible to support both Ocaml and F# essentially with the same code-generator "back-end" (it should, though, still be a separate language to allow customization, such as target mappings, that differ between Ocaml and F#). With a lot of luck, I have time over the summer to re-activate the project and also discuss, what is necessary to get a F# target into the Isabelle main distribution. I definitely would not like to continue to maintain it outside of Isabelle itself ...
Tobias Nipkow (May 30 2022 at 07:44):No code generator for Python in the works (at the moment) I am afraid. But having one for F# would indeed be cool!
Achim Brucker (May 30 2022 at 07:58):I will try to have a look into the "new" (changes since Isabelle 2017, which IMO was the last version I got my home-grown F# generator to work) code generator setup over the summer (it is on my to-do list anyways and there is another project on my stack that would benefit from it). While I do not believe that the core part of Ocaml and F# deviated a lot in the last couple of years, it is something to check as well. As far as I remember, I mostly needed to ensure whitespaces/indentations for F#, as F# block structure is purely based on indentation (as Haskell's is), while Ocaml somewhat more flexible. Otherwise a few constants and library functions had different names, but overall, it was not too difficult. My motivation to develop it in the first place was to have access to the whole Microsoft environment via F#/dotnet (similar as Scala provides access to the whole Java environment).
Florian Haftmann (May 31 2022 at 17:51):Hi Achim, I am happy to help with integrating a pre-existing F# code generator into the Isabelle distribution, but I think details are discussed best at a personal virtual meeting. You can ping me by e-mail for that (I am not a regular follower of discussions on Zulip.)
Note that integrating into the Isabelle distribution very likely means a standard similar to the existing integration of OCaml and Haskell by means of isabelle tools ghc_setup, ocaml_setup etc.
Florian Haftmann (May 31 2022 at 17:54):@Thomas Gebert you are very welcome to join that effort, but this maybe required to disclose an e-mail account of yours to Achim or also me.
Achim Brucker (Jul 20 2022 at 19:20):For those monitoring this thread: I just posted an update of the current status to the Isabelle User's mailing list:
<https://isabelle.zulipchat.com/#narrow/stream/247541-Mirror.3A-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20Request.20for.20Feedback.20-.20New.20Code.20Generator.20Targ.2E.2E.2E>
Manuel Eberl (Jul 20 2022 at 20:36):This sounds like a staggering amount of work. Nice job!
Last updated: Dec 21 2024 at 12:33 UTC