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

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.


> > _______________________________________________
> > isabelle-dev mailing list
> >
> >
> > elle-dev
> _______________________________________________
> isabelle-dev mailing list
> le-dev
isabelle-dev mailing list

Reply via email to