<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Hm, ich wusste nicht, das nur “Developer” mit dem Prädikat <div class="">IMG (in München gewesen) Beiträge an den Isabelle Bibliotheken</div><div class="">leisten können sollen dürfen. Auch wenn das der Isabelle Philosophie</div><div class="">von Code-follows-Function zuwider läuft wie in diesem Fall.</div><div class=""><br class=""></div><div class="">Da erscheint Larrys Anregung, gewisse Bibliothekskomponenten</div><div class="">in die AFP auszulagern in einem neuen (und vielleicht unerwuenschtem) Licht.</div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">Nun ja, schade. Um so wichtiger wird es, das die AFP zukünftig </div><div class="">Mechanismen hat, wie auch Isabelle Komponenten zugelassen werden </div><div class="">koennen. Vielleicht ist das ja in der Tat der bessere Weg.</div><div class=""><br class=""></div><div class="">@Makarius/Florian: Gibt es diesbezüglich Neuigkeiten ?</div><div class="">Sollte man eine docker-aehnliche Infrastruktur in der AFP haben ?</div><div class=""><br class=""></div><div class="">Liebe Grüsse aus dem sonnigen Paris,</div><div class=""><br class=""></div><div class="">bu</div><div class=""><br class=""><div class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">Begin forwarded message:</div><br class="Apple-interchange-newline"><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;" class=""><span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif; color:rgba(0, 0, 0, 1.0);" class=""><b class="">From: </b></span><span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif;" class="">Florian Haftmann <<a href="mailto:florian.haftmann@informatik.tu-muenchen.de" class="">florian.haftmann@informatik.tu-muenchen.de</a>><br class=""></span></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;" class=""><span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif; color:rgba(0, 0, 0, 1.0);" class=""><b class="">Subject: </b></span><span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif;" class=""><b class="">Re: [isabelle-dev] New Code Generator Target: F#</b><br class=""></span></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;" class=""><span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif; color:rgba(0, 0, 0, 1.0);" class=""><b class="">Date: </b></span><span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif;" class="">25 August 2022 at 08:27:27 CEST<br class=""></span></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;" class=""><span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif; color:rgba(0, 0, 0, 1.0);" class=""><b class="">To: </b></span><span style="font-family: -webkit-system-font, Helvetica Neue, Helvetica, sans-serif;" class="">Tobias Nipkow <<a href="mailto:nipkow@in.tum.de" class="">nipkow@in.tum.de</a>>, "Achim D. Brucker" <<a href="mailto:adbrucker@0x5f.org" class="">adbrucker@0x5f.org</a>>, Isabelle-Development Mailinglist <<a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a>><br class=""></span></div><br class=""><div class=""><div class=""><blockquote type="cite" class="">Having an external contribution in the<br class="">AFP clearly delineates what comes from the core developers and what not.<br class=""></blockquote><br class="">That could indeed by a criterion, although it sacrifices some aspects of<br class="">maintainability.<br class=""><br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>Florian<br class=""><br class=""><br class=""><blockquote type="cite" class=""><br class="">Tobias<br class=""><br class="">On 23/08/2022 18:13, Florian Haftmann wrote:<br class=""><blockquote type="cite" class="">Hi Achim and Tobias &al.,<br class=""><br class=""><blockquote type="cite" class="">I would appreciate your general opinion on F# as a new code generator<br class="">target and,<br class="">in particular, your opinion and recommendations on future<br class="">maintenance/development<br class="">models. I see, in principle two approaches:<br class=""><br class="">1) integrating it into the main distribution of Isabelle or<br class="">2) keeping it as a separate "component" (theoretically, it could even<br class="">be an AFP<br class=""> entry, if users install dotnet themselves and configure the<br class="">ISABELLE_DOTNET<br class=""> environment variable - i.e., without the sandboxed dotnet<br class="">installation)<br class=""></blockquote><br class=""><blockquote type="cite" class="">the code generator is part of Isabelle's trusted infrastructure. Thus<br class="">I recommend you provide your F# code generator as an AFP entry in the<br class="">Tools category.<br class=""></blockquote><br class="">IMHO this argument on its own does not apply here. The code generator<br class="">is modular: adding another target language does not<br class="">affect existing target languages and hence does not affect their<br class="">trustworthiness, particularly not of Isabelle/ML (»Eval«)<br class="">which is at the core of all proof-replacing evaluation mechanisms.<br class=""><br class="">Concerning trustworthiness in general, the code generator by its<br class="">architecture can never achieve the trustworthiness of e. g.<br class="">the LCF-style inference kernel: you are always free to configure<br class="">pointless or »unsound« things, sometimes burdening<br class="">users to come up with an appropriate »interpretation« what generated<br class="">code means in relaton to its originating theory;<br class="">a prominent example from the distribution is<br class="">HOL/Library/Code_Real_Approx_By_Float.thy.<br class=""><br class="">Hence from my perspective it is difficult to argue that there are<br class="">fundamental differences between distribution<br class="">and AFP concerning trustworthiness of code generation.<br class=""><br class=""> From a maintenance perspective, integration into the distribution seems<br class="">actually to be the more appropriate way:<br class="">we have the tradition to setup target-language specific things in<br class="">theories where their corresponding logical<br class="">notions comes up (e. g. List.thy), and this makes things easier to<br class="">maintain and re-check across all target languages.<br class=""><br class="">There might still be other issues suggesting the AFP.<br class=""><br class="">Cheers,<br class=""> Florian<br class=""><br class=""></blockquote><br class="">_______________________________________________<br class="">isabelle-dev mailing list<br class=""><a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class="">https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev<br class=""></blockquote><br class="">_______________________________________________<br class="">isabelle-dev mailing list<br class=""><a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class="">https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev<br class=""></div></div></blockquote></div><br class=""></div></div></body></html>