package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.1.3.v8.16.tbz
sha256=d6d589ae18453d9251b4250df50e59cfc87254de0e4734e13c5bca06ab14cee5
sha512=802b4673c7f581976526a3cb4bd824f7574c5b1cc8fcc7759fcd3358cdc3e4cebef3ec908899ad68129190777ccda931dfc1643b45db156ede15acae0382c148
doc/src/coq-lsp.coq/workspace.ml.html
Source file workspace.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 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) (************************************************************************) (* Coq Language Server Protocol *) (* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) (* Copyright 2019-2022 Inria -- Dual License LGPL 2.1 / GPL3+ *) (* Written by: Emilio J. Gallego Arias *) (************************************************************************) type t = { coqlib : string ; vo_load_path : Loadpath.vo_path list ; ml_include_path : string list ; require_libs : (string * string option * Vernacexpr.export_with_cats option) list ; indices_matter : bool ; impredicative_set : bool ; kind : string } let default ~implicit ~coqlib ~kind = let mk_path prefix = coqlib ^ "/" ^ prefix in let mk_lp ~ml ~root ~dir ~implicit = { Loadpath.unix_path = mk_path dir ; coq_path = root ; has_ml = ml ; implicit ; recursive = true } in let coq_root = Names.DirPath.make [ Libnames.coq_root ] in let default_root = Libnames.default_root_prefix in let require_libs = [ ("Coq.Init.Prelude", None, Some (Lib.Import, None)) ] in { coqlib ; vo_load_path = [ mk_lp ~ml:false ~root:coq_root ~implicit ~dir:"theories" ; mk_lp ~ml:true ~root:default_root ~implicit:false ~dir:"user-contrib" ] ; ml_include_path = (let unix_path = Filename.concat coqlib "../coq-core/plugins" in System.all_subdirs ~unix_path |> List.map fst) ; require_libs ; indices_matter = false ; impredicative_set = false ; kind } let add_loadpaths base ~vo_load_path ~ml_include_path = { base with vo_load_path = base.vo_load_path @ vo_load_path ; ml_include_path = base.ml_include_path @ ml_include_path } let pp_load_path fmt { Loadpath.unix_path; coq_path; implicit = _; has_ml = _; recursive = _ } = Format.fprintf fmt "Path %s ---> %s" (Names.DirPath.to_string coq_path) unix_path let describe { coqlib; kind; vo_load_path; ml_include_path; require_libs; _ } = let require_msg = String.concat " " (List.map (fun (s, _, _) -> s) require_libs) in let n_vo = List.length vo_load_path in let n_ml = List.length ml_include_path in let extra = Format.asprintf "@[vo_paths:@\n @[<v>%a@]@\nml_paths:@\n @[<v>%a@]@]" (Format.pp_print_list pp_load_path) vo_load_path Format.(pp_print_list pp_print_string) ml_include_path in ( Format.asprintf "@[Configuration loaded from %s@\n\ \ - coqlib is at: %s@\n\ \ - Modules [%s] will be loaded by default@\n\ \ - %d Coq path directory bindings in scope; %d Coq plugin directory \ bindings in scope@]" kind coqlib require_msg n_vo n_ml , extra ) let rec parse_args args init w = match args with | [] -> (init, w) | "-indices-matter" :: rest -> parse_args rest init { w with indices_matter = true } | "-impredicative-nset" :: rest -> parse_args rest init { w with impredicative_set = true } | "-noinit" :: rest -> parse_args rest false w | _ :: rest -> (* emit warning? *) parse_args rest init w (* Require a set of libraries *) let load_objs libs = let rq_file (dir, from, exp) = let mp = Libnames.qualid_of_string dir in let mfrom = Option.map Libnames.qualid_of_string from in Flags.silently (Vernacentries.vernac_require mfrom exp) [ (mp, Vernacexpr.ImportAll) ] in List.(iter rq_file (rev libs)) (* NOTE: Use exhaustive match below to avoid bugs by skipping fields *) let apply ~libname { coqlib = _ ; vo_load_path ; ml_include_path ; require_libs ; indices_matter ; impredicative_set ; kind = _ } = Global.set_indices_matter indices_matter; Global.set_impredicative_set impredicative_set; List.iter Mltop.add_ml_dir ml_include_path; List.iter Loadpath.add_vo_path vo_load_path; Declaremods.start_library libname; load_objs require_libs let workspace_from_coqproject ~coqlib : t = (* Io.Log.error "init" "Parsing _CoqProject"; *) let open CoqProject_file in let to_vo_loadpath f implicit = let open Loadpath in let unix_path, coq_path = f in (* Lsp.Io.log_error "init" * (Printf.sprintf "Path from _CoqProject: %s %s" unix_path.path coq_path); *) { implicit ; recursive = true ; has_ml = false ; unix_path = unix_path.path ; coq_path = Libnames.dirpath_of_string coq_path } in let { r_includes; q_includes; ml_includes; extra_args; _ } = read_project_file ~warning_fn:(fun _ -> ()) "_CoqProject" in let ml_include_path = List.map (fun f -> f.thing.path) ml_includes in let vo_path = List.map (fun f -> to_vo_loadpath f.thing false) q_includes in let vo_load_path = List.append vo_path (List.map (fun f -> to_vo_loadpath f.thing true) r_includes) in let args = List.map (fun f -> f.thing) extra_args in let implicit = true in let kind = Filename.concat (Sys.getcwd ()) "_CoqProject" in let workspace = default ~coqlib ~implicit ~kind in let init, workspace = parse_args args true workspace in let workspace = if not init then { workspace with require_libs = [] } else workspace in add_loadpaths workspace ~vo_load_path ~ml_include_path module CmdLine = struct type t = { coqlib : string ; vo_load_path : Loadpath.vo_path list ; ml_include_path : string list } end let workspace_from_cmdline { CmdLine.coqlib; vo_load_path; ml_include_path } = let kind = "Command-line arguments" in let implicit = true in let w = default ~implicit ~coqlib ~kind in add_loadpaths w ~vo_load_path ~ml_include_path let guess ~cmdline = if Sys.file_exists "_CoqProject" then workspace_from_coqproject ~coqlib:cmdline.CmdLine.coqlib else workspace_from_cmdline cmdline
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>