[isabelle-dev] New Code Generator Target: F#
florian.haftmann at informatik.tu-muenchen.de
Tue Sep 6 09:44:05 CEST 2022
This thread is still unsettled.
Without going into detail, at the moment I think it is best to postpone
the discussion until the next Isabelle release is published. We
definitely need Makarius have a look on the .NET components integration.
Am 25.08.22 um 12:55 schrieb Achim D. Brucker:
> Sorry for the longer answer to several aspects. Yesterday was pretty busy
> for me.
> 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
> "AFP ready".
> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 228 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev