[isabelle-dev] HOL-Codegenerator_Test error

[Manuel Eberl]

It looks like I'm the one who broke it. It does not work after my commit 
3201ddb00097, but it still works in Fabian's d8e7738bd2e9 immediately 
before.

I have no idea what causes this problem. Maybe one of our resident code 
generator experts could comment on it?

I'll try to find out which code equation exactly causes the problem 
tomorrow. If all else fails, I'll just comment out changes until it 
works again and leave this matter to be re-examined after the release.


Cheers,

Manuel



On 11/01/16 18:16, Lawrence Paulson wrote:
> I have finally installed my great mass of new material, but when I try to test it, it fails as shown below. I can’t imagine what I could have done to trigger such an error. Nearly all of my changes are confined to Multivariate_Analysis. Does anybody have an idea what could be going on here?
>
> Larry
>
> Running HOL-Codegenerator_Test ...
>
> HOL-Codegenerator_Test FAILED
> (see also /Users/lp15/isabelle/Repos/heaps/polyml-5.6_x86-darwin/log/HOL-Codegenerator_Test)
>
>                                             ^
> ROOT.scala:17271: error: ambiguous implicit values:
>   both method semiring_char_0_nat in object Generated_Code of type => Generated_Code.semiring_char_0[Generated_Code.nat]
>   and method semiring_div_nat in object Generated_Code of type => Generated_Code.semiring_div[Generated_Code.nat]
>   match expected type Generated_Code.power[Generated_Code.nat]
>                                    power[nat](cb, ca) else zero_nata())
>                                              ^
> 10 errors found
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>