[isabelle-dev] scala-2.12.2

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Mon Jun 12 21:15:57 CEST 2017


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.11.8/bin/scalac -encoding UTF-8 -nowarn -target:jvm-1.8 -Xmax-classfile-name 130 -J-Xms128m -J-Xmx1024m -J-Xss2m scala_12.scala
> 
> real	0m59.888s
> user	2m2.836s
> sys	0m0.848s
> 
> + /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
> 
> real	1m55.739s
> user	3m8.200s
> sys	0m0.760s

Surely there is a considerable increase in time resources but no
termination issue at all.

Maybe we should give it another try?

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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/20170612/70caf65c/attachment.sig>


More information about the isabelle-dev mailing list