coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Defining Tactics from plugins in Coq 8.9

From: Stefan Muller <smuller AT cs.cmu.edu>
To: <coq-club AT inria.fr>
Subject: [Coq-Club] Defining Tactics from plugins in Coq 8.9
Date: Tue, 12 Mar 2019 15:51:19 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=smuller AT cs.cmu.edu; spf=Pass smtp.mailfrom=skm AT andrew.cmu.edu; spf=None smtp.helo=postmaster AT relay-exchange.andrew.cmu.edu
Ironport-phdr: 9a23:jKjPYh/vJt9w3v9uRHKM819IXTAuvvDOBiVQ1KB40e4cTK2v8tzYMVDF4r011RmVBN2ds6sMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5oHfbx9UiDagfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRgHohikaNDA3/m/YhcNsg6xUux+hux9yzpTIbI2JOvdzfKXQds4aS2pbWcZRUjRMDJ6gb4QRAeoOJ+BYpJT6qVsTqRu+ARejBPnywTJPnX/22LA60+AlEQ7YxgwtBM4BsG/OoNrpMacSTPq5w7fVwjXedv5b3yr25ovQch05vP2AQ7F9fdDPxUU1Cg/IjledpZb7Mz6azugBrnaX4ul6We6xkWIrtRx9riW1yssxlIXEh4QYwU3e+ypj2oY6P9i4RVZ7YdG6FJtQsDmXN5FoTcMmWW5puD82xaMJuJGnfCgF0pInxxHBZPCdaYeI5A/sVPyPLjZ2nn5qZLe/hwuo/Ue+1+L8S9G40FdMriVbjtnBrm0B2wLQ58SdVPdx5Fqt1DaN2gzJ9O1JLlg4la/BJJ4gxr4wmIATsUPGHiLug0X2j6qWe14+9eiu9uvneKvpp5GGO4BojwH+L74ildKiDuQlKgQORXSU+fyg1L3/+k30WKlFjvovkqXArJ/aIdkbqbWiDg9O0ocj7g6/AC283NQZm3kHNlNFdwidg4jnIVGdaMz/WKO0hE3pmzN2zdjHOKfgC9PDNC6Qvq3meONG90NSwQx76M1b459OQuUaJe/3XkLrnNfDSBQ8Lkq5z/uxW4Y17Z8XRW/aWvzRC6jVq1Ldvrt+cdnJX5ccvXPGE9Zg4vfviXEjnlpEI/ug25cNZW/+FfF7ZUiVfCi124tTISIxpgM7CdfSphiaSzcKPSS5ROQ34yx9BY67X9+aG9KdxYeZ1SL+JaV4I2BLDlfXSCXyeoGNSrIBeCmSK8lun3oNU7S7RpBn3hSz8gL21ug/Iw==

Hi,

I'm trying to learn how to write Coq plugins in Coq 8.9, but am not able to use tactics that I define.

Here's my file foo.ml4:

DECLARE PLUGIN "Foo"

open Ltac_plugin

let foo () =
Proofview.tclUNIT ()

TACTIC EXTEND foo_tactic
| [ "foo" ] -> [ foo () ]
END

VERNAC COMMAND EXTEND FooIsDefined CLASSIFIED AS QUERY
| [ "HaveFoo" ] -> [Printf.printf "Yes.\n"]
END

I think I've compiled and loaded everything properly (and included FooIsDefined as a test).
But then:

Require Foo.

HaveFoo. (* Prints "Yes." *)

Lemma x : True.
Proof.
foo. (* Error: The reference foo was not found in the current environment. *)

Anyone see what I'm doing wrong? I imagine it's something simple.

Thanks!
Stefan

[Coq-Club] Defining Tactics from plugins in Coq 8.9, Stefan Muller, 03/12/2019