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

[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