isabelle: f1b257607981 tip afp: 1a688183b05a tip Any idea what is going on here?
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
Running ConcurrentGC ...
Running MonoBoolTranAlgebra ...
Running Presburger-Automata ...
Running Vickrey_Clarke_Groves ...
MonoBoolTranAlgebra FAILED
(see also /mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.5.3_x86-linux/log/MonoBoolTranAlgebra)
Output written on root.pdf (20 pages, 176819 bytes).
Transcript written on root.log.
*** Failed to apply proof method (line 465 of "/mnt/home/haftmann/data/tum/afp/master/thys/MonoBoolTranAlgebra/Mono_Bool_Tran.thy"):
*** goal (3 subgoals):
*** 1. !!xa. [| ALL xa. x xa <= xa;
*** x : disjunctive.disjunctive op \<squnion> op \<squnion>
*** (%f. f);
*** x \<top> = x xa \<squnion> x (- xa) |]
*** ==> x (- xa) <= \<bottom>
*** 2. !!xa. [| ALL xa. x xa <= xa;
*** x : disjunctive.disjunctive op \<squnion> op \<squnion>
*** (%f. f);
*** x \<top> = x xa \<squnion> x (- xa) |]
*** ==> - xa \<sqinter> xa <= x xa
*** 3. !!xa. [| ALL xa. x xa <= xa;
*** x : disjunctive.disjunctive op \<squnion> op \<squnion>
*** (%f. f) |]
*** ==> x \<top> = x xa \<squnion> x (- xa)
*** At command "apply" (line 465 of "/mnt/home/haftmann/data/tum/afp/master/thys/MonoBoolTranAlgebra/Mono_Bool_Tran.thy")
Vickrey_Clarke_Groves FAILED
(see also /mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.5.3_x86-linux/log/Vickrey_Clarke_Groves)
*** real
*** (setsum
*** (summedBidVector (pseudoAllocation a <| (N <*> finestpart G)) N G) aa)
*** < real
*** (setsum
*** (summedBidVector (pseudoAllocation a <| (N <*> finestpart G)) N G) a)
*** x <= real (card G)
*** 0 <= x
*** (x = 0) = (a = aa)
*** goal (1 subgoal):
*** 1. x <= real (card G) &
*** 0 <= x &
*** (x = 0) = (a = aa) &
*** (aa ~= a -->
*** setsum
*** (summedBidVector (pseudoAllocation a <| (N <*> finestpart G)) N G) aa
*** < setsum
*** (summedBidVector (pseudoAllocation a <| (N <*> finestpart G)) N G)
*** a)
*** At command "by" (line 985 of "/mnt/home/haftmann/data/tum/afp/master/thys/Vickrey_Clarke_Groves/UniformTieBreaking.thy")
*** Timeout
Presburger-Automata FAILED
(see also /mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.5.3_x86-linux/log/Presburger-Automata)
assumes "rquot_DFS A n"
Found termination order: "(%p. size_list size (snd p)) <*mlex*> {}"
Found termination order:
"(%p. size (snd p)) <*mlex*> (%p. size (fst p)) <*mlex*> {}"
### Ignoring duplicate rewrite rule:
### accepts ?tr1 ?P1 ?s1 ?as1 == ?P1 (foldl ?tr1 ?s1 ?as1)
### Legacy feature! Bad case "goal1" (line 3660 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal2" (line 3668 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal3" (line 3672 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal4" (line 3681 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal5" (line 3685 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal6" (line 3689 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal1" (line 4057 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal2" (line 4065 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### theory "Presburger_Automata"
### 21.954s elapsed time, 75.748s cpu time, 14.988s GC time
### Legacy feature! Bad case "goal3" (line 4069 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal4" (line 4078 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal5" (line 4082 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal6" (line 4086 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
/mnt/home/haftmann/data/tum/isabelle/master/lib/scripts/run-polyml-5.5.3: line 100: 56450 Terminated "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" --error-exit < /dev/null
ConcurrentGC FAILED
(see also /mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.5.3_x86-linux/log/ConcurrentGC)
### Rule already declared as safe introduction (intro!)
### r^** a a
### Rule already declared as elimination (elim)
### [| r : W (s p); valid_W_inv s; marked r s ==> PROP W |] ==> PROP W
### Rule already declared as elimination (elim)
### [| r : W (s p); valid_W_inv s; marked r s ==> PROP W |] ==> PROP W
### Rule already declared as elimination (elim)
### [| r : W (s p); valid_W_inv s; marked r s ==> PROP W |] ==> PROP W
### Rule already declared as elimination (elim)
### [| r : W (s p); valid_W_inv s; marked r s ==> PROP W |] ==> PROP W
### Rule already declared as elimination (elim)
### [| r : W (s p); valid_W_inv s; marked r s ==> PROP W |] ==> PROP W
### Rule already declared as elimination (elim)
### [| r : W (s p); valid_W_inv s; marked r s ==> PROP W |] ==> PROP W
### Rule already declared as elimination (elim)
### [| r : W (s p); valid_W_inv s; marked r s ==> PROP W |] ==> PROP W
### Rule already declared as elimination (elim)
### [| r : W (s p); valid_W_inv s; marked r s ==> PROP W |] ==> PROP W
### Rule already declared as elimination (elim)
### [| r : W (s p); valid_W_inv s; marked r s ==> PROP W |] ==> PROP W
Unfinished session(s): ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves
1:56:29 elapsed time, 7:05:28 cpu time, factor 3.65
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
