search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
150 stars 31 forks source link

Fix help printing #754

Closed ineol closed 4 months ago

ineol commented 4 months ago

Currently, coq-lsp --help crashed because Cmdliner cannot print the default option for --int-backend

It would be nicer to have help print the possible values of the enum, but I couldn't figure out how.

ejgallego commented 4 months ago

Oh! What a silly bug!

Thanks a lot for the fix.

There is also this option, printing the values as you suggest. It also avoids the dummy auto argument.

  let backends = [ ("Coq", Limits.Coq); ("Mp", Limits.Mp) ] in
  let docv = Cmdliner.Arg.doc_alts_enum ~quoted:true backends in
  Arg.(
    value
    & opt (some (enum backends)) None
    & info [ "int_backend" ] ~docv ~doc)
ineol commented 4 months ago

This version prints

      --int_backend=BACKEND (absent='Mp' for OCaml 4.x, 'Coq' for OCaml 5.x)
           Select Interruption Backend, if absent, the best available for
           your OCaml version will be selected. BACKEND is either 'Mp', for
           memprof-limits token-based interruption, or 'Coq', for Coq's
           polling mode (unreliable). The 'Mp' backend is only supported in
           OCaml 4.x series.

which seems clear