[isabelle-dev] NEWS: generated code as proper theory export

[Salomon Sickert]

> On 1. Feb 2019, at 15:30, Lars Hupel <hupel at in.tum.de> wrote:
> 
>> What are the remaining uses of these? How much of this can be integrated
>> into the formal Isabelle session? How much of it is actually obsolete?
> 
> Hard to tell from a distance, but here's what I gather from reading the
> Makefiles:
> 
> – Formal_SSA appears to download some file, unpack it, and compile
> generated code together with it.
> 
> – Lightweight_Java generates an Isabelle theory file with Ott.
> 
> – Buchi_Complementation compiles generated code with MLton.
> 
> – Sturm_Sequences produces some extra LaTeX documentation. The generated
> PDF is even committed to the AFP.

To add a couple more to the list:

— LTL has includes a parser that is used in an example and built using LTL/examples/build_poly.sh

— LTL_to_DRA can generate a tool using either LTL_to_DRA/Code/build_poly.sh and LTL_to_DRA/Code/build_mlton.sh

Best,
Salomon

>>  * no generated files in the repository (these are not sources but
>> results from sources)
> 
> What about generated theory files? This also affects the CakeML entry. I
> could easily package Lem as a component, but how would "isabelle build"
> call it?
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev