coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] VM/native mode within Coq

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] VM/native mode within Coq
Date: Thu, 8 Oct 2015 19:23:32 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:jK9jDh+2YwY1uP9uRHKM819IXTAuvvDOBiVQ1KB90OMcTK2v8tzYMVDF4r011RmSDdmdtK8P0rOO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStKU0Jn8jrnqs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGCaJ/HoXVS0qmwFTAkCR4RfgX5z29DfzrfF88CicJ8z/C74uD2fxp5x3QQPl3X9UfwUy93va35R9

On Thu, Oct 08, 2015 at 06:37:25PM +0200, Epiphanie wrote:
> > Empirically, based on the rate of discovery of
> > proofs of False, it looks as reliable as the rest of the Coq
> > implementation.
> I am not quite sur I understand that sentence, given there is at least
> two known proof of false in vm_compute (that are still present in the
> current stable release but not the beta, as far as I know), notably one
> using 256 constructor for one object.

AFAIK these bugs have been fixed in the git branch for 8.4. When a new pl
release for 8.4 will be made, the fixes are going to be included.

If you really need a data type with many many constructors and fast
computations on it, just git pull and you'll be good to go.

Best,
--
Enrico Tassi

Re: [Coq-Club] VM/native mode within Coq, Andrew W. Appel, 09/30/2015
- <Possible follow-up(s)>
- Re: [Coq-Club] VM/native mode within Coq, Xavier Leroy, 10/06/2015
  - Re: [Coq-Club] VM/native mode within Coq, Maxime Dénès, 10/08/2015
    - Re: [Coq-Club] VM/native mode within Coq, Epiphanie, 10/08/2015
      - Re: [Coq-Club] VM/native mode within Coq, Enrico Tassi, 10/08/2015