Katherine Kosaian (Nov 03 2023 at 13:33): Katherine Kosaian (Nov 03 2023 at 13:33):Hi all, I have a relatively large proof goal that is easily proved ("blast", "metis", "meson", "fast" all solve it). However, when running Sledgehammer, the attached warnings were generated.
Screenshot-2023-11-03-at-7.46.08-AM.png
This warning disappears as soon as I input a proof. This is in the context of a larger development and I have not attempted to generate a minimal example; I expect part of the problem is that the subgoal in question is quite large (it contains many abbreviations which, when expanded, generate large terms). However, I am unsure what would be causing the "bad name binding" warning and whether there is anything I should fix. Any thoughts on what might be underlying this are appreciated!
Yutaka Nagashima (Nov 05 2023 at 23:57):Dear @Katherine Kosaian ,
I apologize, but I don't have a direct answer to your question. However, after examining the screenshot you provided, I wonder if you're trying to suppress the Tracing paused message.
I've previously been bothered by such messages and found a way to suppress them. You might find this link useful:
https://github.com/data61/PSL#hints
Regarding your specific issue, I'm not entirely well-versed in this area. Still, it seems the warning might originate from Line 190 of src/Pure/General/binding.ML. Perhaps you could review how names like #l_lift2 are generated and adjust the naming scheme to ensure compatibility with Symbol_Pos.is_identifier?
Best regards,
Yutaka
Katherine Kosaian (Nov 17 2023 at 21:17):Thank you so much, these are helpful pointers!!
Last updated: Apr 28 2024 at 12:28 UTC