[isabelle-dev] Scala implicits

[Manuel Eberl]

Florian, what are you plans w.r.t. merging this patch into the distribution?

Manuel


On 23/06/16 11:22, Manuel Eberl wrote:
> Looks good. After applying the patch, HOL-Codegenerator_Test goes 
> through with the code equation in Binomial.thy enabled.
>
>
> Cheers,
>
> Manuel
>
>
> On 23/06/16 09:48, Manuel Eberl wrote:
>> The uncommented code equation at the end of ~~/src/HOL/Binomial.thy used
>> to break Codegenerator_Test. I can have a look later to see whether this
>> is still the case.
>>
>> If it is not, we should probably proceed to move some more of René
>> Thiemann et al's efficient code equations from the AFP to the 
>> distribution.
>>
>> I'm glad to see this (hopefully) resolved.
>>
>>
>> Cheers,
>>
>> Manuel
>>
>>
>> On 23/06/16 09:45, Florian Haftmann wrote:
>>> Dear power users of code generation to Scala,
>>>
>>> during the last months there have been some reports on ambiguity
>>> problems with implicits in Scala.
>>>
>>> One kind of these has been known for long and can be addressed in more
>>> recent versions of Scala, which has been done in 7cffe366d333.
>>>
>>> One other kind is presumably resolved with the patch attached,
>>> applicable to b3e5bdb784f5. The key idea is to generate implicits in
>>> Scala (stemming from type class instances) into the respective 
>>> companion
>>> objects of corresponding type classes.
>>>
>>> Since I have no example at hand where such ambiguities have been
>>> observed to happen, I would kindly ask whether someone might try 
>>> whether
>>> that patch resolves the issue. No problems on the visible theory
>>> universe (Isabelle distribution plus AFP) have been encountered.
>>>
>>> The patch still keeps the traditional Scala approach that each implicit
>>> dictionary holds all operations of all super classes. I don't know
>>> whether this is still apt to expose problems, but this could be tackled
>>> in a second step.
>>>
>>> Thanks to Lars Hupel for suggesting these solutions.
>>>
>>> Cheers,
>>>     Florian
>>>
>>>
>>>
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>>>
>>>
>>>