isabelle: e1e6bb36b27a tip
afp: be89f13e81c1 tip
> Running Pratt_Certificate ...
> Running Codegen ...
> Running Sturm_Tarski ...
> Running SumSquares ...
> Running pGCL ...
>
> Pratt_Certificate FAILED
> (see also
> /mnt/home/haftmann/data/tum/isabelle/devel/heaps/polyml-5.6_x86-linux/log/Pratt_Certificate)
>
> *** q : prime_factors (p - Suc 0) -->
> *** [a ^ ((p - Suc 0) div q) \<noteq> Suc 0] (mod p) |]
> *** ==> Suc 0 < p
> *** At command "by" (line 478 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/Pratt_Certificate/Pratt_Certificate.thy")
> *** Failed to finish proof (line 424 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/Pratt_Certificate/Pratt_Certificate.thy"):
> *** goal (1 subgoal):
> *** 1. 0 < q
> *** At command "by" (line 424 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/Pratt_Certificate/Pratt_Certificate.thy")
> *** Failed to apply initial proof method (line 394 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/Pratt_Certificate/Pratt_Certificate.thy"):
> *** using this:
> *** prime p
> *** goal (1 subgoal):
> *** 1. ALL q:prime_factors (p - 1). q < p
> *** At command "by" (line 394 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/Pratt_Certificate/Pratt_Certificate.thy")
> *** Failed to apply initial proof method (line 81 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/Pratt_Certificate/Pratt_Certificate.thy"):
> *** using this:
> *** prime p
> *** goal (1 subgoal):
> *** 1. 0 < p
> *** At command "by" (line 81 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/Pratt_Certificate/Pratt_Certificate.thy")
> rmdir: failed to remove '/tmp/isabelle-haftmann57322': Directory not empty
> Finished Codegen (0:00:13 elapsed time, 0:00:34 cpu time, factor 2.61)
>
> SumSquares FAILED
> (see also
> /mnt/home/haftmann/data/tum/isabelle/devel/heaps/polyml-5.6_x86-linux/log/SumSquares)
>
> ### Ignoring duplicate rewrite rule:
> ### (0::?'a1) < ?a1 ^ 2 == ?a1 ~= (0::?'a1)
> ### Ignoring duplicate rewrite rule:
> ### (0::?'a1) < ?a1 ^ 2 == ?a1 ~= (0::?'a1)
> ### Ignoring duplicate rewrite rule:
> ### abs ?a1 ^ 2 == ?a1 ^ 2
> ### Ignoring duplicate rewrite rule:
> ### ?n1 ~= 0 ==> ?a1 ^ ?n1 dvd ?b1 ^ ?n1 == ?a1 dvd ?b1
> ### Ignoring duplicate rewrite rule:
> ### abs ?a1 ^ 2 == ?a1 ^ 2
> ### Ignoring duplicate rewrite rule:
> ### (0::?'a1) <= ?a1 ^ 2 == True
> *** exception Fail raised (line 100 of "PIDE/execution.ML"): Unregistered
> execution: 128
> *** At command "have" (line 419 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/SumSquares/FourSquares.thy")
> *** exception Fail raised (line 100 of "PIDE/execution.ML"): Unregistered
> execution: 128
> *** At command "have" (line 419 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/SumSquares/FourSquares.thy")
> *** Failed to refine any pending goal
> *** At command "show" (line 115 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/SumSquares/FourSquares.thy")
> *** Failed to refine any pending goal
> *** At command "show" (line 79 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/SumSquares/FourSquares.thy")
>
> pGCL FAILED
> (see also
> /mnt/home/haftmann/data/tum/isabelle/devel/heaps/polyml-5.6_x86-linux/log/pGCL)
>
> *** Failed to finish proof (line 252 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/pGCL/Termination.thy"):
> *** goal (1 subgoal):
> *** 1. [| %s. p \<tturnstile> wp body
> *** \<guillemotleft> \<N> G \<guillemotright>;
> *** k <= 1 |]
> *** ==> \<guillemotleft> G \<guillemotright> s * (p * (1 - k) + k)
> *** <= \<guillemotleft> G \<guillemotright> s *
> *** (wp body \<guillemotleft> \<N> G \<guillemotright> s * (1 - k)
> +
> *** k)
> *** At command "by" (line 252 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/pGCL/Termination.thy")
> *** Failed to finish proof (line 355 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/pGCL/WellDefined.thy"):
> *** goal (1 subgoal):
> *** 1. (1 - P s) * (wlp b Q s + wp b R s) \<ominus> 1 - P s =
> *** (1 - P s) * (wlp b Q s + wp b R s \<ominus> 1)
> *** At command "by" (line 355 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/pGCL/WellDefined.thy")
> *** Failed to finish proof (line 116 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/pGCL/Healthiness.thy"):
> *** goal (1 subgoal):
> *** 1. [| nneg Q; bounded_by b Q; healthy (wp g); P s <= 1 |]
> *** ==> 0 <= (1 - P s) * wp g Q s
> *** At command "by" (line 116 of
> "/mnt/home/haftmann/data/tum/afp/devel/thys/pGCL/Healthiness.thy")
> *** Timeout
> Sturm_Tarski FAILED
> (see also
> /mnt/home/haftmann/data/tum/isabelle/devel/heaps/polyml-5.6_x86-linux/log/Sturm_Tarski)
>
> gcd_poly == gcd :: 'a poly => 'a poly => 'a poly
> lcm_poly == lcm :: 'a poly => 'a poly => 'a poly
> ### theory "Polynomial"
> ### 5.233s elapsed time, 16.108s cpu time, 2.976s GC time
> Loading theory "Poly_Deriv"
> ### Rewrite rule not in simpset:
> ### Wellfounded.accp pderiv_rel (pCons ?a1 ?p1)
> ### ==> pderiv (pCons ?a1 ?p1) ==
> ### if ?p1 = 0 then 0 else ?p1 + pCons (0::'a) (pderiv ?p1)
> ### theory "Poly_Deriv"
> ### 0.885s elapsed time, 2.108s cpu time, 0.200s GC time
> Loading theory "PolyMisc" (required by "Sturm_Tarski")
> ### theory "PolyMisc"
> ### 0.795s elapsed time, 2.652s cpu time, 0.204s GC time
> Loading theory "Sturm_Tarski"
> Found termination order: "length <*mlex*> {}"
> ### theory "Sturm_Tarski"
> ### 1.672s elapsed time, 9.880s cpu time, 0.576s GC time
> ### Metis: Unused theorems: "List.list.inject"
> *** Interrupt
> Unfinished session(s): Pratt_Certificate, Sturm_Tarski, SumSquares, pGCL-- 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
