coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Axioms reported by coqchk

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Axioms reported by coqchk
Date: Fri, 19 Aug 2016 15:08:51 +0200
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 hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:7+9GqRBsQRD1QBrcSB5jUyQJP3N1i/DPJgcQr6AfoPdwSP79psbcNUDSrc9gkEXOFd2CrakV0qyM7eu9BCRAuc/H6yFaNsQUFlcssoY/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbtr8FoOatcmrzef6o8SVOFQRwmDjKu4vZFXu9EOK55FQ2dMjYo8KiTLx6kNSfOpXwW46bXmypD3bovmKwZh47i5LsOgg/cMTGY/zfqA/UKAKRG9+azN90uSw6kKGFVfHpiZEEzZerh0dCA/cqRr+Q53Zsy3gt+M71jPJE9fxSOUOUDCsp4V2ThCg3CUaMTER9XnWz9dvl+Rcuh339E83+JLdfIzAbKk2RajaZ95PGDJM

Hi,

> On 08/19/2016 01:52 PM, Ralf Jung wrote:
>> For an axiom-free development, that's lots of axioms. Some of them
>> (those is iris.program_logic.model.iProp_solution) are actually names
>> sealed through an opaque module. I believe not showing them has been
>> discussed not-too-long-ago here on coq-club, but I don't recall the
>> consensus. Has this been fixed for 8.6, or should we report a bug?
>> Showing module names of a properly instantiated module interface as
>> "axioms" is at best confusing (and "Print Assumptions" doesn't show
>> them).
> I think this qualifies as a bug indeed. Or at least it would require a
> discussion on the bug tracker.

Reported as <https://coq.inria.fr/bugs/show_bug.cgi?id=5030>.

Kind regards,
Ralf

Re: [Coq-Club] Axioms reported by coqchk, (continued)
- Re: [Coq-Club] Axioms reported by coqchk, Jacques-Henri Jourdan, 08/19/2016
  - Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ade Umut Huxtable, 08/19/2016
  - Re: [Coq-Club] Axioms reported by coqchk, Jonathan Leivent, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ade Umut Huxtable, 08/19/2016
  - Re: [Coq-Club] Axioms reported by coqchk, Jonathan Leivent, 08/19/2016
    - Re: [Coq-Club] Axioms reported by coqchk, Jason Gross, 08/20/2016
      - Re: [Coq-Club] Axioms reported by coqchk, Jonathan Leivent, 08/20/2016
        
        Re: [Coq-Club] Axioms reported by coqchk, Jonathan Leivent, 08/20/2016
        
        Re: [Coq-Club] Axioms reported by coqchk, Jonathan Leivent, 08/20/2016
        
        Re: [Coq-Club] Axioms reported by coqchk, Jonathan Leivent, 08/20/2016
        
        RE: [Coq-Club] Axioms reported by coqchk, Soegtrop, Michael, 08/21/2016