coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] mllib vs mlpack

From: Kenneth Roe <kendroe AT hotmail.com>
To: Coq-Club <coq-club AT inria.fr>
Subject: [Coq-Club] mllib vs mlpack
Date: Thu, 16 Nov 2017 15:21:53 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=Pass smtp.mailfrom=kendroe AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM02-SN1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:vqE6ZhE2iCBbH00aoY+SRZ1GYnF86YWxBRYc798ds5kLTJ76ocmwAkXT6L1XgUPTWs2DsrQf1LqQ7viocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TXhpQIVTz74LE9eIvn/UtrZiN3y3OSv8bXSZR9JjXyze+UhAg+xqFDyu88QjJdiYpw2x1OdoXZOd/5RyEtoIk6Wlhf4oMy3+cgwoGxrp/s9+psYAu3BdKMiQOkAAQ==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Coq 8.7 supports two packaging mechanisms for plugins, "mllib" and "mlpack". Towards the end of my .ml4 file, I have the following declarations:

TACTIC EXTEND AR2

| ["arewrite"] -> [Stuff.arewrite]

END

(* PrintAST command

The depth specifies the depth at which to unroll nested type definitions *)

VERNAC COMMAND EXTEND AR

| [ "printAST" constr(def) ] -> [ Stuff.print_ast 0 def ]

| [ "printExp" constr(def) ] -> [ Stuff.print_exp 0 def ]

| [ "printAST" constr(def) "with" "depth" integer(depth)] -> [ Stuff.print_ast depth def ]

END

After doing some experimentation, I found that with mllib everything works. However, when I package everything into an mlpack library, the "arewrite" tactic is not recognized. However, the "printAST" and "printExp" commands are recognized. Do TACTIC declarations need to be done differently for an mlpack?

- Ken

[Coq-Club] mllib vs mlpack, Kenneth Roe, 11/16/2017