Email Gateway (Aug 18 2022 at 15:24): 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
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: Nov 21 2024 at 12:39 UTC