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]>

.ocamlformat

@@ -1,2 +1,2 @@
-version=0.26.2
+version=0.27.0
 profile=default

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

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;