[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:
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")


Attached is the generated source.


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