[isabelle-dev] New Code Generator Target: F#
Achim D. Brucker
adbrucker at 0x5f.org
Thu Aug 25 12:55:14 CEST 2022
Sorry for the longer answer to several aspects. Yesterday was pretty busy
On Thu, Aug 25, 2022 at 08:27:27AM +0200, Florian Haftmann wrote:
> > Having an external contribution in the
> > AFP clearly delineates what comes from the core developers and what not.
As the trustworthy argument, this is a valid argument. And, of course,
as core maintainers, you need to decide what contribution you accept or
now. I will not argue on that.
Still, as Isabelle is an Open Source project, I would have hoped that "pull requests"
(to use the github terminology) are, in principle, welcomed. Again, I am happy to commit
to maintaining it and I am also willing to invest work on bringing it up to the
required level of quality. Or maybe there is room for an 'incubator' concept (to
use Eclipse terminology), i.e., let the code generator print a warning (both in
JEdit/VSCode and the generated code) that this is an externally (less trusted)
contribution, whenever the F# target is used.
If a formal copyright transfer statement needs to be signed (e.g., to assign
copyright to TUM), I am more than happy to sign such an agreement.
> That could indeed by a criterion, although it sacrifices some aspects of
I thought a lot about this and, frankly speaking, I have right now no idea how an
AFP entry can be maintained while, at the same time, ensuring the required
* the code generator setup for Scala, OCaml, and SML is done locally in
the theories defining the formal concepts. This makes a lot of sense, as it
keeps the formal definitions and the code generator setup close together
and, by that, it is very easy to review that customized code_printings
are consistent with the formal definitions.
* as the AFP does not run any generated code, an "Isabelle/F#" in the AFP
would not benefit from the "AFP as regression test" for Isabelle feature,
i.e., there would be no notifications whatsoever if changes in Isabelle
would break anything - actually worse, most likely they would not break
the F# code generation, they would just diverge silently. Also, users
will need to follow additional installations steps manually, as Isabelle
Tools cannot be distributed via the AFP.
* for me, maintaining an AFP entry would essentially mean that I would need
to track all commits in the Isabelle repository and manually port changes
to an external setup that contains a "monolithic" code generator setup.
This would, IMHO, similar to the old code generator setup for Isabelle
around 2005ish, when I did my first prototype of an F# target in the context
of HOL-Testgen. I am sure there have been very good reasons why this
setup has been phased out.
* Currently, by having it on a branch in the mercurial repository and providing
it as deep integration (i.e., next to the SML/OCaml setup), I have the big
benefit that I get all the updates to the SML/OCaml/Scala setup as hg commits
and hg points me rather directly to the changes (they usually pop up as merge
conflicts) and as F# is essentially a ML-dialect, updating the F# Setup only
takes a few minutes. I do not see (again, help and ideas are appreciated) how
I get a similar semi-automated setup working for setup that would be
Thus, I fear that there are only two options with a realistic maintenance workload:
either an integration into Isabelle or the distributing as patch that users need
to apply (or, of course, re-packaging a Isabelle fork). The patch/fork option is,
if course, not attractive for regular users of Isabelle.
More information about the isabelle-dev