[isabelle-dev] Datatypes & Isatest failures

[Florian Haftmann]

> It doesn't seem like "subst_tac" had anything to do with it. I still have no idea about what made "HOL-Proofs" slower on "at-poly-e" beween September 13 and 14. The log reveals nothing special, except a truncation at the end. (while processing "Predicate.thy"). My personal inclination would be to disable this test for this platform -- "HOL-Proofs" isn't exactly used by many people, and I'm not sure there's much value in running CPUs for 1 hour each night to test it on some slow hardware and old version of Poly/ML (5.3).
> 
> I see the following options as relatively painless ways of solving this:
> 
> 1. Increase the timeout from 3600 s to, e.g. 4800.

Could be.

> 2. Make "HOL-Proofs" and dependencies "ISABELLE_FULL_TEST".

Definitely not.  HOL-Proofs is am important indicator whether something
got utterly wrong in handling of thm values in Pure.  (Or would you like
JinjaThreads depend on ISABELLE_FULL_TEST also ;-)?)

> 3. Introduce another condition to control whether "HOL-Proofs" should be built.

The pain of introducting another condition seems bigger to me than to
raise the timeout.

> Does anybody have an opinion?

So, (1) is my opinion.

	Florian

-- 

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: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140925/f4f10572/attachment.sig>