On 09/10/18 10:57, Christian Sternagel wrote:
> On 10/08/2018 04:14 PM, Makarius wrote:
>> On 08/10/18 15:58, Lars Hupel wrote:
>>
>> I don't mind if it is possible to eliminate AFP/HLDE (theory
>> Diophantine_Eqns_Lin_Hom.Solver_Code) outright, and just refrain from
>> doing such things in AFP.
>>
>
> Compiling a binary in HLDE was a mere experiment on our side too. So I
> also do not mind much to remove this again from the AFP.
>
> I would however like to keep theory Solver_Code and still let it
> generate Haskell source code (that is required for the handwritten Main.hs).
The still open question is how to generate the Haskell source without
writing into odd place of the file-system.
Can 'export_code' do that, with a slight modification to produce formal
exports via Export.export?
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
