Re: [isabelle-dev] scala-2.12.2

> The guys there are talking about Dotty. Do you think it will be also > taken into account by the regular scalac maintainers eventually? Those are Martin Odersky's students, so it's natural that they want to avoid this in Dotty. I'm confident that the scalac team at Lightbend will also have a

Re: [isabelle-dev] scala-2.12.2

> a "StackOverflowError" (in the patmat phase), before I even got a chance > at running this I have investigated this now. It is a regression from Scala 2.11.x to Scala 2.12.x. The offending function is "integer_of_char", which performs a 256-way pattern matching. Maybe this should be

Re: [isabelle-dev] scala-2.12.2

On 22/06/17 14:10, Lars Hupel wrote: >> a "StackOverflowError" (in the patmat phase), before I even got a chance >> at running this > > I have investigated this now. It is a regression from Scala 2.11.x to > Scala 2.12.x. > > The offending function is "integer_of_char", which performs a 256-way

Re: [isabelle-dev] scala-2.12.2

> I took the opportunity to have a look at it and found out it can be done > differently, see attached patch. The patch is now running on testboard: . > The clue about "integer_of_char" is that it had to work regardless > whether HOL chars

Re: [isabelle-dev] scala-2.12.2

> Alternatively, Florian might offer some insight why he set up the code > equations for that particular constant in that way (see "String.thy", > where a ML snippet generates 256 code equations). Note that large > pattern matches on the JVM should be avoided, lest we violate the 64k > method