The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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).  You might want to Set Ltac Profiling or Set NativeCompute Profiling by default.  Perhaps you want to see proof diffs, and Set Diffs to something other than "off".  Or perhaps you want to Set Fast Name Printing, because your goals are taking too long to print.  Perhaps you want to Set Ltac Backtrace, now that by default Coq 8.10 (I think) no longer displays full backtraces for Ltac.  Maybe you want to Set Nested Proofs Allowed, because you often develop with nested proofs, but you don't care to allow them in completed files.  Maybe you want to change one of two dozen different printing options.  Perhaps you want to Set Suggest Proof Using, so that you notice when you have completed a proof without a `Proof using` statement.  (You can see all available options with `Print Options.`)  You might also want to include tactics or definitions which you use only for debugging (e.g., I frequently use `Axiom admit : forall {T}, T.` when prototyping things, so it might be a candidate for a .coqrc file.)

My ~/.coqrc file is:

Unset Printing Dependent Evars Line.

Set Suggest Proof Using.

Set Ltac Backtrace.

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

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.