From 0ae62a0d91e99a71b9c9611e1d0aa7c907f9fc57 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Tue, 24 Dec 2024 12:28:00 +0200 Subject: [PATCH] Make the LSP independent of level assignment. The fingerprint calculation reverted to is_const (as it is now done in the main branch) instead of get_level to make the fingerprint calculation independent of the level assignment. This is done to avoid having level assignments on the critical path in the LSP, as it is too slow. In my case, it took 30 seconds to calculate the levels, which blocks subsequent LSP commands. Signed-off-by: Karolis Petrauskas --- .ocamlformat | 2 +- lsp/lib/docs/proof_step.ml | 4 +++- src/backend/fingerprints.ml | 7 ++++++- 3 files changed, 10 insertions(+), 3 deletions(-) diff --git a/.ocamlformat b/.ocamlformat index 8adea03e..f2116634 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,2 +1,2 @@ -version=0.26.2 +version=0.27.0 profile=default diff --git a/lsp/lib/docs/proof_step.ml b/lsp/lib/docs/proof_step.ml index 245061db..02df0b94 100644 --- a/lsp/lib/docs/proof_step.ml +++ b/lsp/lib/docs/proof_step.ml @@ -370,7 +370,9 @@ let of_module (mule : Tlapm_lib.Module.T.mule) prev : t option = proof status between the modifications. *) let o = match o.fingerprint with - | None -> Tlapm_lib.Backend.Prep.prepare_obligation o + | None -> + (* `Tlapm_lib.Backend.Prep.prepare_obligation o` works too slow here. *) + Tlapm_lib.Backend.Fingerprints.write_fingerprint o | Some _ -> o in let o = Obl.of_parsed_obligation o Proof_status.Pending in diff --git a/src/backend/fingerprints.ml b/src/backend/fingerprints.ml index 9bbf7cb9..db9633b2 100644 --- a/src/backend/fingerprints.ml +++ b/src/backend/fingerprints.ml @@ -446,9 +446,14 @@ and fp_sequent stack buf sq = spin stack cx; let v,r = Stack.pop stack in if !r then + (* Here `Expr.Levels.get_level e` was used instead of + `if Expr.Constness.is_const e then 0 else 3`, + but that introduces a dependency on having the levels + assigned before calculating fingerprints. The former is + slow and thus is problematic to use in LSP. *) bprintf buf "$Def(%d,%d)" (match v with Identhypi i -> i | _ -> assert false) - (Expr.Levels.get_level e) + (if Expr.Constness.is_const e then 0 else 3) | Defn ({core = Bpragma (nm, _, _)}, _, Hidden, _) -> Stack.push stack (IdentBPragma nm.core, ref false); spin stack cx;