Stream: General

Topic: More Debug Info in Batch Build

view this post on Zulip Qiyuan Xu (Nov 24 2022 at 09:36):

Dear Isabelle players, I am struggling with the batch build command isabelle build. It is true I used heavily ML code that works with locales and contexts, so I think there must be some bug in my code. The thing is, in the interactive GUI mode my theory works well, whereas in the batch build mode, it raises an error with only one line message

*** Bad context for command "." (line 7057 of "~/Current/nu-system-I/Phi_System/Sys.thy")
*** At command "." (line 7057 of "~/Current/nu-system-I/Phi_System/Sys.thy")

The source code looks like

lemma "....."
    some_of_my_proof_commands
    .  (* it fails! it is the last command to finish the lemma.*)

Clearly, I need more infos to debug it. I know there are a lot differences between the batch mode and the interactive mode. So I need to either turn on some option to let the batch mode print more debug info like even stack trace, or, reproduce the problem in the interactive mode where I can have stack trace (maybe I need to turn on some options to simulate the batch mode in the interactive mode, I dunno).

Are there any friends who know how to turn on those features?

view this post on Zulip Qiyuan Xu (Nov 24 2022 at 09:46):

I also sent a copy to the mail list.

Last updated: Dec 21 2024 at 12:33 UTC