[isabelle-dev] scala-2.12.2

[Lars Hupel]

> The scalac part should be OK. The problem is the scala part, i.e. actual
> runtime -- presumably the run_cmd here:
> http://isabelle.in.tum.de/repos/isabelle/annotate/20304512a33b/src/HOL/Library/code_test.ML#l562
> 
> I've just made a quick test of HOL-Codegenerator_Test on lxbroy10: it
> leads to a very long running java process. Killing that produces the
> following error:
> 
> *** Code check failed for Scala: isabelle_scala scalac
> $ISABELLE_SCALAC_OPTIONS ROOT.scala
> *** At command "export_code" (line 18 of
> "~~/src/HOL/Codegenerator_Test/Generate.thy")

Very curious, for multiple reasons:

- testboard is supposed to run Scala as well (I'll need to double check
that that's the case)
- the code check error message explicitly talks about "scalac"
- I just unpacked the attachment you sent and, with scalac 2.12.2 I get
a "StackOverflowError" (in the patmat phase), before I even got a chance
at running this