[isabelle-dev] Build problems in AFP

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20151203/d51c0715/attachment.asc>