The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Is it okay to get user error "User error: Cannot find library Definitions in loadpath" when solving problem "Takeuchi Function tak"?



On Wed, Jan 1, 2014 at 12:57 AM, Yoichi Hirai <i AT yoichihirai.com> wrote:
>
> I just woke up to find these pieces of advice:
>
> (1/1/14 1:08 AM), Vladimir Voevodsky wrote:
> > How about "admit" ?
> >
> > V.
> >
> > PS Why is LoadPath forbidden?
> Currently, "admit" is detected by coqchk -o command.
> "LoadPath" can be dangerous because it might be used to explore the directory structure.
>
> (1/1/14 12:45 AM), Perry E. Metzger wrote:
> > Depending on the operating system you are running on, you can use
> > various MAC or capability systems to lock down the Coq processes. On
> > FreeBSD I recommend Capsicum. On Linux, AppArmor and things like it
> > may be appropriate choices
> This seems like a well-paven path.  Thank you.
>
> (1/1/14 1:16 AM), drg AT illinois.edu wrote:
> > It would be better to put coqc in an external sandbox, following, say, the
> > advice of Daniel J. Bernstein in "Some thoughts on security after ten years of
> > qmail 1.0"  http://cr.yp.to/qmail/qmailsec-20071101.pdf , because it's hard to
> > audit a complex program for security.
> The paper looks interesting on its own.  The section 5.2 is quite relevant.
> Being paranoid is both worthwhile and interesting.
>
> Sincerely,
>
> Yoichi Hirai
>