The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hi Abhishek,

In principle, you can access layers as low as kernel/safe_typing.mli
without danger. It means that you trust only the kernel, but don't mess
with its internals.

So a plug-in using only higher layers like toplevel/command.mli should
not be able to break Coq's consistency.

I wouldn't be too surprised if it was still possible to find a part of
the kernel whose correctness relies on external invariants of the
system, but no such problem is known at the moment and we would consider
it a bug.

We are currently working on a plug-in API that should be not only safe,
but also make it easier to write plug-ins.

Hope it helps.

Maxime.

On 11/16/16 05:16, Abhishek Anand wrote:
> 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
> <https://github.com/coq/coq/blob/trunk/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/ <http://www.cs.cornell.edu/~aa755/>