coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Automatically tracking down bugs in coq?

From: Bas Spitters <spitters AT cs.ru.nl>
To: Hendrik Tews <tews AT os.inf.tu-dresden.de>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Automatically tracking down bugs in coq?
Date: Fri, 12 Apr 2013 08:08:04 -0400

You can have a look at the improved universe polymorphism in trunk.

On Fri, Apr 12, 2013 at 2:56 AM, Hendrik Tews <tews AT os.inf.tu-dresden.de> wrote:

Jason Gross <jasongross9 AT gmail.com> writes:

I've thrown together a bit of code at
https://github.com/JasonGross/coq-bug-finder which does some basic

It would be nice if your tool could also be used to create
minimal examples for bugs in Coq specifications.

For example, I have a universe inconsistency error within a
development of 10,000 lines. I would be really interested to
strip this down to the minimal set of definitions/lemmas that
reproduce the universe inconsistency.

Bye,

Hendrik

[Coq-Club] Automatically tracking down bugs in coq?, Jason Gross, 04/09/2013
- Re: [Coq-Club] Automatically tracking down bugs in coq?, Frédéric Besson, 04/09/2013
  - Re: [Coq-Club] Automatically tracking down bugs in coq?, AUGER Cédric, 04/10/2013
    - Re: [Coq-Club] Automatically tracking down bugs in coq?, Jonas Oberhauser, 04/10/2013
      - Re: [Coq-Club] Automatically tracking down bugs in coq?, Jason Gross, 04/11/2013
        
        Re: [Coq-Club] Automatically tracking down bugs in coq?, Hendrik Tews, 04/12/2013
        
        Re: [Coq-Club] Automatically tracking down bugs in coq?, Jason Gross, 04/12/2013
        
        Re: [Coq-Club] Automatically tracking down bugs in coq?, Bas Spitters, 04/12/2013