search

IBM / graph2tac

Graph-based neural tactic prediction models for Coq.
Apache License 2.0
8 stars 4 forks source link

measure time of prediction_requests.send() #140

Closed mirefek closed 1 year ago

mirefek commented 1 year ago

Also measuring the prediction_requests.send(). On the other hand, it didn't seem to me that there would be a significant time difference from the other coroutine in my simple tests. Maybe, @jasonrute could check with his experiments.

LasseBlaauwbroek commented 1 year ago

If you are on the latest coq-tactician-reinforce, the network delay should indeed be short.

But: With the current PR, couldn't a lot of the network time still be hidden in the for loop statement itself?

for msg in message_iterator:
jasonrute commented 1 year ago

@LasseBlaauwbroek We are still recording the iterator time I think, but it was hidden. See my comment above.

LasseBlaauwbroek commented 1 year ago

Okay, yes, I still misunderstood the code. LGTM.

Another drive-by-comment: Aren´t LoggingCounter.msg_idx and LoggingCounters.n_predict the same thing? Can one be removed?

jasonrute commented 1 year ago

I think (as other discussion above shows), a lot of the counters are the same. The question is if the code is cleaner with their own counters or the same. The advantage of having separate counters is that we don't have to worry about say off-by-one errors or other issues where we have to check that the counters are indeed the same. The disadvantage is more code.

mirefek commented 1 year ago

Yes, I think it will probably be better to keep just one counter

LasseBlaauwbroek commented 1 year ago

In this particular case, these variables seem to have exactly the same semantics. Their docs is also (virtually) the same. I don't see any advantage to keeping them separate.

jasonrute commented 1 year ago

As I think about it, if all the counters are the same and have at least one step (since we are always sending back a response), then we don't need the NA stuff in the summary and we don't need/want the +1 in Messages cnt either. https://github.com/IBM/graph2tac/blob/b71be269e9a518eb5a9c89c75fa6aa062e1c628e/graph2tac/loader/predict_server.py#L233-L241

mirefek commented 1 year ago

They are not completely the same, msg_idx is initialized to -1, the others to 0.

mirefek commented 1 year ago

I tried to address the comments, I hope I haven't introduced a +-1 error