PSL Theory batch processing

[discounter24]

I am trying to use PSL together with the isabelle process command. Unfortunately when i run it on a file that contains a try_parallelat the right place, the process will not output anything nor will it terminate. It's not a very hard proof so normally it should terminate fairly quick. (~1 minute in Isabelle/Jedit by doing in manually) Doing the same thing with a sledgehammer example will work as expected. (output a proof if found, then terminate)

I used the command (Theory file as .txt attached): isabelle process -d . -d ../../lib/PSL -l PSL -o quick_and_dirty -T pslexample

pslexample.txt

[yutakang]

Thanks for opening the issue (and using PSL)!

I will try to fix it.

[yutakang]

Hi @discounter24 ,

Sorry for the delay...

I ran pslexample.txt with the command you posted in Isabelle2021.

Of course, Isabelle2021 "failed to finish proof" because of the "sorry" command, but it managed to emit the following in about one minute or so:

subgoal 
apply (induct x)
apply ( metis revtest.simps ( 1 ) )
apply ( metis helper revtest.simps ( 2 ) )
done 

I do not know what made the difference. I list potential reasons why I could not reproduce the problem.

• [1] My laptop is powerful enough. I am using MacBook Pro 2019.
• [2] Something has changed from Isabelle2020 to Isabelle2021.
• [3] I changed the default timeout for sub-tools (Sledgehammer, Quickcheck, Nitpick) for shorter ones (5s and 10s).

Anyway, the problem might be already "solved" in your setting as well.

For now, I close this issue. If you find other problems or if this problem still exists in your setting, please feel free to open new issues.

Sorry for the delay and thanks for using PSL and all that.

I took a full time position for the SuSLik project. So, my response would be slow. But I try to keep improving this repository in my spare time.