c.sternagel at gmail.com
Tue Oct 9 10:57:03 CEST 2018
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).
Then the task of setting up a proper Haskell environment and compiling
an executable is moved to prospective users. Which is fine with me.
More information about the isabelle-dev