[isabelle-dev] Build problems in AFP

[Lawrence Paulson]

I fixed these about two hours ago.
Larry

> On 3 Dec 2015, at 14:56, Florian Haftmann <florian.haftmann at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev