Skip to content

Commit 0ae62a0

Browse files
committed
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 <[email protected]>
1 parent 07d8ce0 commit 0ae62a0

File tree

3 files changed

+10
-3
lines changed

3 files changed

+10
-3
lines changed

.ocamlformat

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
1-
version=0.26.2
1+
version=0.27.0
22
profile=default

lsp/lib/docs/proof_step.ml

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -370,7 +370,9 @@ let of_module (mule : Tlapm_lib.Module.T.mule) prev : t option =
370370
proof status between the modifications. *)
371371
let o =
372372
match o.fingerprint with
373-
| None -> Tlapm_lib.Backend.Prep.prepare_obligation o
373+
| None ->
374+
(* `Tlapm_lib.Backend.Prep.prepare_obligation o` works too slow here. *)
375+
Tlapm_lib.Backend.Fingerprints.write_fingerprint o
374376
| Some _ -> o
375377
in
376378
let o = Obl.of_parsed_obligation o Proof_status.Pending in

src/backend/fingerprints.ml

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -446,9 +446,14 @@ and fp_sequent stack buf sq =
446446
spin stack cx;
447447
let v,r = Stack.pop stack in
448448
if !r then
449+
(* Here `Expr.Levels.get_level e` was used instead of
450+
`if Expr.Constness.is_const e then 0 else 3`,
451+
but that introduces a dependency on having the levels
452+
assigned before calculating fingerprints. The former is
453+
slow and thus is problematic to use in LSP. *)
449454
bprintf buf "$Def(%d,%d)"
450455
(match v with Identhypi i -> i | _ -> assert false)
451-
(Expr.Levels.get_level e)
456+
(if Expr.Constness.is_const e then 0 else 3)
452457
| Defn ({core = Bpragma (nm, _, _)}, _, Hidden, _) ->
453458
Stack.push stack (IdentBPragma nm.core, ref false);
454459
spin stack cx;

0 commit comments

Comments
 (0)