[isabelle-dev] scala-2.12.2

Lars Hupel hupel at in.tum.de
Mon Jun 19 13:38:57 CEST 2017

> 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
> *** 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

More information about the isabelle-dev mailing list