[isabelle-dev] scala-2.12.2

Makarius makarius at sketis.net
Mon Jun 19 13:33:22 CEST 2017

On 12/06/17 21:15, Florian Haftmann wrote:
> Am 11.06.2017 um 09:01 schrieb Florian Haftmann:
>>> It definitely looks like scala-2.12.2 causes non-termination, e.g. of
>>> src/HOL/Codegenerator_Test/Generate.thy -- I have opened that file in
>>> isabelle jedit and waited for approx. 30min; a batch build of
>>> HOL-Codegenerator_Test ran into timeout of 2h.
>>> Maybe Florian has an idea.
> Unfortunately I cannot reproduce this.
> Starting with a2e441805d6a, I did a
> 	hg backout 94b0da1b242e
> and neither src/HOL/Codegenerator_Test/Generate.thy nor
> src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy exposed
> any problems.
> I took the generated code and ran separate Scala compilations:
>> + /home/haftmann/.isabelle/contrib/scala-2.12.2/bin/scalac -encoding UTF-8 -nowarn -target:jvm-1.8 -Xmax-classfile-name 130 -J-Xms128m -J-Xmx1024m -J-Xss2m scala_12.scala

The scalac part should be OK. The problem is the scala part, i.e. actual
runtime -- presumably the run_cmd here:

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

Attached is the generated source.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.scala.xz
Type: application/x-xz
Size: 98716 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170619/a02299c5/attachment-0002.xz>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170619/a02299c5/attachment.sig>

More information about the isabelle-dev mailing list