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

Tobias Nipkow nipkow at in.tum.de
Thu Aug 25 14:28:32 CEST 2022

I don't know who you wanted to address when you emailed "Makarius Wenzel 
<isabelle-dev at in.tum.de>", but please use English on this list.


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,
> bu
>> Begin forwarded message:
>> *From: *Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de 
>> <mailto:florian.haftmann at informatik.tu-muenchen.de>>
>> *Subject: **Re: [isabelle-dev] New Code Generator Target: F#*
>> *Date: *25 August 2022 at 08:27:27 CEST
>> *To: *Tobias Nipkow <nipkow at in.tum.de <mailto:nipkow at in.tum.de>>, "Achim D. 
>> Brucker" <adbrucker at 0x5f.org <mailto:adbrucker at 0x5f.org>>, 
>> Isabelle-Development Mailinglist <isabelle-dev at in.tum.de 
>> <mailto:isabelle-dev at in.tum.de>>
>>> 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
>>>>>     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
>>> isabelle-dev at in.tum.de <mailto:isabelle-dev at in.tum.de>
>>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de <mailto:isabelle-dev at in.tum.de>
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5535 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220825/244ff4be/attachment-0001.bin>

More information about the isabelle-dev mailing list