Stream: Beginner Questions

Topic: Mirabelle/Sledgehammer

view this post on Zulip joe (May 11 2022 at 09:56):

Hello!
I'm absolutely new to isabelle, and want to use it to generate the sledgehammer smtlib benchmarks. So I wanted to ask whether anyone could tell me what's the best way to generate these (using mirabelle)?
I tried running
isabelle mirabelle -D $AFP/thys -O output -T 'Ordinary_Differential_Equations' -m 1 -A 'sledgehammer[keep=true, prover_timeout=1]'
but no output files were generated.

view this post on Zulip Mathias Fleury (May 11 2022 at 14:58):

you have to pass an option to sledgehammer to keep the files

view this post on Zulip Mathias Fleury (May 11 2022 at 14:59):

keep=true according to isabelle mirabelle -?

Last updated: Apr 23 2024 at 20:15 UTC