Tobias
On 25/08/2022 12:15, Burkhart Wolff wrote:
Hm, ich wusste nicht, das nur “Developer” mit dem Prädikat IMG (in München gewesen) Beiträge an den Isabelle Bibliotheken leisten können sollen dürfen. Auch wenn das der Isabelle Philosophie von Code-follows-Function zuwider läuft wie in diesem Fall. Da erscheint Larrys Anregung, gewisse Bibliothekskomponenten in die AFP auszulagern in einem neuen (und vielleicht unerwuenschtem) Licht. Nun ja, schade. Um so wichtiger wird es, das die AFP zukünftig Mechanismen hat, wie auch Isabelle Komponenten zugelassen werden koennen. Vielleicht ist das ja in der Tat der bessere Weg. @Makarius/Florian: Gibt es diesbezüglich Neuigkeiten ? Sollte man eine docker-aehnliche Infrastruktur in der AFP haben ? Liebe Grüsse aus dem sonnigen Paris, buBegin forwarded message:*From: *Florian Haftmann <[email protected] <mailto:[email protected]>>*Subject: **Re: [isabelle-dev] New Code Generator Target: F#* *Date: *25 August 2022 at 08:27:27 CEST*To: *Tobias Nipkow <[email protected] <mailto:[email protected]>>, "Achim D. Brucker" <[email protected] <mailto:[email protected]>>, Isabelle-Development Mailinglist <[email protected] <mailto:[email protected]>>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. 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] <mailto:[email protected]> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list [email protected] <mailto:[email protected]> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev_______________________________________________ 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
