The Coq mailing list

[Yoichi Hirai <i AT yoichihirai.com>]

(12/31/13 6:54 PM), Guillaume Melquiond wrote:
> On 31/12/2013 10:30, Yoichi Hirai wrote:
> 
>> Here I'd like to ask which Coq commands are unsafe.  Since the server runs
>> coqc and coqchk on user inputs, some keywords are forbidden
>> (Pwd Cd Drop ProtectedLoop Load Declare LoadPath Path ML State Debug 
>> Extract).
>> I am not very sure whether this list is complete.
> 
> You should also disable the "external" tactic. Not sure whether this is 
> enough. (In fact, I am pretty sure it is not, since Coq was not designed as 
> a sandbox.)
> 
> Best regards,
> 
> Guillaume
> 
> PS: I'm sure you already took care of it, but just in case, make sure that 
> the memory the processes can consume is limited. It only takes a few lines 
> of Coq to instantly bring a machine to its knees otherwise.
> 

Thank you for the remark.  That one is immediate.
Also I think I need other measures than just banning keywords.

The resource consumption problem arose when I tried the tauto tactic on this
https://proofmarket.org/problem/view/8

Sincerely,

Yoichi