Balazs Toth (Aug 26 2026 at 13:43): Balazs Toth (Aug 26 2026 at 13:43):I just did a full afp build and noticed that the two entries "Detour_Calculus" and "Perrons_Formula" don't seem to build. Is that an error on my side or a general issue?
Balazs Toth (Aug 26 2026 at 13:57):Detour_Calculus FAILED (see also "isabelle build_log -H Error Detour_Calculus")
*** Undefined fact: "eqloops_reversepath_cong" (line 1536 of "$AFP/Detour_Calculus/Detour_Calculus.thy")
*** At command "by" (line 1536 of "$AFP/Detour_Calculus/Detour_Calculus.thy")
Unfinished session(s): Detour_Calculus
Finished at Wed Aug 26 15:57:38 GMT+2 2026
0:06:32 elapsed time, 0:31:38 cpu time, factor 4.84
Balazs Toth (Aug 26 2026 at 13:59):Perrons_Formula FAILED (see also "isabelle build_log -H Error Perrons_Formula")
*** Undefined fact: "nat_sum_has_integral_ceiling" (line 314 of "$AFP/Perrons_Formula/Dirichlet_Series_At_I_Infinity_Bound.thy")
*** At command "by" (line 314 of "$AFP/Perrons_Formula/Dirichlet_Series_At_I_Infinity_Bound.thy")
Unfinished session(s): Perrons_Formula
Finished at Wed Aug 26 15:59:26 GMT+2 2026
0:01:11 elapsed time, 0:04:43 cpu time, factor 3.98
Fabian Huch (Aug 31 2026 at 15:21):There was a bad change-set (now backed out by me) in the AFP repository.
Last updated: Sep 15 2026 at 09:19 UTC