coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Why does coq_makefile impose -q option?

From: Ian Zimmerman <itz AT very.loosely.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Why does coq_makefile impose -q option?
Date: Sat, 26 Oct 2019 10:25:48 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=itz AT very.loosely.org; spf=Pass smtp.mailfrom=itz AT very.loosely.org; spf=Pass smtp.helo=postmaster AT very.loosely.org
Ironport-phdr: 9a23:0i0g3ReNgXeQ8Lf517BBIwwvlGMj4u6mDksu8pMizoh2WeGdxcS6YR7h7PlgxGXEQZ/co6odzbaP6OaxBCdZuM3JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRu7oR/Vu8QWjoduN7s9xxXUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU293zZitFrjKJDvh2uuwB/zYDTYIGQLvV+f6Xdds4eSWdOWstdUipMCZ6+YYQSFeoMJehWoYnjqVUTrhW+CwajC//yxTBKiHD7xrE63/g7HA3awAAtBcwCvXLJp9v1LqcSVuW1wbHLwzrZafNdxDTy6InNchAkv/6MR7dwftDXyUIyEA7Fj0mQqI3+MjOLyOsNqWia4/BkVeKojG4nsB9+ojyvx8s2jYnJnI0Vx0nC+C5kzog1Iti4R1R6Yd6iCJZQsiaaN4xxQs84X25ovyM6x7sbspC4ZCgH0IkryhzRZvCdbYSF4hLuWPyPLTtlhH9pYrOyihKq/UWhyODwTNS43VRFoyZfjNXBuH4A2wbN5sSaSPZw+Fqq1yyV2ADJ8O5EJFg5larFJJ4lxb49joQTvlrZHi72gkn2iKiWdkI/+ue27+TmYq/qppiGN497kg3+M6IuldKjAekgLwQDXWaW9f6i2LDj/UD1WqtGguA2n6XDsZ3XIdwXpqujDA9U1oYj5Qy/DzCj0NkAnHkHMFNEdQmZj4f3IVHPIOr0DfO4g1Srizdk2fTGP737DpXKNHjDn6/tfaxh5E5E1Aoz0ddf6opIBbEGOfL/Q1P+tNjFDhAiKAG02ObmCNBl1owEQ26PA6mZMLnTsVCS/O4vLfOMN8cpv2P2LOFg7Przh1c4n0UcdO+nx8g5cne9S9VvJQ2rYH/pj80EGGFC6gsiXsT0hUeTFzpUYG2/W7N64Ss0XtH1RbzfT5yg1eTSlBywGYdbMzwXUw3eITLTb4yBHsw0RmeSL8tmy2xWS7W7Wskl0ha1uQvrjb19IbiNo3xKhdfYzNFwotbru1Q3/D1wAd6a1jjdHX95hHJOQzgxx617sAp60FjRiPEk0cwdLsRa4rZyail/LYTVlrwoFd3oS0TFedCSRVK3BNK8DmNpQw==

On 2019-10-26 02:30, Jason Gross wrote:

> I believe .coqrc is intended for local commands that you might want for
> interactive use, but not globally. e.g., you might have a different
> preferred printing width (Set Printing Width) or depth (Set Printing
> Depth).

This sounds sensible, but why does coqc also obey the commands in this
file, in such case?

--
Please don't Cc: me privately on mailing lists and Usenet,
if you also post the followup to the list or newsgroup.
To reply privately _only_ on Usenet and on broken lists
which rewrite From, fetch the TXT record for no-use.mooo.com.

[Coq-Club] Why does coq_makefile impose -q option?, Ian Zimmerman, 10/12/2019
- Re: [Coq-Club] Why does coq_makefile impose -q option?, Gaëtan Gilbert, 10/12/2019
  - Re: [Coq-Club] Why does coq_makefile impose -q option?, Ian Zimmerman, 10/26/2019
    - Re: [Coq-Club] Why does coq_makefile impose -q option?, Jason Gross, 10/26/2019
      - Re: [Coq-Club] Why does coq_makefile impose -q option?, Ian Zimmerman, 10/26/2019
        
        Re: [Coq-Club] Why does coq_makefile impose -q option?, Jason Gross, 10/26/2019
        
        Re: [Coq-Club] Why does coq_makefile impose -q option?, Ian Zimmerman, 10/26/2019
        
        Re: [Coq-Club] Why does coq_makefile impose -q option?, Jason Gross, 10/26/2019