Email Gateway (Nov 24 2022 at 13:36): Email Gateway (Nov 24 2022 at 13:36):From: Qiyuan XU ????? <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle players,
Sorry for the interruption again... Guys, I solved the problem.
It is about the 'sort' of keywords. I quote-marked the sort because I don't know the formal name of those "prf_open % proof". I didn't find any documentation about this...
The following code is more readable on zulip https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/.E2.9C.94.20More.20Debug.20Info.20in.20Batch.20Build
Wrong:
theory Thy
keywords "❴" "❵" :: prf_decl % "proof"
Correct:
theory Thy
keywords "❴" :: prf_open % "proof"
and "❵" :: prf_goal % "proof"
The place where my code goes wrong:
lemma "...."
❴
...
❵
. (* here it goes wrong! *)
Command "❵" is some magic defined by myself, and I didn't know what the keyword sort does. So I mimicked other commands and wrote "prf_decl % proof". It works in the interactive mode, but it seems the batch mode checks more about the outer syntax of Isar. The thing is the command "❵" generates some proof obligations and the usage in my theory is like ❵ by methods. However, keyword sort "prf_decl % proof" is not for appending a proof script like this, so it fails in the syntax check and what Isar wanted to tell me is actually that the command "." (corresponding to "by methods" here) is used at the wrong place.
After I corrected the sort to be prf_goal % "proof" which is expected to be followed by a proof script. The syntax check is passed and then everything works.
Again... I really hope for more documentation about the system. Isabelle/Isar is really great art and a complicated video game... I really enjoy it! again!
Sincerely
Qiyuan Xu
发件人: Qiyuan XU ?????
发送时间: 2022年11月24日 17:51
收件人: cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
主题: More Debug Info in Batch Build
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 ...)
*** At command "." (line 7057 of ...)
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 options 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).
Is there anybody who knows how to turn on those features?
Best Regards
Qiyuan Xu
CONFIDENTIALITY: This email is intended solely for the person(s) named and may be confidential and/or privileged. If you are not the intended recipient, please delete it, notify us and do not copy, use, or disclose its contents.
Towards a sustainable earth: Print only when necessary. Thank you.
Email Gateway (Nov 25 2022 at 15:44):From: Qiyuan XU ????? <cl-isabelle-users@lists.cam.ac.uk>
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 ...)
*** At command "." (line 7057 of ...)
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 options 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).
Is there anybody who knows how to turn on those features?
Best Regards
Qiyuan Xu
CONFIDENTIALITY: This email is intended solely for the person(s) named and may be confidential and/or privileged. If you are not the intended recipient, please delete it, notify us and do not copy, use, or disclose its contents.
Towards a sustainable earth: Print only when necessary. Thank you.
Email Gateway (Nov 25 2022 at 20:57):From: Makarius <makarius@sketis.net>
On 24/11/2022 14:35, Qiyuan XU ????? (via cl-isabelle-users Mailing List) wrote:
It is about the 'sort' of keywords. I quote-marked the sort because I don't
know the formal name of those "prf_open % proof". I didn't find any
documentation about this...
That 'sort' of a command keyword is actually called 'kind': you can see this
in the ML and Scala sources, which are the primary documentation.
It is a running gag of Isabelle history that command kinds are not very
well-defined: the meaning fluctuates according to the gradual change of the
language structure and meaning, and the front-ends. The concept was first
introduced for Proof General Emacs, approx. 1998.
For theory commands and diagnostic commands it is usually sufficient to
imitate examples: there are not so many possibilities.
For proof commands the situation is much more complex, but strictly speaking
this is not a regular programming interface anyway: the Isar proof language is
given as is, it is one of the rare spots in Isabelle that are not open for
add-ons by the user.
Correct:isabelle
theory Thy
keywords "❴" :: prf_open % "proof"
and "❵" :: prf_goal % "proof"
```
Command "❵" is some magic defined by myself, and I didn't know what the
keyword sort does.
I doubt that this is going to work at all. Proof blocks and nested proofs need
to be properly balanced. Both "prf_open" and "prf_goal" are an "open", but of
a different kind.
Can you say what you intend to do? What is the application?
Again... I really hope for more documentation about the system. Isabelle/Isar
is really great art and a complicated video game... I really enjoy it! again!
It is certainly and art and a game. But new Isar proof commands are difficult
to introduce: for me as the language designer it usually takes years to add
something that makes sense.
Makarius
Last updated: Apr 24 2024 at 12:33 UTC