I took a look, and it all runs perfectly well, except here: show "xs ∈ T⇩c ∧ ys ∈ T⇩c ∧ ipurge_tr_rev I⇩c id u xs = ipurge_tr_rev I⇩c id u ys ⟶ {x. u = x ∧ xs @ [x] ∈ T⇩c} = {x. u = x ∧ ys @ [x] ∈ T⇩c}" (* The following proof step performs an exhaustive case distinction over all traces and domains, and then can take long to be completed. *) by (simp add: T⇩c_def I⇩c_def, rule impI, (erule conjE)+, cases u, (((erule disjE)+)?, simp, blast?)+)
The comment doesn’t tell us whether to wait minutes or hours. Clearly this is a fragile step. Any sort of change could break this. Larry > On 25 Jun 2015, at 14:00, Florian Haftmann > <florian.haftm...@informatik.tu-muenchen.de> wrote: > > 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 > > -- > > PGP available: > http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev