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

Salomon Sickert sickert at in.tum.de
Mon Feb 4 08:00:22 CET 2019

> 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


>>  * 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

More information about the isabelle-dev mailing list