Maybe this is hitting the concrete wall set by hardware constraints. I am building on lxbroy10; relevant settings might include
> ISABELLE_BUILD_JAVA_OPTIONS=-Xmx4096m -Xss2m
> ISABELLE_PLATFORM32=x86-linux
> ISABELLE_JAVA_SYSTEM_OPTIONS=-server -Dfile.encoding=UTF-8
> -Disabelle.threads=0
> ISABELLE_PLATFORM64=x86_64-linux
> ISABELLE_PLATFORM=x86-linux
> ISABELLE_SCALA_BUILD_OPTIONS=-encoding UTF-8 -nowarn -target:jvm-1.7
> -Xmax-classfile-name 130
In my view lxbroy10 still has some status as a reference machine, and I
am seriously concerned as soon as resources appear to be too tiny there.
Anybody else experiencing similar problems?
Florian
Am 25.06.2015 um 15:00 schrieb Florian Haftmann:
> isabelle: 19c277ea65ae tip
> afp: 16e7d42ef7f4 tip
>
> Running Noninterference_Generic_Unwinding ...
> *** Timeout
> Noninterference_Generic_Unwinding FAILED
> (see also
> /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/Noninterference_Generic_Unwinding)
>
> val it = (): unit
> Loading theory "GenericUnwinding"
> Proofs for inductive predicate(s) "rel_induct_auxp"
> Proving monotonicity ...
> Proving the introduction rules ...
> Proving the elimination rules ...
> Proving the induction rule ...
> Proving the simplification rules ...
> ### theory "GenericUnwinding"
> ### 1.941s elapsed time, 11.008s cpu time, 0.136s GC time
>
> Any hints what could have gone wrong?
>
> Florian
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
