coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Uncaught exception upon destructing a disjunction

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr, Bruno Le Floch <blflatex AT gmail.com>
Subject: Re: [Coq-Club] Uncaught exception upon destructing a disjunction
Date: Tue, 12 Dec 2017 10:03:17 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT jupiter.mpi-klsb.mpg.de
Ironport-phdr: 9a23:lGTvoRz6vB75Ck3XCy+O+j09IxM/srCxBDY+r6Qd0uIQIJqq85mqBkHD//Il1AaPBtqLra8cw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2NBXupSi56idXERHiPyJ0IP70E8jclYD//fqv/ZqbRwgAqj66arM6eB+yowHYqsQGqYRnI6c1jBDOpy0bVf5RwDZSLFad1zTh4Mj4qJx+9St4vuogstVfSuP9ZatuHu8QNygvL21gvJ6jjhLEVwbavnY=

Hi,

On 12.12.2017 02:38, Bruno Le Floch wrote:
> Hi Ralf,
>
>> This is definitely a bug! Coq 8.5 is pretty ancient (the current
>> version is 8.7), but in fact the issue reproduces with Coq 8.7.
>>
>> Can you report this at <https://github.com/coq/coq/issues/>?
>
> Thanks. Yes, I just use version of Coq that comes out-of-the-box on
> Ubuntu. Tej Chajed reported the bug on GitHub, thanks for that too.

That is strange -- 8.5 is not the version shipped with any version of
Ubuntu: The LTS are on 8.4, and everything else seems to be on 8.6.
<https://packages.ubuntu.com/search?keywords=coq&searchon=names&suite=all&section=all>

But, anyway, distribution packages are frequently pretty outdated. The
recommended way to obtain Coq is to install opam from your distribution
("apt install opam"), and then install coq from opam ("opam install
coq"). That way, you will get new versions quickly.

Kind regards,
Ralf

>
> Best regards,
> Bruno
>

[Coq-Club] Uncaught exception upon destructing a disjunction, Bruno Le Floch, 12/10/2017
- Re: [Coq-Club] Uncaught exception upon destructing a disjunction, Ralf Jung, 12/11/2017
  - Re: [Coq-Club] Uncaught exception upon destructing a disjunction, Bruno Le Floch, 12/12/2017
    - Re: [Coq-Club] Uncaught exception upon destructing a disjunction, Ralf Jung, 12/12/2017
      - Re: [Coq-Club] Uncaught exception upon destructing a disjunction, Bruno Le Floch, 12/15/2017
- Re: [Coq-Club] Uncaught exception upon destructing a disjunction, Gabriel Scherer, 12/11/2017
  - Re: [Coq-Club] Uncaught exception upon destructing a disjunction, Merlin Göttlinger, 12/11/2017
    - Re: [Coq-Club] Uncaught exception upon destructing a disjunction, Tej Chajed, 12/11/2017