Stream: Mirror: Isabelle Development Mailing List

Topic: Failure of AFP/Go_Test_Slow

Email Gateway (Jan 31 2025 at 18:00):

From: Makarius <makarius@sketis.net>
After running "isabelle go_setup" it is possible to run test with
"condition=ISABELLE_GOEXE" manually. This produces the following failure:

Go_Test_Slow FAILED (see also "isabelle build_log -H Error Go_Test_Slow")
*** Unknown statement name: "Code_Numeral.Neg"
*** At command "export_code" (line 12 of
"$AFP/Go/test/slow/Generate_Binary_Nat.thy")
*** Unknown statement name: "Code_Numeral.Neg"
*** At command "export_code" (line 19 of "$AFP/Go/test/slow/Generate.thy")

Any clues?

This is Isabelle/9601f5582f33 + AFP/26bfca109e32.

Makarius

Email Gateway (Jan 31 2025 at 19:18):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
See now
https://foss.heptapod.net/isa-afp/afp-devel/-/commit/b1295207946a90e2c347c43f08518f4e222ac7d3

After so many years of unnoticed accumulation of various ambitious code
generation extensions over the AFP, some rearrangement of elementary
material in the distribution raise this now to the surface.

Cheers,
Florian

Am 31.01.25 um 18:59 schrieb Makarius:

After running "isabelle go_setup" it is possible to run test with
"condition=ISABELLE_GOEXE" manually. This produces the following failure:

Go_Test_Slow FAILED (see also "isabelle build_log -H Error Go_Test_Slow")
*** Unknown statement name: "Code_Numeral.Neg"
*** At command "export_code" (line 12 of "$AFP/Go/test/slow/
Generate_Binary_Nat.thy")
*** Unknown statement name: "Code_Numeral.Neg"
*** At command "export_code" (line 19 of "$AFP/Go/test/slow/Generate.thy")

Any clues?

This is Isabelle/9601f5582f33 + AFP/26bfca109e32.

Makarius

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Email Gateway (Jan 31 2025 at 22:38):

From: Makarius <makarius@sketis.net>
On 31/01/2025 20:18, Florian Haftmann wrote:

See now https://foss.heptapod.net/isa-afp/afp-devel/-/commit/
b1295207946a90e2c347c43f08518f4e222ac7d3

Great.

Makarius

Last updated: Feb 01 2025 at 20:19 UTC