Skip to content

Commit

Permalink
Merge pull request #813 from ejgallego/ppxlib_toolchain
Browse files Browse the repository at this point in the history
[build] [deps] Bump ppxlib toolchain to 0.26.0.
  • Loading branch information
ejgallego authored Aug 30, 2024
2 parents f4564b4 + 6219d34 commit 94d647e
Show file tree
Hide file tree
Showing 7 changed files with 61 additions and 68 deletions.
8 changes: 8 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
@@ -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
-----------------------------------

Expand Down
20 changes: 10 additions & 10 deletions coq-lsp.opam
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
Expand Down
23 changes: 23 additions & 0 deletions lsp/jLang.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
6 changes: 6 additions & 0 deletions lsp/jLang.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
5 changes: 5 additions & 0 deletions lsp/jStdlib.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module Result = struct
include Stdlib.Result

type ('a, 'e) t = [%import: ('a, 'e) Stdlib.Result.t] [@@deriving yojson]
end
63 changes: 7 additions & 56 deletions petanque/json/jAgent.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
4 changes: 2 additions & 2 deletions petanque/json_shell/protocol_shell.ml
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@
(************************************************************************)

open Petanque_json
open JAgent

(** [set_workspace { debug; root }] sets the current workspace to the directory
specified in [root] *)
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit 94d647e

Please sign in to comment.