Parsing preorder reasoning expressions takes very, very long! #3209
Comments
|
@nicolabotta If it is a parsing issue, then it may be due to the way external syntax is handled now, which is unfortunately not very efficient and requires a lot of backtracking. I am not completely sure what is the optimal workaround, but my guess is that it would be possible to use something like |
|
Actually, another alternative would be to use |
|
@ahmadsalim You are right: in the original On the other hand, I do not like the idea of sacrificing readability for the sake of type checking time and I think that, in principle, proofs should be easy to read for humans (in fact, I always tend to explicitely add to my proofs trivial steps (steps that can be implemented in terms of Thus, the question here is whether parsing preorder reasoning proofs can be significantly improved or not. In the first case, I am happy to wait until this is done (if it is not going to take years). On the other hand, if the misbehavior reported in this thread turns out to be a symptom of a more fundamental problem (e.g. parsing time more than linear in the length of proofs), then it would probably be meaningful to issue some warning or recommendation against using preorder reasoning in all but very short proofs. |
|
@nicolabotta I think the parsing should be improved but rewritting the parser requires a bit of work (if it has to be done correctly). module Test
import Syntax.PreorderReasoning
import Control.Isomorphism
infixl 1 =**
infixl 1 **=
data Step : (a : Type) -> (x : a) -> (y : a) -> Type where
MkStep : (x : a) -> (x = y) -> Step a x y
(=**) : (x : a) -> (x = y) -> Step a x y
x =** prf = MkStep x prf
(**=) : Step a x y -> y = z -> x = z
(MkStep x {y = y} prf) **= prf2 = rewrite prf in rewrite prf2 in Refl
stupidProof : 2 + 2 = 4
stupidProof = 2 + 2 =** Refl **= 4 QEDfor your current proof? |
|
@ahmadsalim Do you expect the introduction of with Am I missing something obvious? My guess is that something has changed in Idris lately that makes parsing certain expressions a pain. How can it be that it takes almost 10 minutes to parse 42 lines of code? |
|
@nicolabotta I did, I guess my initial assumption of that this was being primarily to external syntax is wrong. |
|
Can you try to lower the version bound on trifecta to see if it's a recent
|
|
I have no idea what trifecta is, but it takes about 50sec for my first example to fail to type check with 88d8075 (Mar 1, 2016) against about 5 minutes with fc3e88c. Now, 50 seconds is still a lot of time for 40 lines of code. But the test shows that something very bad for parsing efficiency happened in the last three months. |
|
Trifecta is the parsing library that idris uses. One can test with an older
|
|
@melted It does not appear to be possible to in because of dependency problems. Thus, I assume that as in the current Idris version (that needs about 5 minutes to parse the example). I am going to bisect a little bit more and report. |
|
The culprit appears to be commit 536372f (Rename Lazy' => Delayed edwinb committed 23 days ago). Here are the results of the bisection exercise:
It would probably be good to add examples like the one above to the test suite to catch sudden deteriorations of parsing times and type checking times. |
|
Putting my two cents out there: Rather than the test suite, I think it would be better to add it to the benchmarks if you are to add something. |
|
I think that the first step is to get the parsing times back from 400 sec. to 40 sec. Something has happened with commit 536372f that has made parsing almost 10 times slower. This might or might not be directly related with the commit itself. It is conceivable that some external library (trifecta?) is responsible for the misbehaviour. Once the problem is understood and fixed, we should think about tests that can effectively prevent things like this to happen. I am happy to help here, but I need some advice. |
|
@nicolabotta So there are no changes in the parser in that commit, so maybe it is a previous commit or trifecta as you mentioned? |
|
Ahmad Salim Al-Sibahi notifications@github.com wrote:
As you can see from the bisection results, commit 5925424 (and the commits before) take about 40 seconds to parse and commit 536372f (and the subsequent commits) take about 400 seconds to parse! As I mentioned, the commit itself does not need to be directly responsible for the misbehavior: it could be something that happened between 5925424 and 536372f in external libraries. Still, a proper check of parsing or type checking times would have avoided this pitfall.
|
|
@nicolabotta So the latest changes in the parser happened with commit 5a937cc . Could you please see if your issues also happen with that commit? Thanks, and sorry for the trouble. |
Done. With 5a937cc it takes about 330 seconds to parse the example! This is a bit surprising because, as reported above, all the Idris versions that I had tried before 536372f parsed the example in 40 to 60 seconds. And all the version after (and included) 536372f needed between 400 and 450 seconds. This was because I was bisecting through Idris versions, of course. Now, the new results suggest that there are more points in the commit sequence where the jump between 40-60 and 400-450 seconds occurs. Two commits after 5a937cc (commit 0917cf8) we are back to 40 seconds! |
|
@nicolabotta So it is because I looked for parent commits of the commit 536372f you referenced (I did it on GitHub), and it seems that the 5a937cc was the ancestral commit that modified the parser. |
|
@ahmadsalim Ok, now the question is: why do we revert back to 40 seconds with commit 0917cf8 (or, perhaps even a3b40c2)? Assumig that commit 5a937cc has "spoiled" the parser, how can it be that commit 0917cf8 (or a3b40c2) "fix" the problem without even touching the parser? I suspect that the issue is related with external libraries and that different commits make the parser use different external libraries. Does this make sense? How do you plan to proceed? Please, let me know if you want me to run further tests. |
|
That sounds like an artifact of merging. The commit that is fast was likely
|
|
@melted Fine. In this case, let's start with the hypothesis that commit 5a937cc is the culprit. The question is: are there obvious reasons why this commit might have increased the parsing time of the example by a factor of about 10? Is it possible to undo the changes introduced by 5a937cc and check whether this brings back reasonable parsing times? |
|
@nicolabotta So I think major rule that was added was |
|
@nicolabotta To be honest, I am not sure how to proceed. I think that if there is going to be some rollback then I would guess it has to be done by @edwinb. Alternatively, the parser needs to be rewritten, but working on Idris is not my primary job (I contribute a bit during breaks) and I unfortunately have too much work to be able to do so soon. |
|
I can take a look at it after work. First thing is just to make a profile
|
|
@melted Sounds great, thanks! I'll try to find out whether the commit has also affected the parsing time of other expressions. But at the first glance it seems that the major impact has been on equational reasoning proofs. One thing that I can say is that eliminating all explicit implicit arguments of not their justifications. The parsing time also seems to be reasonably linear in the number of such expressions: it takes roughly 30 seconds per line! |
|
Ok, I think I know what it is. The expression parser has a number of "try"s that are recursive, that is they contain a parse of another expression. That will make Idris do something like a depth-first search with loads of backtracking for big expressions. This can be fixed by restricting the scope of the trys so they aren't recursive. I made a census and most of them seem straightforward. There is one important place I need to think some more, This was obviously not caused by the commit mentioned above, it just made it worse. 40s is way too long for a parse too. |
|
@melted Thanks Niklas, that looks very promising! |
|
The reason that it is slower from that commit is that it tries constraintPi before unboundPi on line 1140 in Parser/Expr.idr, unfortunately they can't simply be inverted as there are constraint lists for which the unboundPi parse would succeed. And a constraint list can contain whatever as long as it's comma separated and is followed by "=>", so that alternative isn't ever rejected out of hand. |
|
I think the best bet here is to let constraint parser also handle the case where it finds itself with an opExpr and no following "=>", then there will be no backtracking. |
|
But of course that doesn't work because an opExpr in a constraint can't contain implicits. |
|
There is plenty of low-hanging fruit to improve performance in the expression parser, this isn't one of them. |
|
I knew there were issues with the parser which made it hard to change, but I was hoping that a set of new eyes could see if there was an easy fix. |
|
I added a check that an unboundPi wasn't a constraint list, by putting in a check for "=>". Then I could put it first and restore the performance. It still isn't good of course, but one thing at a time. |
Thanks for addressing this issue Niklas! Is it really the case that you have managed to restore the parsing times to the values before commit 5a937cc? With 635d448 (the latest commit) I am still getting parsing times of about 5 minutes for the example above. Best, Nicola |
|
That's probably because I haven't merged the PR yet :)
|
|
I can confirm that we are now back to more human parsing and type checking times: from 5 minutes to 40 seconds for the example and from 25 to 15 minutes for the |
With 0.11.2-git:fc3e88c and on my machine, it takes almost 5 minutes for
to fail to type check:
! Thus, parsing proofs based on preorder reasoning does not scale up anymore. Slightly longer expressions yield unacceptable type checking times.
As shown in #3208, this is the major reason for the extremely long type checking times originally reported in #3197.
I have been routinely type checking this and similar examples (with suitable
importdirectives) since months but, if I am not mistaken, the issue has come up (or worsened) only recently.Any idea how to circumvent this problem? Thanks, Nicola
The text was updated successfully, but these errors were encountered: