The protocol now supports a call:
```
(NewDoc ((top_name "Module")
         (iload_path (path_1 ... path_n)
         (require_libs (require_1 ... require_n))))
```
where `path_i` is of type
```
Mltop.coq_path = {
  path_spec: coq_path_spec;
  recursive: bool;
}

type coq_path_spec =
  | VoPath of vo_path_spec
  | MlPath of string

type vo_path_spec = {
  unix_path : string;
  coq_path  : Names.DirPath.t;
  implicit  : bool;
  has_ml    : add_ml;
}
```
and `require_i` is of type:
```
string * string option * bool option
```
where `(module, root, import)` corresponds to `From root Require import module`

`iload_path` and `require_libs` are optional, if absent, SerAPI will
resort to the defaults.

By default, invoking `sertop` will create a document with the standard
paths and `Prelude` loaded. To avoid that, use the commit line option
`--no_init`.

This PR improves a certain number of things, including `compser` and
`sercomp` will now create documents with the proper module path cc: #84.

This also improves #49 and #59.

The protocol now supports a method:
```
(NewDoc ((top_name "Module")
         (iload_path (path_1 ... path_n)
         (require_libs (require_1 ... require_n))))
```
where `path_i` is of type
```
Mltop.coq_path = {
  path_spec: coq_path_spec;
  recursive: bool;
}

type coq_path_spec =
  | VoPath of vo_path_spec
  | MlPath of string

type vo_path_spec = {
  unix_path : string;
  coq_path  : Names.DirPath.t;
  implicit  : bool;
  has_ml    : add_ml;
}
```
and `require_i` is of type:
```
string * string option * bool option
```
where `(module, root, import)` corresponds to `From root Require import module`

`iload_path` and `require_libs` are optional, if absent, SerAPI will
resort to the defaults.

By default, invoking `sertop` will create a document with the standard
paths and `Prelude` loaded. To avoid that, use the commit line option
`--no_init`.

This PR improves a certain number of things, including `compser` and
`sercomp` will now create documents with the proper module path cc: #84.

This also improves #49 and #59.

The protocol now supports a method:
```
(NewDoc ((top_name "Module")
         (iload_path (path_1 ... path_n)
         (require_libs (require_1 ... require_n))))
```
where `path_i` is of type
```
Mltop.coq_path = {
  path_spec: coq_path_spec;
  recursive: bool;
}

type coq_path_spec =
  | VoPath of vo_path_spec
  | MlPath of string

type vo_path_spec = {
  unix_path : string;
  coq_path  : Names.DirPath.t;
  implicit  : bool;
  has_ml    : add_ml;
}
```
and `require_i` is of type:
```
string * string option * bool option
```
where `(module, root, import)` corresponds to `From root Require import module`

`iload_path` and `require_libs` are optional, if absent, SerAPI will
resort to the defaults.

By default, invoking `sertop` will create a document with the standard
paths and `Prelude` loaded. To avoid that, use the commit line option
`--no_init`. **Important** in practice the user still can only use
this option to create one single document using `NewDoc`, as the
protocol doesn't yet include per-document addressing.

This PR improves a certain number of things, including `compser` and
`sercomp` will now create documents with the proper module path cc: #84.

This also improves #49 and #59.

Thanks to everyone that helped and used this project for almost 7
years!

The following issues are solved by coq-lsp:

closes #252, closes #261, closes #234, closes #202, closes #117,
closes #49, closes #32, closes #26, closes #24, closes #13

Thanks to everyone that helped and used this project for almost 7
years!

The following issues are solved by coq-lsp:

closes #252, closes #261, closes #234, closes #202, closes #117,
closes #49, closes #32, closes #26, closes #24, closes #21,
closes #18, closes #13

Thanks to everyone that helped and used this project for almost 7
years!

The following issues are solved by coq-lsp:

closes #252, closes #261, closes #234, closes #202, closes #117,
closes #49, closes #32, closes #26, closes #24, closes #21,
closes #18, closes #13