On 25/08/2022 08:27, Florian Haftmann wrote:
Having an external contribution in the AFP clearly delineates what comes from the core developers and what not.That could indeed by a criterion, although it sacrifices some aspects of maintainability.
It sounds to me like this could be overcome by a well-defined interface that allows people to add their own code generator.
Tobias
FlorianTobias On 23/08/2022 18:13, Florian Haftmann wrote:Hi Achim and Tobias &al.,I would appreciate your general opinion on F# as a new code generator target and, in particular, your opinion and recommendations on future maintenance/development models. I see, in principle two approaches: 1) integrating it into the main distribution of Isabelle or 2) keeping it as a separate "component" (theoretically, it could even be an AFP entry, if users install dotnet themselves and configure the ISABELLE_DOTNET environment variable - i.e., without the sandboxed dotnet installation)the code generator is part of Isabelle's trusted infrastructure. Thus I recommend you provide your F# code generator as an AFP entry in the Tools category.IMHO this argument on its own does not apply here. The code generator is modular: adding another target language does not affect existing target languages and hence does not affect their trustworthiness, particularly not of Isabelle/ML (»Eval«) which is at the core of all proof-replacing evaluation mechanisms. Concerning trustworthiness in general, the code generator by its architecture can never achieve the trustworthiness of e. g. the LCF-style inference kernel: you are always free to configure pointless or »unsound« things, sometimes burdening users to come up with an appropriate »interpretation« what generated code means in relaton to its originating theory; a prominent example from the distribution is HOL/Library/Code_Real_Approx_By_Float.thy. Hence from my perspective it is difficult to argue that there are fundamental differences between distribution and AFP concerning trustworthiness of code generation. From a maintenance perspective, integration into the distribution seems actually to be the more appropriate way: we have the tradition to setup target-language specific things in theories where their corresponding logical notions comes up (e. g. List.thy), and this makes things easier to maintain and re-check across all target languages. There might still be other issues suggesting the AFP. Cheers, Florian_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
