search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
143 stars 31 forks source link

[fleche] Handle performance data correctly for cached sentences #693

Closed ejgallego closed 4 months ago

ejgallego commented 4 months ago

We extend Memo as to store the original performance execution data, this way, we can display it correctly, and we distinguish the case where a sentence was memoized better.

This is a fix, because before we would display the wrong data for incremental checking.

This is complementary to #686 and #689.

We cherry pick the protocol fixes from #689 as to have this PR in mergeable / testeable shape.