[isabelle-dev] AFP/HLDE

[Makarius]

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