Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything


chronological Thread 
  • From: Stéphane Glondu <steph AT glondu.net>
  • To: Georges Gonthier <gonthier AT microsoft.com>
  • Cc: Bruno Barras <bruno.barras AT inria.fr>, "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything
  • Date: Wed, 04 May 2011 13:49:31 +0200

Le 04/05/2011 13:20, Georges Gonthier a écrit :
[...] Also coqchk should have an option to trace the assumptions under which 
the file is checked. [...]

It has (-o).


Cheers,

--
Stéphane



Archive powered by MhonArc 2.6.16.

Top of Page