Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Selecting provers with Set/Unset Hammer only works after hammer did run once #130

Open
MSoegtropIMC opened this issue Mar 29, 2022 · 0 comments
Labels
bug Something isn't working

Comments

@MSoegtropIMC
Copy link

I had a minor issue writing test files which check if specific provers are there. This works:

(* This file tests if E-Prover is present *)

From Hammer Require Import Hammer.
Require Import Arith.

(** See https://coqhammer.github.io/#hammer-options *)

(** Specifiy manually which provers/modes to use *)
Set Hammer GSMode 0.

(** Don't run provers in parallel *)
Unset Hammer Parallel.

(** Always run external prover*)
Set Hammer SAutoLimit 0.

(** Prove a lemma using any prover, so that hammer loads and queries provers *)

Lemma lem_1 : le 1 2.
  hammer.
Qed.

(** Use only E-prover *)
Set Hammer Eprover.
Unset Hammer Z3.
Unset Hammer Vampire.
Unset Hammer CVC4.

Lemma lem_2 : forall n : nat, Nat.Odd n \/ Nat.Odd (n + 1).
  Time hammer.
Qed.

but when I remove lem_1, it proves lem_2 with Z3 and not eprover. I guess this is so because the provers are only queried when hammers is used first, which then overwrites the explicit prover selection.

I don't think it is really an issue for anybody, but it would be worthwhile to document it, in case it is hard to fix.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants