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?
I also sent a copy to the mail list.
Last updated: Dec 07 2024 at 16:22 UTC