package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file args.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
(*************************************************************************)
(* Copyright 2015-2019 MINES ParisTech -- Dual License LGPL 2.1+ / GPL3+ *)
(* Copyright 2019-2024 Inria           -- Dual License LGPL 2.1+ / GPL3+ *)
(* Copyright 2024-2025 Emilio J. Gallego Arias  -- LGPL 2.1+ / GPL3+     *)
(* Copyright 2025      CNRS                     -- LGPL 2.1+ / GPL3+     *)
(* Written by: Emilio J. Gallego Arias & coq-lsp contributors            *)
(*************************************************************************)
(* Rocq Language Server Protocol: Rocq arguments API                     *)
(*************************************************************************)

open Cmdliner

(* [Boot.Util.relocate] is too specific to rocq.exe for it to work, EJGA: this
   needs likely more attention in our case, but OMMV *)
let coqlib_dyn =
  match Coq_config.coqlib with
  | NotRelocatable p -> p
  | Relocatable p ->
    let paths =
      match Sys.getenv_opt "PATH" with
      | None -> []
      | Some paths ->
        let sep = if Coq_config.arch_is_win32 then ';' else ':' in
        String.split_on_char sep paths
    in
    let name =
      if Sys.(os_type = "Win32" || os_type = "Cygwin") then "rocq.exe"
      else "rocq"
    in
    let bindir = fst (System.find_file_in_path ~warn:false paths name) in
    Filename.concat (Filename.concat bindir "..") p

(****************************************************************************)
(* Common Coq command-line arguments *)
let coqlib =
  let doc =
    "Load Coq.Init.Prelude from $(docv); theories and user-contrib should live \
     there."
  in
  Arg.(value & opt string coqlib_dyn & info [ "coqlib" ] ~docv:"COQLIB" ~doc)

let findlib_config =
  let doc = "Override findlib's config file" in
  Arg.(
    value
    & opt (some string) None
    & info [ "findlib_config" ] ~docv:"OCAMLFIND_CONF" ~doc)

let ocamlpath =
  let doc = "Extra Paths to OCaml's libraries" in
  Arg.(
    value & opt (list string) [] & info [ "ocamlpath" ] ~docv:"OCAMLPATH" ~doc)

let coq_lp_conv ~implicit (unix_path, lp) =
  { Loadpath.coq_path = Libnames.dirpath_of_string lp
  ; unix_path
  ; implicit
  ; installed = false
  ; recursive = true
  }

let rload_paths : Loadpath.vo_path list Term.t =
  let doc =
    "Bind a logical loadpath LP to a directory DIR and implicitly open its \
     namespace."
  in
  Term.(
    const List.(map (coq_lp_conv ~implicit:true))
    $ Arg.(
        value
        & opt_all (pair dir string) []
        & info [ "R"; "rec-load-path" ] ~docv:"DIR,LP" ~doc))

let qload_paths : Loadpath.vo_path list Term.t =
  let doc = "Bind a logical loadpath LP to a directory DIR" in
  Term.(
    const List.(map (coq_lp_conv ~implicit:false))
    $ Arg.(
        value
        & opt_all (pair dir string) []
        & info [ "Q"; "load-path" ] ~docv:"DIR,LP" ~doc))

let debug : bool Term.t =
  let doc = "Enable debug mode" in
  Arg.(value & flag & info [ "debug" ] ~doc)

let bt =
  let doc = "Enable backtraces" in
  Cmdliner.Arg.(value & flag & info [ "bt" ] ~doc)

let ri_from : (string option * string) list Term.t =
  let doc =
    "FROM Require Import LIBRARY before creating the document, à la From Coq \
     Require Import Prelude"
  in
  Term.(
    const (List.map (fun (x, y) -> (Some x, y)))
    $ Arg.(
        value
        & opt_all (pair string string) []
        & info [ "rifrom"; "require-import-from" ] ~docv:"FROM,LIBRARY" ~doc))

let int_backend =
  let docv = "BACKEND" in
  let backends = [ ("Coq", Limits.Coq); ("Mp", Limits.Mp) ] in
  let backends_str =
    "either 'Mp', for memprof-limits token-based interruption,\n\
    \  or 'Coq', for Coq's polling mode (unreliable). The 'Mp' backend is only \
     supported in OCaml 4.x series."
  in
  let doc =
    Printf.sprintf
      "Select Interruption Backend, if absent, the best available for your \
       OCaml version will be selected. %s is %s"
      docv backends_str
  in
  let absent = "'Mp' for OCaml 4.x, 'Coq' for OCaml 5.x" in
  Arg.(
    value
    & opt (some (enum backends)) None
    & info [ "int_backend" ] ~docv ~doc ~absent)

let roots : string list Term.t =
  let doc = "Workspace(s) root(s)" in
  Arg.(value & opt_all string [] & info [ "root" ] ~docv:"ROOTS" ~doc)

let coq_diags_level : int Term.t =
  let doc =
    "Controls whether Coq Info and Notice message appear in diagnostics.\n\
    \ 0 = None; 1 = Notices, 2 = Notices and Info"
  in
  Arg.(value & opt int 0 & info [ "diags_level" ] ~docv:"DIAGS_LEVEL" ~doc)