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