[isabelle-dev] Problem in AFP
isabelle: 9a4c049f8997 tip afp: af801987e595 tip Running Separation_Logic_Imperative_HOL ... *** Undefined fact: "sum_list_update_nat" (line 598 of "/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy") *** At command "from" (line 598 of "/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy") *** Undefined fact: "sum_list_update_nat" (line 580 of "/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy") *** At command "from" (line 580 of "/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy") *** Undefined fact: "sum_list_update_nat" (line 374 of "/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy") *** At command "from" (line 374 of "/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy") *** Undefined fact: "sum_list_update_nat" (line 356 of "/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy") *** At command "from" (line 356 of "/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy") Unfinished session(s): Separation_Logic_Imperative_HOL 0:02:11 elapsed time, 0:07:54 cpu time, factor 3.62 Florian -- PGP available: http://isabelle.in.tum.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
Re: [isabelle-dev] Problem in AFP near 16e7d42ef7f4
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
[isabelle-dev] Problem in AFP near 16e7d42ef7f4
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 signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Problem in AFP near 16e7d42ef7f4
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
Re: [isabelle-dev] Problem in AFP near 16e7d42ef7f4
Hi Larry,
thanks for finding out so quickly!
Florian
Am 25.06.2015 um 16:02 schrieb Larry Paulson:
This does it nicely (20s):
apply (simp add: T⇩c_def I⇩c_def)
apply clarify
apply (cases u; elim disjE; simp; blast)
Larry
On 25 Jun 2015, at 14:52, Larry Paulson l...@cam.ac.uk wrote:
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
--
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
Re: [isabelle-dev] Problem in AFP near 16e7d42ef7f4
This does it nicely (20s):
apply (simp add: T⇩c_def I⇩c_def)
apply clarify
apply (cases u; elim disjE; simp; blast)
Larry
On 25 Jun 2015, at 14:52, Larry Paulson l...@cam.ac.uk wrote:
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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Problem in AFP/Ordinary_Differential_Equations
isabelle id 9d623cada37f afp id 68e8895167cc Florian -- 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
Re: [isabelle-dev] Problem in AFP/Ordinary_Differential_Equations
solved in afp id 03689082b646 Am Dienstag, den 05.11.2013, 19:09 +0100 schrieb Florian Haftmann: isabelle id 9d623cada37f afp id 68e8895167cc ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
