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:
>> <https://ci.isabelle.systems/jenkins/job/isabelle-repo-makeall/912/consoleFull>.
>> (I had tested it with testboard before anyway.)
>>
>
> OK, I will look more closely again.
I have tried 18f5014331a1 again where scala-2.12.2 was still active,
while in 94b0da1b242e it is back to scala-2.11.8.
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.
> There are some other problems with Windows: some of this already works
> in e896db33d4ce, but it is not yet finished.
This is an independent problem from long ago, when Poly/ML switched from
Cygwin to native MinGW. With Isabelle/8411f1a2272c
HOL-Codegenerator_Test should work on Windows.
In Isabelle/6181ccb4ec8c, I have even activated ISABELLE_GHC, although
that causes somewhat erratic results in HOL-Quickcheck_Examples.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
