On Sun, 16 Dec 2012, Lukas Bulwahn wrote:
If nothing happens, lets say until the last week of the year, I will
start moving find_unused_assms to HOL/ex.
Things have changed in 768a3fbe4149 and it solved the issue in
find_unused_assms.
Excellent -- it seems to work now. In 9efc99c990d5 I have made this a bit
more parallel, so that Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
takes approx. 45s on 4 or 8 cores.
Moving this to Quickcheck_Examples for continous testing made it much
slower, though, probably due to pseudo-random numbers that become really
random in parallel execution. For the moment we better leave it like that
(subject to condition=ISABELLE_FULL_TEST).
Just for your information, it was due to a non-terminating code equation
for the vimage constant.
The Codegenerator_Test session only checks if code is generated but not
if the executable equations make much sense, the find_unused_assm theory
complements that by actually executing a number of generated programs
and should not be dropped in the future if it ever breaks again. A
failure in this theory indicates some open issue in the code generation
process or setup.
OK. It is always better to have a tiny repair by someone who understands
the issue, instead of speculative actions by someone else.
Issue closed. One less problem for the upcoming release.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
