lambdapi
lambdapi copied to clipboard
Deducteam
Performance slowdown with version 2.1.0
Hi everyone,
trying to port my lambdapi programs to version 2.2.0, I noticed a slowdown in the verification. It seems like the issue appeared between version 2.0.0 and 2.1.0. Making the example as concise as possible required about 40 quantified hypotheses to make it clear but in my use case it appears much faster.
On my machine, running lambdapi on the content of quant_hyp_test.txt takes:
- 0.2s with version 2.0.0
- 13.3s with version 2.1.0.
Have a nice Easter Monday :)
Hi Quentin. He doesn't surprise me. The introduction of term refinement (in order to add coercions) was known to introduce an important slow down. See https://github.com/Deducteam/lambdapi/blob/master/CHANGES.md. How important is it for your whole development?
Its quite severe: my whole test suite for lambdapi used to go through in 15s and with version 2.1.0 it now takes 4m21s.
Also, it seems like there is something that has an exponential complexity. Here are the results for the modified test given above:
| size (nb of variables) | 10 | 15 | 20 | 25 | 30 | 35 |
|---|---|---|---|---|---|---|
| time (s) | 0.16 | 0.36 | 0.84 | 1.9 | 3.8 | 7.0 |
This is problematic indeed. Unfortunately, we do not have the time to look after this at the moment. Gabriel is ending the writing of his PhD, and I am myself busy with many things too. Not sure that we can look at this before September... :-(
No problem, I can simply use version 2.0.0 for now. I wish good luck to you and to Gabriel :)
I would also like to move on to other things, and I think giving you the basis of my lambdapi development might help. Would you consider adding it as an example ? For now it doesn't compile, because of issues #862 and #861, but I can give it to you when they are resolved ?
Sure, we can add them in tests. But please consider adding your LP developments on https://github.com/Deducteam/opam-lambdapi-repository.