The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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.

> among other reasons because then at least one

> opam package fails to build, not isolating itself from the local
> configuration.

That sounds like a bug to be reported in this opam package.

On Sat, Oct 26, 2019 at 1:19 AM Ian Zimmerman <itz AT very.loosely.org> wrote:

On 2019-10-12 22:58, Gaėtan Gilbert wrote:

> > So ... -init-file is getting passed correctly, but it has no effect
> > because it is accompanied by -q.  Why does coq_makefile pass -q to
> > coqc, and how can I change this behavior?

> make COQFLAGS=

Thanks, I didn't use this literally but it showed me the way.

But now, how to make this work in coqide?  Nothing I tried so far worked
- usually coqide refuses to even start, saying "coqidetop stopped badly"
or something like that.  If I don't do anything it starts OK but it
won't parse any file that contains ssreflect notations.

This is the same with coqide 8.9 (Gtk 2 based) and 8.10 (Gtk 3 based).

Everything works if I put those imports in my _global_ ~/.coqrc but I
don't want to do that - among other reasons because then at least one
opam package fails to build, not isolating itself from the local
configuration.

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