LSP type naming inconsistency

[kaifronsdal]

Several of the type fields used in the coq lsp extensions (described in editor/code/lib/types.ts) are inconsistently named. The general lsp naming conventions are to use camel case for everything (with the exception of some constants such as TM_CURRENT_LINE). However, the type definitions in coq-lsp sometimes switch to snake case.

Additionally, lsp type names are typically very descriptive, even at the expense of brevity. For example, CodeLensWorkspaceClientCapabilities or TextDocumentSaveRegistrationOptions. Many of the type names and type fields in coq-lsp break this convention. A few example of what I mean include Loc, Loc.bp, Loc.ep, Hyp.ty, SentencePerfParams, and SentencePerfParams.mem.

My recommendation is to standardize the naming conventions to always use camel case and to not use acronyms or shorten names. This would improve readability for users and make it easier to understand the purpose of each field without referring to the source code. As it stands, I am still not sure what Loc.bp is.

In the case where there would be a naming conflict, such as with renaming Loc with Location, perhaps as an alternative we could use a name such as CoqLocation or instead use the standard lsp Location format of {uri: DocumentUri, range: Range}.

[ejgallego]

Thanks for the feedback @kaifronsdal . Indeed the convention we use in ocaml is snake case which is the standard in many industrial Ocaml projects.

I think your recommendation makes a lot of sense, I've scheduled the fix to the upcoming 0.2.0 release as not to break the couple API users there.

[ejgallego]

Hi @kaifronsdal , what alternative would you propose for SentencePerfParams ?

[ejgallego]

The notification is called perf , so I dunno