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
test.scala.xz
Description: application/xz
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
