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-...@in.tum.de > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab > > elle-dev > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel > le-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
