Make the LSP independent of level assignment.

.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;