Stream: Coq devs & plugin devs

Topic: Timing options in CoqMakefile


view this post on Zulip Pierre-Marie Pédrot (Nov 19 2020 at 10:44):

Is there any reason why we pass the -time option to coqtop as a command line argument instead of an environment variable?

view this post on Zulip Pierre-Marie Pédrot (Nov 19 2020 at 10:44):

This means that devs not relying on coqmakefile need to handle that option manually.

view this post on Zulip Pierre-Marie Pédrot (Nov 19 2020 at 10:45):

Notably, remake has been ignoring the flag for ages and I abandoned the idea of tweaking it.

view this post on Zulip Pierre-Marie Pédrot (Nov 19 2020 at 10:45):

What about using instead (or also) a COQ_TIMING variable?

view this post on Zulip Pierre-Marie Pédrot (Nov 19 2020 at 10:46):

I am asking because I'd like to also add more precise memory profile outputs to coqc

view this post on Zulip Pierre-Marie Pédrot (Nov 19 2020 at 10:47):

@Jason Gross has written scripts for that, so pinging him explicitly

view this post on Zulip Enrico Tassi (Nov 19 2020 at 11:31):

It makes sense to use an env var, as long as it is called COQ_something I'm OK with it

view this post on Zulip Guillaume Melquiond (Nov 19 2020 at 15:45):

Pierre-Marie Pédrot said:

What about using instead (or also) a COQ_TIMING variable?

I would go for a more general name. Indeed, there are a bunch of command-line options that have no impact on reading .v or producing .vo and thus could be passed by a side channel: -profile-ltac, --memory, -debug.

view this post on Zulip Gaëtan Gilbert (Nov 19 2020 at 15:46):

coqrunparam?

view this post on Zulip Pierre-Marie Pédrot (Nov 19 2020 at 15:47):

@Guillaume Melquiond Are you proposing to merge all those options in one single environment variable?

view this post on Zulip Pierre-Marie Pédrot (Nov 19 2020 at 15:47):

This sounds slightly cumbersome.

view this post on Zulip Pierre-Marie Pédrot (Nov 19 2020 at 15:48):

In particular if two pieces of code try to set orthogonal flags, one will erase the other.

view this post on Zulip Pierre-Marie Pédrot (Nov 19 2020 at 15:49):

I would rather have a bunch of weirdly named environment variables...

view this post on Zulip Guillaume Melquiond (Nov 19 2020 at 16:07):

I am proposing to just have COQOPTIONS="-time -profile-ltac". That is, parsing the command line options starts by parsing the content of this environment variable. The same way the less command has a LESS variable.

view this post on Zulip Pierre-Marie Pédrot (Nov 19 2020 at 16:09):

but less also has a lot of other environment variables though

view this post on Zulip Pierre-Marie Pédrot (Nov 19 2020 at 16:09):

one doesn't preclude the other

view this post on Zulip Pierre-Marie Pédrot (Nov 19 2020 at 16:10):

I don't know if there are official guidelines on the use of environment variables

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 15:46):

To be build-system independent, we also need to print the time data inside a file rather than on the standard output.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 15:47):

For this, I need to handle timing metadata in a special way in System.with_time. I am hesitating between adding a dedicated Feedback node, or reuse the Feedback.Custom one.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 15:48):

@Emilio Jesús Gallego Arias any idea on which one is better?

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 15:48):

Custom doesn't require changing anything but carrying string data over XML is fragile IIUC.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 15:50):

My plan is then to set a feedback handler for that information when -time is passed so that the output is redirected to whatever.v.timing instead of performing that through CoqMakefile currently.

view this post on Zulip Enrico Tassi (Nov 20 2020 at 15:50):

PCDATA?

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 15:50):

I don't know what invariants are promised currently.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 15:50):

I think you can break stuff if you have unescaped characters?

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 15:51):

Or dually XML-escaped characters.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 15:52):

Reading the code, it seems that the contents of PCData is escaped in printing, but only for a handful of XML-specific characters.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 15:57):

(Maybe the Feedback.Custom node should use another datatype as XML, so that we know we can send whatever data in there and let the upper layer perform the XML serialization for us.)

view this post on Zulip Emilio Jesús Gallego Arias (Nov 20 2020 at 15:59):

@Pierre-Marie Pédrot see https://github.com/coq/coq/issues/11542 and https://github.com/coq/coq/pull/12730

I don't think System.with_time is the right place for this , neither the feedback handler approach. Ideally, the document manager would keep the timing information in each of the sentences, then dump in catapult format, as for example timings may not be linear but overlap, etc...

The way the processing loop is written today makes it a bit challenging.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 15:59):

Okay.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 15:59):

But I want to bench today.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:00):

An a figurative today, but still.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 20 2020 at 16:00):

Just keep in mind that system.with_time is called in some other parts of the system.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:00):

Ltac profiling already relies on Custom feedback nodes for instance.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:00):

Yes, but it has the batch option which is dedicated to coqc timing it seems.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 20 2020 at 16:01):

That's a good example of a problem, as it forces simple compiler etc... to link to the stm.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 20 2020 at 16:01):

and provides not the best information. You could go quite far storing the timing info in Vernacstate but still the upper layers need to be aware and collect the information.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 20 2020 at 16:02):

I think that finishing the PR I pointed out may be more efficient in the medium term, but indeed OMMV

view this post on Zulip Emilio Jesús Gallego Arias (Nov 20 2020 at 16:02):

Yeah the per-span timing PR may be not so hard to fix

view this post on Zulip Emilio Jesús Gallego Arias (Nov 20 2020 at 16:02):

Unfortunately I don't have the cycles today :S

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:02):

Also, fixing dune is not going to help me in any way.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:03):

Precisely, I want to work around people not using the standard Coq build system.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 20 2020 at 16:03):

Dune doesn't need to be fixed, I just pointed out to that PR as an example of how Dune handles timing data with catapult

view this post on Zulip Emilio Jesús Gallego Arias (Nov 20 2020 at 16:03):

sorry if I was not clear

view this post on Zulip Emilio Jesús Gallego Arias (Nov 20 2020 at 16:03):

Which seems like a good choice of output format. So if you manage to get the timing info in the document nodes, then dumping it is pretty easy

view this post on Zulip Emilio Jesús Gallego Arias (Nov 20 2020 at 16:04):

and independent of the build system

view this post on Zulip Emilio Jesús Gallego Arias (Nov 20 2020 at 16:04):

I tried to do that as to have a reliable way for users to get the timing data on hover for jscoq

view this post on Zulip Emilio Jesús Gallego Arias (Nov 20 2020 at 16:04):

It is just one word per document node so the overhead is minimal

view this post on Zulip Emilio Jesús Gallego Arias (Nov 20 2020 at 16:05):

streaming the data IMHO gets quite tricky at some point

view this post on Zulip Emilio Jesús Gallego Arias (Nov 20 2020 at 16:05):

in particular as we deal with re-executiong and delayed stuff which happens

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:05):

What about profile data that is global to the document?

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:06):

Like, e.g. total memory consumed.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 16:06):

What is the right way to dump this?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 20 2020 at 16:11):

That's a bit tricky to compute due to sharing, as execution happens usually in chunks; the best place IMHO is to place it in the stm structures, this time, not per node, but per document.

view this post on Zulip Jason Gross (Nov 25 2020 at 15:11):

I was under the impression that LtacProf used custom feedback nodes because that's the blessed way to communicate with the main thread/stm when running from a worker. (In particular we need to persist profiling state---generated during a proof---past the end of Qed.)

view this post on Zulip Jason Gross (Nov 25 2020 at 15:14):

In particular if two pieces of code try to set orthogonal flags, one will erase the other.

There is a standard solution to this problem (which occurs already with PATH); code should always extend this variable, not overwrite it

view this post on Zulip Enrico Tassi (Nov 25 2020 at 16:49):

LtacProf uses the custom node because we did not add a dedicated node ;-) All feedback is streamed to master and potentially to the UI. Custom was there to let plugins generate their own feedback without changing Coq.


Last updated: Oct 16 2021 at 09:07 UTC