Merge updated_enabled_cdot.

[kape1395]

Here is an attempt to merge old branch updated_enabled_cdot.

[kape1395]

The LSP server currently fails with

LSP request failed with exception Not_found, backtrace:
Raised at Stdlib__List.find in file "list.ml", line 232, characters 10-25
Called from Tlapm_lib__Property.get in file "src/util/property.ml", line 71, characters 9-54
Called from Tlapm_lib__E_levels.get_level_info in file "src/expr/e_levels.ml" (inlined), line 68, characters 23-47
Called from Tlapm_lib__E_levels.get_level in file "src/expr/e_levels.ml", line 70, characters 21-37
Called from Tlapm_lib__Fingerprints.fp_sequent.spin in file "src/backend/fingerprints.ml", line 446, characters 23-48
Called from Tlapm_lib__Fingerprints.fp_sequent.spin in file "src/backend/fingerprints.ml", line 441, characters 13-26
...

It seems like the levels are not assigned somewhere.

[kape1395]

@muenchnerkindl, @damiendoligez, who could review this PR?

[damiendoligez]

Looks good modulo a few suggestions.

[kape1395]

I accepted all the suggested changes and merged the changes from the main branch.

[kape1395]

With these changes, the parsing became slower.
For a document I work on, it takes 0.5 seconds to parse it on the main and 1.3 seconds on this branch.

However, from the LSP server perspective, the lag is even longer (10 or more seconds). I will investigate what makes it so slow.

[kape1395]

For the record on the performance.

This line

tlapm/lsp/lib/docs/proof_step.ml

Line 381 in 07d8ce0

let obs = List.filter_map mule_obl (Array.to_list obs) in

now takes 30 seconds on my document (855 LOC).

This PR changed a call (in the body of mule_obl)

Tlapm_lib.Backend.Fingerprints.write_fingerprint o

with

Tlapm_lib.Backend.Prep.prepare_obligation o

to have proof methods assigned properly.

[kape1395]

Here is the flame graph from a profiler.

[kape1395]

add_expr_level also takes almost half of the TLAPM execution time in the normal (non-lsp) execution.

@damiendoligez, do you know if that's expected? Should I look to make the add_expr_level much faster or try to avoid it in the critical path in the LSP execution? Currently, it makes the LSP unusable on a bit larger proofs.

[kape1395]

I opened #186 to this branch to avoid having the level checking in the critical path of the LSP.