[isabelle-dev] HOL-Codegenerator_Test error

Manuel Eberl eberlm at in.tum.de
Tue Jan 12 12:04:32 CET 2016

There are actually several affected functions:


I have no idea what causes this and why my changed affected it. I also 
do not have the faintest idea what I could possibly do to fix it. I also 
do not understand why "export_code … checking" puts everything in a 
single module and if that perhaps has anything to do with it. If I 
simply do "export_code" (without "checking" and "module_name"), the 
problem does /not/ occur. (another completely different problem occurs, 
something about implicits and Typereps)

 From what I have seen so far, it seems like there are some lingering 
issues with code generation in general and Codegenerator_Test in 
particular that my rather innocuous change exposed, and that simply 
deleting that one code equation that I added is not the solution we want 
(not even in the short term).

Moreover, at least one AFP entry (namely Rene Thiemann's 
Algebraic_Numbers) crucially depends on a similar code equation for 
"binomial", which causes the exact same problem. We could just leave 
this orphaned code equation in the AFP for now, but that does not strike 
me as a good solution either.



More information about the isabelle-dev mailing list