2020-04-21 12:23:25 (GMT)
Mostly for @Alexander Bentkamp @Petar Vukmirovic.
Last week, Alex had some suspiciously low numbers for the LMCS submission of the lambda-free paper (like 160 vs. 180 for LPO and even worse for KBO). Since then I've heard of a polymorphic-ArgCong bug and of a "nasty (performance) bug" involving AVATAR, and some other issues that seem to have afflicted the FSCD camera-ready version.
I have the impression that now would be a good time to iron out all these bugs, if they are not all solved, and also to reflect a bit on the heuristics used for ArgCong. There are two types of ArgCong inferences: those where is the identity and the rest. I'm all in favor of down-prioritizing the rest very much (it's not going to be useful often -- mostly in conjunction with, say, lists of functions or other polymorphic types instantiated with functions), but I hope we keep on applying ArgCong fairly aggressively, because it cannot be that explosive. Maybe polymorphic (i.e. ) ArgCong shouldn't even be in pragmatic (if an eval founds that to be a good idea)?
In general, I am wondering how the stream weights actually work. To my surprise, nothing at all is said about clause weights in our JAR submission. I'd expect that there should be no penalty associated with the first clause (ignoring $$\empty$$s), but that the penalty rapidly rises afterwards; it's rare that one wants the second, third, etc., clause from a stream, I would expect. Of course, these are just guesses, but I have the impression that this was never really evaluated.
Question for Alex: What's the status of the planned LMCS submission, and when do you think we'll be in a good shape to submit?
2020-04-21 12:27:21 (GMT)
Question for Alex: What's the status of the planned LMCS submission, and when do you think we'll be in a good shape to submit?
Due to the bug Petar mentioned, I have to reevaluate now, hoping that I get usable eval result next week. But I am also not sure if Uwe wants to read before we submit.
2020-04-21 13:6:19 (GMT)
Alex you should evaluate on Miami to get resuylts faster
2020-04-21 13:7:6 (GMT)
@Jasmin Blanchette : ArgCong is implemented as follows:
2020-04-21 13:8:5 (GMT)
If the clause is monomorphic the conclusion is put directly into passive set, not in the stream mechanism
2020-04-21 13:8:55 (GMT)
If we perform ArgCong on polymorphic literal, first two conclusions are put in the stream and the rest is scheduled using the stream mechanism
2020-04-21 13:9:7 (GMT)
Petar Vukmirovic: Alex you should evaluate on Miami to get resuylts faster
I am evaluating on Miami!
2020-04-21 13:10:41 (GMT)
Wait... the one with red logo is faster
2020-04-21 13:10:52 (GMT)
Aaaaaand.. now I checked
2020-04-21 13:10:57 (GMT)
That one is Iowa, sorry
2020-04-21 13:11:13 (GMT)
I.e., this one: https://www.starexec.org/
2020-04-21 13:29:53 (GMT)
Not a proper link :p
2020-04-21 13:36:50 (GMT)
(By "put in the stream", you mean "put in the passive set", I presume.)
2020-04-21 13:39:17 (GMT)
Yeah, exactly