coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

[Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything, guninski
- Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything, Stéphane Glondu
- <Possible follow-ups>
- Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything, Bruno Barras
  - RE: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything, Georges Gonthier
    - Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything, Stéphane Glondu