Re: [isabelle-dev] scala-2.12.2

On 24/06/17 21:08, Florian Haftmann wrote: > See now finally http://isabelle.in.tum.de/repos/isabelle/rev/a41435469559 Great. In Isabelle/d91108ba9474 we are also back to scala-2.12.2 and can hopefully keep it this time. Makarius signature.asc Description: OpenPGP digital signature __

Re: [isabelle-dev] scala-2.12.2

See now finally http://isabelle.in.tum.de/repos/isabelle/rev/a41435469559 Florian Am 23.06.2017 um 08:43 schrieb Lars Hupel: >> The patch is now running on testboard: >> . > > Unfortunately, this patch did not work out. > > 22:13:3

Re: [isabelle-dev] scala-2.12.2

> The patch is now running on testboard: > . Unfortunately, this patch did not work out. 22:13:39 *** Failed to finish proof (line 62 of "~~/src/HOL/Library/Code_Target_Nat.thy"): 22:13:39 *** goal (1 subgoal): 22:13:39 *** 1. Transfer.Rel

Re: [isabelle-dev] scala-2.12.2

> I took the opportunity to have a look at it and found out it can be done > differently, see attached patch. The patch is now running on testboard: . > The clue about "integer_of_char" is that it had to work regardless > whether HOL chars a

Re: [isabelle-dev] scala-2.12.2

> Alternatively, Florian might offer some insight why he set up the code > equations for that particular constant in that way (see "String.thy", > where a ML snippet generates 256 code equations). Note that large > pattern matches on the JVM should be avoided, lest we violate the 64k > method lengt

Re: [isabelle-dev] scala-2.12.2

> The guys there are talking about Dotty. Do you think it will be also > taken into account by the regular scalac maintainers eventually? Those are Martin Odersky's students, so it's natural that they want to avoid this in Dotty. I'm confident that the scalac team at Lightbend will also have a lo

Re: [isabelle-dev] scala-2.12.2

On 22/06/17 14:10, Lars Hupel wrote: >> a "StackOverflowError" (in the patmat phase), before I even got a chance >> at running this > > I have investigated this now. It is a regression from Scala 2.11.x to > Scala 2.12.x. > > The offending function is "integer_of_char", which performs a 256-way >

Re: [isabelle-dev] scala-2.12.2

> a "StackOverflowError" (in the patmat phase), before I even got a chance > at running this I have investigated this now. It is a regression from Scala 2.11.x to Scala 2.12.x. The offending function is "integer_of_char", which performs a 256-way pattern matching. Maybe this should be implemented

Re: [isabelle-dev] scala-2.12.2

On 19/06/17 14:16, Makarius wrote: > On 19/06/17 13:38, Lars Hupel wrote: > >> - I just unpacked the attachment you sent and, with scalac 2.12.2 I get >> a "StackOverflowError" (in the patmat phase), before I even got a chance >> at running this > > I have started to experiment with that, and ran

Re: [isabelle-dev] scala-2.12.2

On 19/06/17 13:38, Lars Hupel wrote: >> 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.sca

Re: [isabelle-dev] scala-2.12.2

> 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

Re: [isabelle-dev] scala-2.12.2

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

Re: [isabelle-dev] scala-2.12.2

> I've just pushed the inverse patch of 94b0da1b242e to testboard, so > we'll see. > > HOL-Codegenerator_Test runs fine (0:14:41 elapsed time). Cheers Lars ___ isabelle-dev mailing list isabelle-

Re: [isabelle-dev] scala-2.12.2

> Maybe we should give it another try? I've just pushed the inverse patch of 94b0da1b242e to testboard, so we'll see. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mail

Re: [isabelle-dev] scala-2.12.2

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 time

Re: [isabelle-dev] scala-2.12.2

> 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. Btw. I am

Re: [isabelle-dev] scala-2.12.2

On 22/05/17 15:16, Makarius wrote: > On 22/05/17 13:12, Lars Hupel wrote: >>> After your change d76937b773d9, I still see a non-terminating >>> HOL-Codegenerator_Test. So in 94b0da1b242e I have switched back to >>> scala-2.11.8. >> >> Interesting. In Jenkins, this commit builds fine: >>

Re: [isabelle-dev] scala-2.12.2

On 22/05/17 13:12, Lars Hupel wrote: >> After your change d76937b773d9, I still see a non-terminating >> HOL-Codegenerator_Test. So in 94b0da1b242e I have switched back to >> scala-2.11.8. > > Interesting. In Jenkins, this commit builds fine: >

Re: [isabelle-dev] scala-2.12.2

> After your change d76937b773d9, I still see a non-terminating > HOL-Codegenerator_Test. So in 94b0da1b242e I have switched back to > scala-2.11.8. Interesting. In Jenkins, this commit builds fine: . (I had tested it w

Re: [isabelle-dev] scala-2.12.2

On 21/05/17 13:56, Lars Hupel wrote: >> With Isabelle/a43a079156a6 we are on scala-2.12.2, leaving the 2.11.x >> behind. > > See also Isabelle/d76937b773d9, which repairs a broken code adaptation. > Note that `error` had been deprecated for at least one major release cycle. Thanks for keeping an

Re: [isabelle-dev] scala-2.12.2

> With Isabelle/a43a079156a6 we are on scala-2.12.2, leaving the 2.11.x > behind. See also Isabelle/d76937b773d9, which repairs a broken code adaptation. Note that `error` had been deprecated for at least one major release cycle. Maybe we should start performing code checks with stricter compile