Re: [isabelle-dev] AFP/HLDE
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
[isabelle-dev] System migration
Dear Isabelle developers and users, we will perform a large-scala system migration over the next 24–48 hours. The purpose is to move towards the latest Ubuntu 18.04 LTS. Affected will be continuous integration, the AFP, and the AFP submission service. Expect intermittent unavailability and HTTPS errors. I will update as soon as the migration is completed. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP/HLDE
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. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
