diff --git a/CHANGES.md b/CHANGES.md index bcc7ad96..dacded90 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,11 @@ +# unreleased +------------ + + - [deps] Bump toolchain so minimal `ppxlib` is 0.26, in order to fix + some `ppx_import` oddities. This means our lower bound for the Jane + Street packages is now `v0.15`, which should be fine for the + foreseeable future (@ejgallego, #813) + # coq-lsp 0.2.0: From Green to Blue ----------------------------------- diff --git a/coq-lsp.opam b/coq-lsp.opam index cf4ddd26..950f6166 100644 --- a/coq-lsp.opam +++ b/coq-lsp.opam @@ -34,23 +34,23 @@ depends: [ "menhir" { >= "20220210" } # unit testing - "ppx_inline_test" { >= "0.14.1" } + "ppx_inline_test" { >= "v0.15.0" } # Uncomment this for releases # "coq" { >= "8.17" < "8.18" } # coq deps: remove this for releases - "ocamlfind" {>= "1.8.1"} - "zarith" {>= "1.11"} + "ocamlfind" {>= "1.9.1"} + "zarith" {>= "1.13"} # serlib deps: see what we need to keep for release - "ppx_deriving" { >= "4.2.1" } - "ppx_deriving_yojson" { >= "3.4" } - "ppx_import" { >= "1.5-3" } - "sexplib" { >= "v0.13.0" & < "v0.18" } - "ppx_sexp_conv" { >= "v0.13.0" & < "v0.18" } - "ppx_compare" { >= "v0.13.0" & < "v0.18" } - "ppx_hash" { >= "v0.13.0" & < "v0.18" } + "ppx_deriving" { >= "5.2" } + "ppx_deriving_yojson" { >= "3.7.0" } + "ppx_import" { >= "1.11.0" } + "sexplib" { >= "v0.15.0" & < "v0.18" } + "ppx_sexp_conv" { >= "v0.15.0" & < "v0.18" } + "ppx_compare" { >= "v0.15.0" & < "v0.18" } + "ppx_hash" { >= "v0.15.0" & < "v0.18" } ] depopts: ["lwt" "logs"] diff --git a/lsp/jLang.ml b/lsp/jLang.ml index 7df98eb9..e5490703 100644 --- a/lsp/jLang.ml +++ b/lsp/jLang.ml @@ -88,3 +88,26 @@ module Diagnostic = struct let message = Pp.to_string message in _t_to_yojson { range; severity; message; data } end + +module Stdlib = JStdlib + +module With_range = struct + type 'a t = [%import: ('a Lang.With_range.t[@with Lang.Range.t := Range.t])] + [@@deriving yojson] +end + +module Ast = struct + module Name = struct + type t = [%import: Lang.Ast.Name.t] [@@deriving yojson] + end + + module Info = struct + type t = + [%import: + (Lang.Ast.Info.t + [@with + Lang.Range.t := Range.t; + Lang.With_range.t := With_range.t])] + [@@deriving yojson] + end +end diff --git a/lsp/jLang.mli b/lsp/jLang.mli index 3aba7f17..2b59f7b8 100644 --- a/lsp/jLang.mli +++ b/lsp/jLang.mli @@ -38,3 +38,9 @@ module Diagnostic : sig [@@deriving yojson] end end + +module Ast : sig + module Info : sig + type t = Lang.Ast.Info.t [@@deriving yojson] + end +end diff --git a/lsp/jStdlib.ml b/lsp/jStdlib.ml new file mode 100644 index 00000000..5995cbaf --- /dev/null +++ b/lsp/jStdlib.ml @@ -0,0 +1,5 @@ +module Result = struct + include Stdlib.Result + + type ('a, 'e) t = [%import: ('a, 'e) Stdlib.Result.t] [@@deriving yojson] +end diff --git a/petanque/json/jAgent.ml b/petanque/json/jAgent.ml index dac37aa8..58c39789 100644 --- a/petanque/json/jAgent.ml +++ b/petanque/json/jAgent.ml @@ -8,22 +8,6 @@ module Inspect = struct end (* The typical protocol dance *) - -(* What a mess result stuff is, we need this in case result is installed, as - then the types below will be referenced as plain result ... *) -module Stdlib = struct - module Result = struct - include Stdlib.Result - - type ('a, 'e) t = [%import: ('a, 'e) Stdlib.Result.t] [@@deriving yojson] - end -end - -module Result = Stdlib.Result - -(* ppx_import < 1.10 hack, for some reason it gets confused with the aliases. *) -module Result_ = Stdlib.Result - module Error = struct type t = [%import: Petanque.Agent.Error.t] [@@deriving yojson] end @@ -36,57 +20,24 @@ module Run_result = struct type 'a t = [%import: 'a Petanque.Agent.Run_result.t] [@@deriving yojson] end +(* Both are needed as of today *) +module Stdlib = Lsp.JStdlib +module Result = Stdlib.Result + module R = struct - type 'a t = - [%import: - ('a Petanque.Agent.R.t - [@with - Stdlib.Result.t := Result_.t; - Result.t := Result_.t])] - [@@deriving yojson] + type 'a t = [%import: 'a Petanque.Agent.R.t] [@@deriving yojson] end module Goals = struct type t = string Lsp.JCoq.Goals.reified_pp option [@@deriving yojson] end -module Lang = struct - module Range = struct - type t = Lsp.JLang.Range.t [@@deriving yojson] - end - - module With_range = struct - type 'a t = [%import: ('a Lang.With_range.t[@with Lang.Range.t := Range.t])] - [@@deriving yojson] - end - - module Ast = struct - module Name = struct - type t = [%import: Lang.Ast.Name.t] [@@deriving yojson] - end - - module Info = struct - type t = - [%import: - (Lang.Ast.Info.t - [@with - Lang.Range.t := Range.t; - Lang.With_range.t := With_range.t])] - [@@deriving yojson] - end - end -end +module Lang = Lsp.JLang module Premise = struct module Info = struct type t = [%import: Petanque.Agent.Premise.Info.t] [@@deriving yojson] end - type t = - [%import: - (Petanque.Agent.Premise.t - [@with - Stdlib.Result.t := Result_.t; - Result.t := Result_.t])] - [@@deriving yojson] + type t = [%import: Petanque.Agent.Premise.t] [@@deriving yojson] end diff --git a/petanque/json_shell/protocol_shell.ml b/petanque/json_shell/protocol_shell.ml index 4f4bb4d7..12acda71 100644 --- a/petanque/json_shell/protocol_shell.ml +++ b/petanque/json_shell/protocol_shell.ml @@ -6,7 +6,6 @@ (************************************************************************) open Petanque_json -open JAgent (** [set_workspace { debug; root }] sets the current workspace to the directory specified in [root] *) @@ -47,7 +46,8 @@ module TableOfContents = struct end module Response = struct - type t = (string * Lang.Ast.Info.t list option) list [@@deriving yojson] + type t = (string * Lsp.JLang.Ast.Info.t list option) list + [@@deriving yojson] end module Handler = struct