> 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.
This is not a new problem. It is merely slightly exacerbated by making it more difficult to run such tests manually. There have been various discussions about this in the past, but they are all orthogonal to the issue of code generation. It would like to reiterate that the technical part of this issue is the easy bit. The difficult bit is deciding policy: Should Isabelle committers be responsible for breakage in downstream artifacts? In other words, should the AFP stability guarantees be extended? Right now we have that odd situation where extra sources are present (e.g. Makefiles) but nobody bothers to look at them. Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
