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.
you have to pass an option to sledgehammer to keep the files
keep=true according to
isabelle mirabelle -?
Last updated: Aug 13 2022 at 05:18 UTC