Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code Generation: Error Messages


view this post on Zulip Email Gateway (Aug 18 2022 at 15:24):

From: Tjark Weber <webertj@in.tum.de>
Florian,

Thanks for your recent replies! I have one more observation regarding
the "No code equations for ..." error messages that export_code may
produce -- namely that they can be tedious to hunt down. Getting

*** No code equations for All
*** At command "export_code".

when trying to export code for some top-level constant that depends on
All only through a lengthy chain of dependencies is helpful, but not
really great.

Ideally, I'd like to be able to click on the error message to go to the
corresponding source location. :-) Failing this, a textual
representation of the dependency chain would be nice: e.g.,

*** No code equations for All (required by Foo via Bar via Baz)
*** At command "export_code".

Tjark

view this post on Zulip Email Gateway (Aug 18 2022 at 15:24):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Tjark,

there are a couple of diagnostic devices:

a) code_deps

b) code_thms

c) or even

code_abort All
export_code ...

But an explicit depedency trail would also make sense, and nowadays it
should be not that difficult to accomplish.

Hope this helps,
Florian
signature.asc


Last updated: Mar 28 2024 at 08:18 UTC