Skip to content

Commit

Permalink
[serapi] Add document creation NewDoc protocol call.
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
ejgallego committed Nov 29, 2018
1 parent 82c7dc8 commit 49545fc
Show file tree
Hide file tree
Showing 19 changed files with 597 additions and 417 deletions.
3 changes: 3 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 15,9 @@ _Version 0.6.0_:
@palmskog,
* [sercomp] add `--mode` option to better control output,
* [sercomp] add `compser` for deserialization (inverse of `sercomp`)
* [serapi] Allow custom document creation using the `NewDoc` call.
Use the `--no_init` option to avoid automatic creation
on init. (@ejgallego)

_Version 0.5.7_:

Expand Down
41 changes: 41 additions & 0 deletions serapi/serapi_paths.ml
Original file line number Diff line number Diff line change
@@ -0,0 1,41 @@
(************************************************************************)
(* * 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 serialization API/Plugin *)
(* Copyright 2016-2018 MINES ParisTech -- Dual License LGPL 2.1 / GPL3 *)
(* Written by: Emilio J. Gallego Arias *)
(************************************************************************)
(* Status: Very Experimental *)
(************************************************************************)

(******************************************************************************)
(* Coq Prelude Loading Defaults (to be improved) *)
(******************************************************************************)

let coq_loadpath_default ~implicit ~coq_path =
let open Mltop in
let mk_path prefix = coq_path ^ "/" ^ prefix in
let mk_lp ~ml ~root ~dir ~implicit =
{ recursive = true;
path_spec = VoPath {
unix_path = mk_path dir;
coq_path = root;
has_ml = ml;
implicit;
};
} in
(* in 8.8 we can use Libnames.default_* *)
let coq_root = Names.DirPath.make [Libnames.coq_root] in
let default_root = Libnames.default_root_prefix in
[mk_lp ~ml:AddRecML ~root:coq_root ~implicit ~dir:"plugins";
mk_lp ~ml:AddNoML ~root:coq_root ~implicit ~dir:"theories";
mk_lp ~ml:AddRecML ~root:default_root ~implicit:false ~dir:"user-contrib";
]
20 changes: 20 additions & 0 deletions serapi/serapi_paths.mli
Original file line number Diff line number Diff line change
@@ -0,0 1,20 @@
(************************************************************************)
(* * 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 serialization API/Plugin *)
(* Copyright 2016-2018 MINES ParisTech -- Dual License LGPL 2.1 / GPL3 *)
(* Written by: Emilio J. Gallego Arias *)
(************************************************************************)
(* Status: Very Experimental *)
(************************************************************************)

(* Default load path for Coq's stdlib *)
val coq_loadpath_default : implicit:bool -> coq_path:string -> Mltop.coq_path list
34 changes: 33 additions & 1 deletion serapi/serapi_protocol.ml
Original file line number Diff line number Diff line change
Expand Up @@ -667,6 667,22 @@ module ControlUtil = struct

end

(******************************************************************************)
(* Init / new document *)
(******************************************************************************)
type newdoc_opts = {

(* name of the top-level module *)
top_name : string;

(* Initial LoadPath. [XXX: Use the coq_pkg record?] *)
iload_path : Mltop.coq_path list sexp_option;

(* Libs to require in STM init *)
require_libs : (string * string option * bool option) list sexp_option;

}

(******************************************************************************)
(* Help *)
(******************************************************************************)
Expand All @@ -689,6 705,7 @@ let serproto_help () =
(******************************************************************************)

type cmd =
| NewDoc of newdoc_opts
| Add of add_opts * string
| Cancel of Stateid.t list
| Exec of Stateid.t
Expand All @@ -711,6 728,22 @@ type cmd =
let exec_cmd (cmd : cmd) =
let doc = Stm.get_doc !doc_id in
coq_protect @@ fun () -> match cmd with
| NewDoc opts ->
let open Names in
let sertop_dp = DirPath.make [Id.of_string opts.top_name] in
let stm_options = Stm.AsyncOpts.default_opts in
let require_libs = Option.default (["Coq.Init.Prelude", None, Some true]) opts.require_libs in
let iload_path = Option.default
Serapi_paths.(coq_loadpath_default ~implicit:true ~coq_path:Coq_config.coqlib)
opts.iload_path in
let ndoc = { Stm.doc_type = Stm.Interactive sertop_dp
; require_libs
; iload_path
; stm_options
} in
(* doc_id := fst Stm.(get_doc @@ new_doc ndoc); [] *)
let _ = Stm.new_doc ndoc in
doc_id := 0; []
| Add (opt, s) -> snd @@ ControlUtil.add_sentences ~doc opt s
| Cancel st -> List.concat @@ List.map (fun x -> snd @@ ControlUtil.(cancel_sentence ~doc x)) st
| Exec st -> ignore(Stm.observe ~doc st); []
Expand Down Expand Up @@ -751,4 784,3 @@ type tagged_cmd = cmd_tag * cmd
type answer =
| Answer of cmd_tag * answer_kind
| Feedback of Feedback.feedback

20 changes: 18 additions & 2 deletions serapi/serapi_protocol.mli
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 27,7 @@ open Sexplib.Conv
(* Basic Protocol Objects *)
(******************************************************************************)
type coq_object =
CoqString of string
| CoqString of string
| CoqSList of string list
| CoqPp of Pp.t
(* | CoqRichpp of Richpp.richpp *)
Expand Down Expand Up @@ -146,6 146,22 @@ type add_opts = {
verb : bool [@default false];
}

(******************************************************************************)
(* Init / new document *)
(******************************************************************************)
type newdoc_opts = {

(* name of the top-level module *)
top_name : string;

(* Initial LoadPath. [XXX: Use the coq_pkg record?] *)
iload_path : Mltop.coq_path list sexp_option;

(* Libs to require in STM init *)
require_libs : (string * string option * bool option) list sexp_option;

}

(******************************************************************************)
(* Help *)
(******************************************************************************)
Expand All @@ -157,6 173,7 @@ type add_opts = {
(******************************************************************************)

type cmd =
| NewDoc of newdoc_opts
| Add of add_opts * string
| Cancel of Stateid.t list
| Exec of Stateid.t
Expand Down Expand Up @@ -200,4 217,3 @@ type answer =
(* implicit : bool; *)
(* async : Sertop_init.async_flags; *)
(* } *)

37 changes: 37 additions & 0 deletions serlib/ser_mltop.ml
Original file line number Diff line number Diff line change
@@ -0,0 1,37 @@
(************************************************************************)
(* * 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 serialization API/Plugin *)
(* Copyright 2016-2018 MINES ParisTech *)
(* Written by: Emilio J. Gallego Arias *)
(************************************************************************)
(* Status: Very Experimental *)
(************************************************************************)

open Sexplib.Conv

module Names = Ser_names

type add_ml =
[%import: Mltop.add_ml]
[@@deriving sexp]

type vo_path_spec =
[%import: Mltop.vo_path_spec]
[@@deriving sexp]

type coq_path_spec =
[%import: Mltop.coq_path_spec]
[@@deriving sexp]

type coq_path =
[%import: Mltop.coq_path]
[@@deriving sexp]
Loading

0 comments on commit 49545fc

Please sign in to comment.