coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] safe interface for writing Coq plugins

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] safe interface for writing Coq plugins
Date: Tue, 15 Nov 2016 23:16:49 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f169.google.com
Ironport-phdr: 9a23:S+26gR+b8kYu1/9uRHKM819IXTAuvvDOBiVQ1KB+2ukcTK2v8tzYMVDF4r011RmSDN6dsqkP1LKe8/i5HzdfsdDZ6DFKWacPfiFGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkImbtjyT4XVloG80/24s8nYZBwNjz6ga5tzKg+3pEPfrJ9Fr5FlL/MYwBvIuXtFeKx/w2puKRrHlhz859yw8Z0l+iJZvf5n9s9cXo31eq05SfpTCzFwYDN939HiqRSWFVjH3XAbSGhDyhc=

As someone wanting to extend a Coq plugin (template-coq), how can I be sure that I don't jeopardize Coq's consistency?

Is it true that any plugin that uses only the functions in coq/toplevel/command.mli to make changes to Coq's state (e.g. to add new definitions) does not jeopardize Coq's consistency?

If not, is there such a safe interface?

By consistency, I mean that there should be no closed proof of False, no matter what the plugin does.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] safe interface for writing Coq plugins, Abhishek Anand, 11/16/2016
- Re: [Coq-Club] safe interface for writing Coq plugins, Maxime Dénès, 11/16/2016
  - Re: [Coq-Club] safe interface for writing Coq plugins, Hugo Herbelin, 11/16/2016