Re: [isabelle-dev] AFP config files?

2016-06-23 Thread Gerwin Klein
This specific entry currently exists only in devel. Release is clean. Cheers, Gerwin > On 23.06.2016, at 17:54, Lars Hupel wrote: > >> This is my entry. I submitted it a few days ago, and I included the >> config file in my submission. I was not aware that those don't exist

Re: [isabelle-dev] Scala implicits

2016-06-23 Thread Florian Haftmann
> Florian, what are you plans w.r.t. merging this patch into the > distribution? It's currently on the testboard. Florian > > 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

Re: [isabelle-dev] Scala implicits

2016-06-23 Thread 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

Re: [isabelle-dev] Scala implicits

2016-06-23 Thread Manuel Eberl
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

Re: [isabelle-dev] AFP config files?

2016-06-23 Thread Manuel Eberl
This is my entry. I submitted it a few days ago, and I included the config file in my submission. I was not aware that those don't exist anymore. On 23/06/16 09:49, Florian Haftmann wrote: Dear AFP maintainers, in 79fb78da1ef0 there exists exactly one file named "config", namely

Re: [isabelle-dev] Scala implicits

2016-06-23 Thread Manuel Eberl
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

[isabelle-dev] Scala implicits

2016-06-23 Thread Florian Haftmann
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