Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] how to use auto2?

view this post on Zulip Email Gateway (Jul 17 2022 at 13:10):

From: Adam Dingle <adam.dingle@mff.cuni.cz>
Hello -

I'd like to try using the auto2 prover in writing an Isabelle proof:

<https://github.com/bzhan/auto2>

It appears that it's not included in the standard Isabelle
distribution. So I cloned it to a local directory
(/home/adam/src/auto2). Now I'd like to install it so that I can use
the 'auto2' tactic in any proof that I write. Unfortunately I'm not
sure about how to proceed, even after studying the Isabelle System
Manual. As one attempt, I created a file ~/.isabelle/ROOTS with this
text:

/home/adam/src/auto2

Then at the top of my theory file I wrote

theory arith
imports Main "Auto2_HOL.Auto2_Main"
begin
...

I tried various variations of the 'imports' statement, but Isabelle
always reported

Bad theory import "Auto2_HOL.Auto2_Main"

I'm not even sure if I'm using the right approach. Should I instead
use the 'isabelle' command-line tool to register this library somehow?
Any advice would be appreciated. Thanks -

Adam

view this post on Zulip Email Gateway (Jul 17 2022 at 13:19):

From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Hi Adam,

auto2 is part of the AFP:
https://www.isa-afp.org/entries/Auto2_HOL.html

Please use that version. Instructions on how to use AFP entries can be
found here:
https://www.isa-afp.org/help/

Best wishes,

Kevin

Last updated: Oct 31 2025 at 20:23 UTC