[isabelle-dev] Problem in AFP near 16e7d42ef7f4

[Florian Haftmann]

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-dev at 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150625/cf23c3b0/attachment.sig>