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, bu > Begin forwarded message: > > From: Florian Haftmann <[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]>, "Achim D. Brucker" > <[email protected]>, Isabelle-Development Mailinglist > <[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. > > Florian > > >> >> Tobias >> >> 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 > > _______________________________________________ > isabelle-dev mailing list > [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
