[isabelle-dev] New Code Generator Target: F#

[Florian Haftmann]

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.

Cheers,
	Florian

Am 25.08.22 um 12:55 schrieb Achim D. Brucker:
> Hi,
> 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
>> maintainability.
> 
> 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 
> quality:
> 
> * 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. 
> 
> 
> Best,
>         Achim

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220906/357d0da5/attachment.sig>