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.


Attachment: test.scala.xz
Description: application/xz

Attachment: signature.asc
Description: OpenPGP digital signature

isabelle-dev mailing list

Reply via email to