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

[Peter Lammich]

Can you give some more details on how to achieve this?
> 
> Concrete application: I have a verified SAT solver (lets call that 


1. Gratchk is a similar use-case, where I need to export code, link it
with some external ML code using MLton b/c it's faster, and test the
result for timing regressions. Because gratchk is also bundled with
gratgen, which is implemented in C++, I have not yet put it into the
AFP, b/c that would mean to separate gratchk from gratgen, or to push
C++ code to the AFP, for which I cannot expect an build infrastructure
there.

2. In the AFP, there is the CAVA model checker. It also comes with some
external ML code. I just checked, and this external ML code is already
severely bit-rotten, as it has not been maintained for years now ... at
latest the recent string-literal reform should have reliably killed it.
 
Also, timing regression tests are important when doing such reforms as
the above-mentioned string-literal reform, which has the potential to
severely slowdown the generated code.

--
  Peter



> 
> > _______________________________________________
> > isabelle-dev mailing list
> > isabelle-dev at in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab
> > elle-dev
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev