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: Fri, 25 Oct 2019 22:53:42 -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:CnqVRBQwtWq3vAkE4OWOka7Madpsv+yvbD5Q0YIujvd0So/mwa6yZBGN2/xhgRfzUJnB7Loc0qyK6vumCDBLuM7Y+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi4oAnLssQbjoRuJrstxhfUv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/2bKhMxtl6JbuAyuqABjw4DaZ4GVMeBxfqLbfdgHQWZMUcJcWylHD4ihbYUAEvABMP5WoYf9uVUAsBiwBQejC+zz1zBHhHH50LYm0+g9CwzKwBAsEsgQvHnSsd77NL0SUeewzKTQzjvMdfVW0ir+54jJdxAhpO+DXah1ccXLz0kkCgTIjlSMqY3kJD6VyPoCs3Kb7uZ6UeKvjGknqxpvrTirxsYgkI7Jhpgayl3d8yhy3Yg7Jdq9SEFhYN6kFoNdtySdN4txRcMuWX1nuCE/yrAApJW1fzAKxYw6yxPdZfGLaZaE7xLjWeqLPzt0mXJodKi+ihu26USty+/xWtOp3FtIoSdJiMfAu34D2hDJ9MSLV/lw80G80jiVzQ/T8PtLIUUsmKrbNZEhxrkwm4INsUvdBC/3mF/6jKuRdkUj4ein9eDnY7X8qp+bLY90hRnyMqUomsOhHeQ1KhUCUmqV9OimyrHu/U30TK9UgvErkqTVqpHXKMADqq68GQBV04Ij6xilDzeh1dQVhXgHLE5EeR+ckYjmJUvOIfDiAfe7hFSslyxryO7CPrzhGJnNKWLDkLj5cbZn90Fc0BYzzcxY559MFr4BJ+vzVlbtu9zcEx82KBe5w/3nCdV4zoMRQ3iDAq6fMKPIsF+H/PgjI+eWZNxdhDGoIP88ovXqkHURmFkHfKDv04FERmq/G6FHKkPRU3vph9obFG4M9l4/UP7CllCYQHhXYHGpUqYtoDYhB9T1Xs/4WomxjenZj2+AFZpMazUaWwndQ0etTJ2NXrI3UAzXJ8ZgljIeUr34G90/2Au/8gv9zKFqKvuS/TcX58u6iIpFotbLnBR3zgRaStyH2jjdHX95hHJOQzgxx617sAp60FjRifEl0cwdLsRa4rZyail/NZPYyLUqWc7/QBOHetCOU1uiU5OhGz5jF98=

On 2019-10-26 01:26, Jason Gross wrote:

> I think the better option to use for this is `-load-vernac-source`,
> rather than `-init-file`. I'm not sure how coqide interacts with
> _CoqProject, but if neither -init-file nor -load-vernac-source work
> with coqide, that sounds like a bug worth reporting.

Well, at least -l has a corresponding vernacular command (Load) which I
can enter in the Scratch window. This is an acceptable workaround,
thanks.

I do wonder what .coqrc is intended for, then?

--
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