coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How do I install and use the tactics in the coqhammer?

From: Łukasz Czajka <lukaszcz AT mimuw.edu.pl>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] How do I install and use the tactics in the coqhammer?
Date: Sun, 12 Apr 2020 20:06:48 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lukaszcz AT mimuw.edu.pl; spf=Pass smtp.mailfrom=lukaszczz AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f47.google.com
Ironport-phdr: 9a23:Rtdr8RdJJVIZ8iMN7PEgyBdrlGMj4u6mDksu8pMizoh2WeGdxc2zZR7h7PlgxGXEQZ/co6odzbGJ4+a9ASQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpRZbIBj0NBJ0K+LpAcaSyp3vj6Hhs6HUNi5PnXKWZa54ZEG9qhyUvc0Li6NjLLwww13HuC0bVf5RwDZMOFGahATLzdW5/p1qu3BUpvEo7NxLQ43/fqElUvpVAClgK2Rjt56jjgXKUQbavihUaW4RiBcdRlGdtEimDKe0iTPzs69G4AffJdf/FOxmXDWn8rgtRRP1zj8DZWZgoTPnz/dohacemyqP4hl2woraeoaQbaMscabUfNdcTm1EDJ8ICn5xR7ikZo5KNNIveOZVq46n+gkLpBq6QASgXabhlmAOiXjx0qk3le8mFFOe0Q==

> I am trying to install and use coqhammer. Following the readme, I installed
> this with
>
> opam install coq-hammer
>
> However, while the hammer tactic works, it seems hauto or sauto does not.

These tactics are not yet available in the released version 1.1.1 in
opam. For now, you need to install from source on github to use them.
I'll make a new release with these tactics soon (in a week or two).

[Coq-Club] How do I install and use the tactics in the coqhammer?, Agnishom Chattopadhyay, 04/12/2020
- Re: [Coq-Club] How do I install and use the tactics in the coqhammer?, Łukasz Czajka, 04/12/2020
  - Re: [Coq-Club] How do I install and use the tactics in the coqhammer?, Agnishom Chattopadhyay, 04/14/2020