Chengsong Tan (May 07 2024 at 18:42): Chengsong Tan (May 07 2024 at 18:42):Perhaps a minimal solution to the core of the question above, can we redirect the one-liner proofs outputted by sledgehammer to a file while jedit/isabelle build session tools are checking the file?
Mathias Fleury (May 08 2024 at 06:01):try mirabelle
Mathias Fleury (May 08 2024 at 06:02):that prints a log file with that information (except that you do not even need to have sledgehammer calls, it will run every goal with sledgehammer)
Chengsong Tan (May 08 2024 at 08:03):Mathias Fleury said:
try mirabelle
Hi Mathias,
Have you used mirabelle? Does it accept thy files at all (rather than session names)?
I have tried using
isabelle mirabelle -O output \
-A "slegehammer[provers = cvc4, timeout = 30]" \
-T myTheoryName
with or without the .thy extension for myTheoryName, but I always got
Building required heaps ...
### Nothing to build
Running Mirabelle on Isabelle/007e6af8a020 (Isabelle2024-RC3)...
### Nothing to build
0:00:01 elapsed time
Is there anything I am missing? The relevant chapter in the manual does not help as its examples always assumes the existence of an AFP session, like this:
isabelle mirabelle -d $AFP -O output \
-T Semantics -T Compiler \
-A "sledgehammer[prover=e, prover_timeout=30]" \
VeriComp
I have used mirabelle
Mathias Fleury (May 08 2024 at 10:49):Why not create a session for your theory?
Chengsong Tan (May 08 2024 at 16:00):Mathias Fleury said:
Why not create a session for your theory?
I did, but did not succeed, so with command
isabelle build -o quick_and_dirty -D .
I got the error message:
Building HOL ...
HOL FAILED (see also "isabelle build_log -H Error HOL")
...
*** timeout: Time.time,
*** try0: bool,
*** type_enc: string option,
*** uncurried_aliases: bool option, verbose: bool}
*** Argument: Normal : mode
*** Reason: Value being applied does not have a function type
*** ML error (line 377 of "~~/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML"):
*** Type error in function application.
*** Function: (get_params mode thy []) :
*** {abduce: int option,
*** compress: real option,
*** debug: bool,
*** expect: string,
*** fact_filter: string option,
*** fact_thresholds: real * real,
*** falsify: bool option,
*** induction_rules: induction_rules option,
*** isar_proofs: bool option,
*** lam_trans: string option,
*** learn: bool,
*** max_facts: int option,
*** max_mono_iters: int option,
*** max_new_mono_instances: int option,
*** max_proofs: int,
*** minimize: bool,
*** overlord: bool,
*** preplay_timeout: Time.time,
*** provers: string list,
*** slices: int,
*** smt_proofs: bool,
*** spy: bool,
*** strict: bool,
*** timeout: Time.time,
*** try0: bool,
*** type_enc: string option,
*** uncurried_aliases: bool option, verbose: bool}
*** Argument: mode : mode
*** Reason: Value being applied does not have a function type
***
*** At command "ML_file" (line 35 of "~~/src/HOL/Sledgehammer.thy")
My_Session CANCELLED
Unfinished session(s): HOL, My_Session
0:02:13 elapsed time, 0:06:09 cpu time, factor 2.77
Any ideas?
Mathias Fleury (May 09 2024 at 05:58):Cannot reproduce, which Isabelle version are you using? Did you change any ML as part of your other experiments?
Chengsong Tan (May 09 2024 at 10:15):Mathias Fleury said:
Cannot reproduce, which Isabelle version are you using? Did you change any ML as part of your other experiments?
I'm using Isabelle2023, here are the files I have been building with:
BasicInvariants.thy
CoherenceProperties.thy
BuggyRules.thy
NewSharedRdOwn.thy
Transposed.thy
ROOT
Chengsong Tan (May 09 2024 at 10:15):And I haven't written anything yet tot he .ML files while I was trying to build things.
Mathias Fleury (May 09 2024 at 12:20):First fix your stuff such that $ isabelle build -d \$AFP -D . works…
Mathias Fleury (May 09 2024 at 12:22):At the very least, you need to import
$ cat ROOT
session "My_Session" = HOL +
sessions
Eisbach
PSL
theories
BasicInvariants
BuggyRules
CoherenceProperties
NewSharedRdOwn
Transposed
Import "Eisbach.Eisbach" instead of putting the path
Chengsong Tan (May 09 2024 at 15:00):Mathias Fleury said:
At the very least, you need to import
$ cat ROOT session "My_Session" = HOL + sessions Eisbach PSL theories BasicInvariants BuggyRules CoherenceProperties NewSharedRdOwn Transposed
Hi,
I have removed the Eisbach/PSL bit. I just realised the Isabelle I was using was Isabelle2024-RC3. Could that be an issue? I will now try switching to a different version of isabelle to see if anything changes.
Mathias Fleury (May 09 2024 at 15:38):No that will not make a difference… if your ROOT file is not correct, mirabelle will not work
Chengsong Tan (May 09 2024 at 17:25):Mathias Fleury said:
No that will not make a difference… if your ROOT file is not correct, mirabelle will not work
Thanks Mathias! I have now set up correctly my ROOT and thy files so sessions can be built. Is there an option to set in mirabelle to only run sledgehammer on subgoals that actually have a "sledgehammer" command keyword in them? Right now in a single file I have ~400 subgoals. If each subgoal takes on average 1 minute to finish then that runs forever.
Mathias Fleury (May 09 2024 at 17:28):No mirabelle is intended to run sledgehammer on all steps
Mathias Fleury (May 09 2024 at 17:29):But it running sledgehammer can easily be done in parallel. So use bigger machine before lunch break or something?
Chengsong Tan (May 09 2024 at 17:43):Mathias Fleury said:
But it running sledgehammer can easily be done in parallel. So use bigger machine before lunch break or something?
Ok then I suppose building my own mini-tool that does the redirection would be more efficient. So if I want to set up a purely command-line tool that checks thy files as if running through them by jedit inspection, what command should be used? Right now using ./isabelle jedit -l Pure and then opening my thy files via jedit does the job, but is there a purely command-line approach that does not need to hover through the text?
Mathias Fleury (May 09 2024 at 17:49):I see two options: a new tool (as you have already been told on the mailing-list). Or: you script jedit by adding a plugin that scrolls for you, extract the text from the panel and insert it
Chengsong Tan (May 09 2024 at 17:55):Mathias Fleury said:
I see two options: a new tool (as you have already been told on the mailing-list). Or: you script jedit by adding a plugin that scrolls for you, extract the text from the panel and insert it
I forgot to say, I have already been successful at redirecting the outputs to a file (instead of proof panel), so now I can extract multiple sledgehammer calls' results from a thy file in batches and process them. So there really isn't any tool that says: "go through this thy file as if someone went through them in jedit"? That's surprising to me.
Mathias Fleury (May 09 2024 at 17:57):why would it?
Mathias Fleury (May 09 2024 at 17:58):there is a tool to interact with isabelle (isabelle server)
Mathias Fleury (May 09 2024 at 17:58):there is a tool to act like a text editor (vscode using a LSP server)
Chengsong Tan (May 09 2024 at 19:26):Mathias Fleury said:
there is a tool to interact with isabelle (isabelle server)
What's the functionality/use case of isabelle server?
Mathias Fleury (May 10 2024 at 04:53):My understanding: basically create a new UI that needs more control than LSP gives.
Mathias Fleury (May 10 2024 at 04:54):This is a lot of work and I know of only one application
Mathias Fleury (May 10 2024 at 04:54):The isabelle interface of https://arxiv.org/abs/2308.06970
Last updated: Dec 21 2024 at 12:33 UTC