Stream: Mirror: Isabelle Development Mailing List

Topic: Problems in AFP

Email Gateway (May 02 2025 at 20:30):

From: Florian Haftmann <florian.haftmann@cit.tum.de>

Padic_Ints FAILED (see also "isabelle build_log -H Error Padic_Ints")
*** Failed to finish proof (line 566 of "$AFP/Padic_Ints/Padic_Integers.thy"):
*** goal (1 subgoal):
*** 1. ⟦2 ≤ n; 1 ≤ (2::?'a3) ⟹ (4::?'a3) ≤ (2::?'a3) ^ n⟧
*** ⟹ 4 ≤ 2 ^
*** n
*** At command "by" (line 566 of "$AFP/Padic_Ints/Padic_Integers.thy")

CVP_Hardness FAILED (see also "isabelle build_log -H Error CVP_Hardness")
*** Undefined fact: "linordered_semidom_class.power_mono" (line 320 of "$AFP/CVP_Hardness/CVP_p.thy")
*** At command "by" (line 320 of "$AFP/CVP_Hardness/CVP_p.thy")

Coppersmith_Method FAILED (see also "isabelle build_log -H Error Coppersmith_Method")
*** Undefined fact: "linordered_semidom_class.power_mono" (line 115 of "$AFP/Coppersmith_Method/Howgrave_Graham.thy")
*** At command "by" (line 115 of "$AFP/Coppersmith_Method/Howgrave_Graham.thy")

*** Timeout
Schoenhage_Strassen FAILED (see also "isabelle build_log -H Error Schoenhage_Strassen")

Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Email Gateway (May 02 2025 at 20:32):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
isabelle: 267db8c321c4 tip
afp: 2a810c4dd72c tip

Am 02.05.25 um 22:30 schrieb Florian Haftmann:

Padic_Ints FAILED (see also "isabelle build_log -H Error Padic_Ints")
*** Failed to finish proof (line 566 of "$AFP/Padic_Ints/
Padic_Integers.thy"):
*** goal (1 subgoal):
***  1. ⟦2 ≤ n; 1 ≤ (2::?'a3) ⟹ (4::?'a3) ≤ (2::?'a3) ^ n⟧
***     ⟹ 4 ≤ 2 ^
***            n
*** At command "by" (line 566 of "$AFP/Padic_Ints/Padic_Integers.thy")

CVP_Hardness FAILED (see also "isabelle build_log -H Error CVP_Hardness")
*** Undefined fact: "linordered_semidom_class.power_mono" (line 320 of
"$AFP/CVP_Hardness/CVP_p.thy")
*** At command "by" (line 320 of "$AFP/CVP_Hardness/CVP_p.thy")

Coppersmith_Method FAILED (see also "isabelle build_log -H Error
Coppersmith_Method")
*** Undefined fact: "linordered_semidom_class.power_mono" (line 115 of
"$AFP/Coppersmith_Method/Howgrave_Graham.thy")
*** At command "by" (line 115 of "$AFP/Coppersmith_Method/
Howgrave_Graham.thy")

*** Timeout
Schoenhage_Strassen FAILED (see also "isabelle build_log -H Error
Schoenhage_Strassen")

Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Last updated: May 31 2025 at 01:44 UTC