Enabling analytics during compilation results in spurious output

[tchajed]

Due to a Coq bug (coq/coq#10640), I get this printed out every time I compile a file with the plugin loaded via .coqrc:

R15:34 Analytical.Analytics <> <> lib

There doesn't seem to be a way to fix this, but I wanted to document it here in case anyone wondered where that was coming from.

[tchajed]

Side note: coq_makefile by default compiles with the -q flag, disabling loading the .coqrc, so you won't see this output and analytics are not recorded during compilation. I only see it because we have custom build infrastructure that happens to not pass -q.

[tlringer]

Oh, interesting, how do we set it up not to use -q? Ideally everything would load the .coqrc, it's misleading not to

[tchajed]

It is possible to change this, but it's not straightforward. You need to overwrite COQFLAGS in Makefile.coq to an empty string (or $(OTHERFLAGS) $(COQEXTRAFLAGS) if you're using those variables). The easiest way to implement that is to set them in Makefile.coq.conf.

(where in the above Makefile.coq is the name of the Makefile you generated with coq_makefile)