coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Axioms reported by coqchk

From: Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Axioms reported by coqchk
Date: Fri, 19 Aug 2016 14:15:41 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jacques-henri.jourdan AT normalesup.org; spf=Neutral smtp.mailfrom=jacques-henri.jourdan AT normalesup.org; spf=None smtp.helo=postmaster AT ulminfo.fr
Ironport-phdr: 9a23:tL2m5R3wlYOGe9WTsmDT+DRfVm0co7zxezQtwd8ZsegRI/ad9pjvdHbS+e9qxAeQG96KsrQe1aGM4+igATVGusfZ9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oMyKJV8Wz2DtKfMqdVPt/F2X7pFXyaJZaY8JgiPTpXVJf+kEjUhJHnm02yjG28Gr4ZR4+D5Rsf9yv+RJUKH9YrhqBecAVGduYCgJ45jgsgCGRg+S7FMdVH8Xm1xGGVvr9hb/C7X4uTLnu/E4+CScJ8y+b7cpQzir6e8/ShbjkToKLHs5/WfNi4pyi79BrBunjxp42YvdZIyOKeI4ebnSK4BJDVFdV9pcAnQSSri3aJECWrIM

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.

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