Chengsong Tan (May 07 2024 at 00:20): Chengsong Tan (May 07 2024 at 00:20):To achieve the effect of being able to call sledgehammer from anywhere (not just jedit), #narrow/stream/202961-General/topic/tools.20to.20automatically.20adopt.20sledgehammer.20proofs.20into.20theory
I have been investigationg the code in sledgehammer_commands.ML, which seems to be the place where the core functionalities of sledgehammer is placed. It seems that the command is defined as the following function:
val _ =
Outer_Syntax.command \<^command_keyword>\<open>sledgehammer_params\<close>
"set and display the default parameters for Sledgehammer"
(parse_raw_params >> (fn params =>
Toplevel.theory (fold set_default_raw_param params #> tap (fn thy =>
writeln ("Default parameters for Sledgehammer:\n" ^
(case rev (default_raw_params thy) of
[] => "none"
| params => params |> map string_of_raw_param |> sort_strings |> cat_lines))))))
I checked and found that the
(val _ =).... (parse_raw_params >> (fn params =>
Toplevel.theory (fold set_default_raw_param params #> tap (fn thy =>
writeln ("Default parameters for Sledgehammer:\n" ^
(case rev (default_raw_params thy) of
[] => "none"
| params => params |> map string_of_raw_param |> sort_strings |> cat_lines))))))
bit (excluding the first two lines) is of type
fn: Token.T list -> (Toplevel.transition -> Toplevel.transition) * Token.T list.
I was wondering:
1) how to invoke this function properly to trigger the same effect of sledgehammering at a certain position in a lemma. Suppose we have a lemma
lemma foo: "P ==> Q ==> P /\ Q"
(*pos 1 *)
sorry
Then what arguments should I construct to feed to the function of type fn: Token.T list -> (Toplevel.transition -> Toplevel.transition) * Token.T list (or perhaps the hammer_away function to achieve the same effect as calling sledgehammer at position 1?
Thanks a lot,
Chengsong
Yutaka Nagashima (May 07 2024 at 01:24):Hi @Chengsong Tan ,
I applied Sledgehammer on Proof.state by writing this function:
https://github.com/data61/PSL/blob/2eeb751cde35a2b40b1dc746e64f6764efa8daa8/PSL/Subtool.ML#L171
Probably, the ML function you are looking for is Sledgehammer.run_sledgehammer, which I am using in this line:
https://github.com/data61/PSL/blob/2eeb751cde35a2b40b1dc746e64f6764efa8daa8/PSL/Subtool.ML#L183
To call run_sledgehammer from the Isar interface, you need to wrap the function call to run_sledgehammer by a function from Toplevel.transition to Toplevel.transition.
I did this in this function: https://github.com/data61/PSL/blob/2eeb751cde35a2b40b1dc746e64f6764efa8daa8/PSL/Isar_Interface.ML#L106
Initially, it may be confusing a little, but I believe this is Dr. Wenzel's good engineering work to introduce parallelism to Isabelle/jEdit.
I found it useful to incorporate Sledgehammer into a larger automation. :octopus:
In particular, it serves as a helpful tool for generating conjectures.
Many of the proofs in this video were generated by Sledgehammer. :hammer:
Chengsong Tan (May 07 2024 at 17:41):Yutaka Nagashima said:
Hi Chengsong Tan ,
I applied Sledgehammer on Proof.state by writing this function:
https://github.com/data61/PSL/blob/2eeb751cde35a2b40b1dc746e64f6764efa8daa8/PSL/Subtool.ML#L171Probably, the ML function you are looking for is
Sledgehammer.run_sledgehammer, which I am using in this line:
https://github.com/data61/PSL/blob/2eeb751cde35a2b40b1dc746e64f6764efa8daa8/PSL/Subtool.ML#L183To call
run_sledgehammerfrom the Isar interface, you need to wrap the function call torun_sledgehammerby a function fromToplevel.transitiontoToplevel.transition.I did this in this function: https://github.com/data61/PSL/blob/2eeb751cde35a2b40b1dc746e64f6764efa8daa8/PSL/Isar_Interface.ML#L106
Initially, it may be confusing a little, but I believe this is Dr. Wenzel's good engineering work to introduce parallelism to Isabelle/jEdit.
I found it useful to incorporate Sledgehammer into a larger automation. :octopus:
In particular, it serves as a helpful tool for generating conjectures.Many of the proofs in this video were generated by Sledgehammer. :hammer:
Hi @Yutaka Nagashima ,
Thank you very much for the helpful information!
This project looks so cool, I have always wanted a tool like this.
It's very helpful for me to know that to call sledgehammer from within Isar proofs is different from calling them outside Isar environment.
Suppose I want to hack your code to fulfill my task of generating sledgehammer one-liners automatically (and redirecting them) to store them in a file. Which files and functions should I touch on?
Best wishes,
Chengsong
Yutaka Nagashima (May 12 2024 at 23:35):Chengsong Tan said:
So a basic question for hacking your code base: if I want to redirect your
find_proofmethod output to a file (or std output), what are the minimal changes that needs to be done?Best wishes,
Chengsong
Hi @Chengsong Tan ,
I'm not skilled at I/O operations, but this might be helpful:
theory Chengsong
imports Main
begin
ML‹
fun write_string_in_file thy file_name sh_output =
let
val path_to_directory = Resources.master_directory thy |> File.platform_path: string;
val path_to_file = path_to_directory ^ "/" ^ file_name;
val outstream = TextIO.openAppend path_to_file: TextIO.outstream;
val _ = TextIO.outputSubstr (outstream, Substring.full sh_output);
val _ = TextIO.flushOut outstream;
val _ = TextIO.closeOut outstream;
in
()
end;
›
ML‹
write_string_in_file @{theory} "sh_out.txt" "0\n";
write_string_in_file @{theory} "sh_out.txt" "1\n";
write_string_in_file @{theory} "sh_out.txt" "2\n";
›
end
On my machine, I inserted the definition of write_string_in_file and the following code between lines 136 and 137 of Abduction.thy:
val _ = write_string_in_file (Proof_Context.theory_of cxtx_wo_verbose_warnings) "sh_output.txt" message;
And this recorded the result of the Abduction Prover in sh_output.txt.
Note that for large-scale experiments, careful consideration of concurrency issues is essential."
Regards,
Yutaka
Yutaka Nagashima (May 12 2024 at 23:37):Ah, I just noticed that Dr. Wenzel is also offering advice on the mailing list. :smile:
Chengsong Tan (May 13 2024 at 08:37):Yutaka Nagashima said:
Chengsong Tan said:
So a basic question for hacking your code base: if I want to redirect your
find_proofmethod output to a file (or std output), what are the minimal changes that needs to be done?Best wishes,
ChengsongHi Chengsong Tan ,
I'm not skilled at I/O operations, but this might be helpful:
theory Chengsong imports Main begin ML‹ fun write_string_in_file thy file_name sh_output = let val path_to_directory = Resources.master_directory thy |> File.platform_path: string; val path_to_file = path_to_directory ^ "/" ^ file_name; val outstream = TextIO.openAppend path_to_file: TextIO.outstream; val _ = TextIO.outputSubstr (outstream, Substring.full sh_output); val _ = TextIO.flushOut outstream; val _ = TextIO.closeOut outstream; in () end; › ML‹ write_string_in_file @{theory} "sh_out.txt" "0\n"; write_string_in_file @{theory} "sh_out.txt" "1\n"; write_string_in_file @{theory} "sh_out.txt" "2\n"; › endOn my machine, I inserted the definition of
write_string_in_fileand the following code between lines 136 and 137 of Abduction.thy:
val _ = write_string_in_file (Proof_Context.theory_of cxtx_wo_verbose_warnings) "sh_output.txt" message;And this recorded the result of the Abduction Prover in
sh_output.txt.
Note that for large-scale experiments, careful consideration of concurrency issues is essential."Regards,
Yutaka
Hi @Yutaka Nagashima ,
Thank you very much for taking the time to write the functions and replying!
I have been experimenting with redirection and came up with a somewhat similar approach as you have (done to sledgehammer but same idea):
val _ =
Outer_Syntax.command \<^command_keyword>‹sledgehammer›
"search for first-order proof using automatic theorem provers"
(Scan.optional Parse.name runN -- parse_raw_params
-- parse_fact_override -- Scan.option Parse.nat >>
(fn (((subcommand, params), fact_override), opt_i) =>
Toplevel.keep_proof
(hammer_away params (SOME (writeFileln "test2.txt")) subcommand opt_i fact_override o Toplevel.proof_of)))
I have replaced the NONE in the last line in the original code to SOME (writeFileln ...), which switches the output to file rather than proof panel.
The writeFileln function is defined as follows:
fun print_string_op NONE = "NoID"
| print_string_op (SOME s) = s
fun writeFileln filename content =
let val fd = TextIO.openAppend filename
val _ = TextIO.output (fd, String.concat [print_string_op (Position.id_of (Position.thread_data ())), content, "\n"]) handle e => (TextIO.closeOut fd; raise e)
val _ = TextIO.closeOut fd
in () end
However, I am now facing the issue of plugging the generated proof back into the original thy file. In the above function if you try to print also the line number info via Position.line_of, sometimes (or in my case, always) no line number is found, and only the thread id can be retrieved via Position.id_of. This makes it hard to insert the proof found back into the place precisely. I have been working on two solutions for this:
id to its source text. This should be possible, as the sendback markup inserts to the right position once it has been clicked (or maybe not? It relies on the user putting the cursor at the right place)find_proof calls exist. Based on the relative order in which find_proof keyword appears in text, insert each proof with the right label back.Method 1 might not work, method 2 is simple conceptually but can be quite fragile (commented keyword etc.)
Yutaka Nagashima said:
Ah, I just noticed that Dr. Wenzel is also offering advice on the mailing list. :smile:
Yes, he is quite helpful in pointing me to functions like Position.thread_data()! But he also told me it was not always possible to get the line number info :(
Yutaka Nagashima (May 13 2024 at 20:53):Hi @Chengsong Tan ,
If I remember correctly, I used Position.line_of to get the line number back in 2018 when extracting training data from the AFP for PaMpeR. I also remotely recall that the behavior of this function changes depending on whether you use Isabelle in interactive mode or batch mode.
In interactive mode, it provides information related to the timing of your edits, while in batch mode, it returns the line number.
Regarding the two approaches you listed, I am somewhat inclined towards the second solution. As you mentioned, it might not be the most elegant solution, but it works similarly to Mirabelle, if I understand correctly.
However, the effectiveness of this choice depends on the goals of your project, which I am not aware of. Perhaps there is a third option, depending on what you ultimately aim to achieve by inserting proof scripts into theory files. :smile:
Regards,
Yutaka
Chengsong Tan (May 13 2024 at 23:47):bit
Yutaka Nagashima said:
Hi Chengsong Tan ,
If I remember correctly, I used
Position.line_ofto get the line number back in 2018 when extracting training data from the AFP for PaMpeR. I also remotely recall that the behavior of this function changes depending on whether you use Isabelle in interactive mode or batch mode.In interactive mode, it provides information related to the timing of your edits, while in batch mode, it returns the line number.
Regarding the two approaches you listed, I am somewhat inclined towards the second solution. As you mentioned, it might not be the most elegant solution, but it works similarly to Mirabelle, if I understand correctly.
However, the effectiveness of this choice depends on the goals of your project, which I am not aware of. Perhaps there is a third option, depending on what you ultimately aim to achieve by inserting proof scripts into theory files. :smile:
Regards,
Yutaka
Hi @Yutaka Nagashima ,
It's very important to know that line_of is actually usable! Thanks a lot!
How to do the redirection also for the try_hard command?
I have looked into the code and it seems the get_trans_trans function in Isar_Interface.ML is where messages are being printed to the proof panel. However I am not sure how to extract the proof text from the print variable there as it is not of string type. I also tried to modify print_proof_of_graphto output to file, but that function seems to not have been called. Any ideas?
Best wishes,
Chengsong
Chengsong Tan (May 14 2024 at 00:24):I realized that the print_necessary_proofs_only function seems to be what I need. :)
Chengsong Tan (May 14 2024 at 16:31):Ok so get_trans_trans does produce proofs in string format. Problem solved. Apologies for the additional messages.
Out of curiosity, I was playing with your tool and I notice that sometimes the same proof seems to be generated multiple times, as can be seen from the output of mk_apply_script. Can this be avoided? Perhaps this could be a potential performance optimisation for the abduction prover?
Yutaka Nagashima (May 14 2024 at 22:30):Can you share a screenshot to demonstrate the duplication problem?
Chengsong Tan (May 16 2024 at 22:02):Yutaka Nagashima said:
Can you share a screenshot to demonstrate the duplication problem?
Yes,
Screenshot-2024-05-16-at-22.56.31.png
I have put the line 1304 in the picture in Util.ML to output to a file, and it seems the same proof text has been generated multiple times here for the same thread.
I will reproduce this sometime later and send to you (now the file is not modified for my current experiment.).
Chengsong Tan (May 16 2024 at 22:08):Hi @Yutaka Nagashima
I was wondering what's the most powerful command in your tool?
the proof methods find_proof Hammer and try_hard are already quite good.
But I was wondering if there exists any more extensive/powerful commands in the abduction prover that can be given to the machine to try out for long duration of time. My proof does not involve a lot of induction.
Thanks a lot,
Chengsong
Last updated: Dec 21 2024 at 12:33 UTC