I fixed these about two hours ago.
Larry
> On 3 Dec 2015, at 14:56, Florian Haftmann
> <florian.haftm...@informatik.tu-muenchen.de> wrote:
>
> 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
>
> _______________________________________________
> 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
