[isabelle-dev] Problem in AFP near 16e7d42ef7f4

[Larry Paulson]

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.haftmann at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev