Pierre-Marie Pédrot (Nov 19 2020 at 10:44): 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?
Pierre-Marie Pédrot (Nov 19 2020 at 10:44):This means that devs not relying on coqmakefile need to handle that option manually.
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.
Pierre-Marie Pédrot (Nov 19 2020 at 10:45):What about using instead (or also) a COQ_TIMING variable?
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
Pierre-Marie Pédrot (Nov 19 2020 at 10:47):@Jason Gross has written scripts for that, so pinging him explicitly
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
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.
Gaëtan Gilbert (Nov 19 2020 at 15:46):coqrunparam?
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?
Pierre-Marie Pédrot (Nov 19 2020 at 15:47):This sounds slightly cumbersome.
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.
Pierre-Marie Pédrot (Nov 19 2020 at 15:49):I would rather have a bunch of weirdly named environment variables...
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.
Pierre-Marie Pédrot (Nov 19 2020 at 16:09):but less also has a lot of other environment variables though
Pierre-Marie Pédrot (Nov 19 2020 at 16:09):one doesn't preclude the other
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
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.
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.
Pierre-Marie Pédrot (Nov 20 2020 at 15:48):@Emilio Jesús Gallego Arias any idea on which one is better?
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.
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.
Enrico Tassi (Nov 20 2020 at 15:50):PCDATA?
Pierre-Marie Pédrot (Nov 20 2020 at 15:50):I don't know what invariants are promised currently.
Pierre-Marie Pédrot (Nov 20 2020 at 15:50):I think you can break stuff if you have unescaped characters?
Pierre-Marie Pédrot (Nov 20 2020 at 15:51):Or dually XML-escaped characters.
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.
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.)
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.
Pierre-Marie Pédrot (Nov 20 2020 at 15:59):Okay.
Pierre-Marie Pédrot (Nov 20 2020 at 15:59):But I want to bench today.
Pierre-Marie Pédrot (Nov 20 2020 at 16:00):An a figurative today, but still.
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.
Pierre-Marie Pédrot (Nov 20 2020 at 16:00):Ltac profiling already relies on Custom feedback nodes for instance.
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.
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.
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.
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
Emilio Jesús Gallego Arias (Nov 20 2020 at 16:02):Yeah the per-span timing PR may be not so hard to fix
Emilio Jesús Gallego Arias (Nov 20 2020 at 16:02):Unfortunately I don't have the cycles today :S
Pierre-Marie Pédrot (Nov 20 2020 at 16:02):Also, fixing dune is not going to help me in any way.
Pierre-Marie Pédrot (Nov 20 2020 at 16:03):Precisely, I want to work around people not using the standard Coq build system.
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
Emilio Jesús Gallego Arias (Nov 20 2020 at 16:03):sorry if I was not clear
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
Emilio Jesús Gallego Arias (Nov 20 2020 at 16:04):and independent of the build system
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
Emilio Jesús Gallego Arias (Nov 20 2020 at 16:04):It is just one word per document node so the overhead is minimal
Emilio Jesús Gallego Arias (Nov 20 2020 at 16:05):streaming the data IMHO gets quite tricky at some point
Emilio Jesús Gallego Arias (Nov 20 2020 at 16:05):in particular as we deal with re-executiong and delayed stuff which happens
Pierre-Marie Pédrot (Nov 20 2020 at 16:05):What about profile data that is global to the document?
Pierre-Marie Pédrot (Nov 20 2020 at 16:06):Like, e.g. total memory consumed.
Pierre-Marie Pédrot (Nov 20 2020 at 16:06):What is the right way to dump this?
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.
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.)
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
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 13 2024 at 01:02 UTC