[isabelle-dev] scala-2.12.2

[Lars Hupel]

> 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 look,
but we should give them a couple of days.

> Alternatively, if Florian has an idea for a workaround it is also fine.

I'm still not quite sure about the impact of this.

If I manually increase the stack size (-Xss), as is done in
ISABELLE_SCALAC_OPTIONS, the problem goes away (even for the full
"test.scala" file). This would explain why the problem didn't manifest
itself in the testboard. However, I'm not sure if we should expect users
of code generation to invoke compilers with specific options.

Regardless, this is clearly a regression in Scala.

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 length limit in class files ("integer_of_char" currently requires
58044 bytes).