[isabelle-dev] HOL-Codegenerator_Test error

[Lawrence Paulson]

I had a problem like this last year. Unlike a broken proof, they seem almost impossible to fix. Something’s fragile about this setup.
Larry

> On 12 Jan 2016, at 11:04, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> There are actually several affected functions:
> 
> Discrete.sqrt
> size_fset
> lapprox_posrat
> size_multiset
> set_encode
> card_UNIV_fun
> card_UNIV_set
> card_UNIV_finfun
> 
> 
> 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.
> 
> 
> Cheers,
> 
> Manuel
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev