search

albertqjiang / draft_sketch_prove

Other
61 stars 8 forks source link

Questions about working with Isabelle #2

Open jc5201 opened 1 year ago

jc5201 commented 1 year ago

Hello, Thank you for sharing your code and I'm very pleased to have a starting point! I'm struggling for debugging this repo, so I have some questions.

1. The communication with isabelle (through pisa client) is hard to understand because there are no manual or references. For example, I can't understand what or means... Is there any material about api or commands?

  1. The pisa environment is initialized with working_directory_path and theory_file_path (or starter_string?). For similar reason with the first question, I can't even guess how the messages work (IsaPath, IsaContext, ...). What is the purpose of working_directory and theory_file_path?

  2. What is normalhammer? I can't find anything with google search.

-- For more about my environment, I'm trying to reproduce this with Isabelle 2022. In afp version (https://foss.heptapod.net/isa-afp/afp-2022) I use, there is no file named Interactive.thy, so I replaced it with another thy file.

If you feel this issue is more related to (https://github.com/albertqjiang/Portal-to-ISAbelle), please let me know.

albertqjiang commented 1 year ago

Hi!

Sorry about the late reply. I was swamped with ICLR stuff.

Please see Sean's repo: https://github.com/wellecks/ntptutorial/tree/main/partII_dsp for a step-by-step tutorial.

I will have a major update to Portal-to-Isabelle soon and will add more details.

Best, Albert

jc5201 commented 1 year ago

Thanks for your reply. I checked the helpful materials and now I'm also checking PISA and scala-isabelle codes. It would be helpful if your update (for PISA) include some documentations!