Skip to content

Commit

Permalink
[travis] [build] Disable warnings for sexplib >= 0.13, fix Coq version
Browse files Browse the repository at this point in the history
This should fix Travis on newer sexplib, and still keep compat with
0.12.

We also fix Coq's Travis install [wrong version picked for this branch]
  • Loading branch information
ejgallego committed May 29, 2020
1 parent 40760cd commit 000dac6
Show file tree
Hide file tree
Showing 4 changed files with 15 additions and 12 deletions.
6 changes: 3 additions & 3 deletions .travis.yml
Original file line number Diff line number Diff line change
Expand Up @@ -31,9 +31,9 @@ env:
- COMPILER="4.07.1"
# Main test suites
matrix:
- TEST_TARGET="build" COMPILER="4.07.1" EXTRA_OPAM="coq"
- TEST_TARGET="test" COMPILER="4.07.1" EXTRA_OPAM="coq coq-mathcomp-ssreflect"
- TEST_TARGET="js-dune" COMPILER="4.07.1+32bit" EXTRA_OPAM="coq js_of_ocaml js_of_ocaml-lwt"
- TEST_TARGET="build" COMPILER="4.07.1" EXTRA_OPAM="coq.8.10.2"
- TEST_TARGET="test" COMPILER="4.07.1" EXTRA_OPAM="coq.8.10.2 coq-mathcomp-ssreflect"
- TEST_TARGET="js-dune" COMPILER="4.07.1+32bit" EXTRA_OPAM="coq.8.10.2 js_of_ocaml js_of_ocaml-lwt"
# Don't test opam in 8.10 [yet]
- TEST_TARGET="test" SERAPI_COQ_HOME="$HOME/coq-$COQ_VERSION/_build/install/default/lib/"

Expand Down
8 changes: 4 additions & 4 deletions serapi/serapi_protocol.ml
Original file line number Diff line number Diff line change
Expand Up @@ -385,7 +385,7 @@ type query_opt =
pp : format_opt [@default { pp_format = PpSer; pp_depth = 0; pp_elide = "..."; pp_margin = 72 } ];
(* Legacy/Deprecated *)
route : Feedback.route_id [@default 0];
}
} [@@ocaml.warning "-3"]

(** XXX: This should be in sync with the object tag! *)
type query_cmd =
Expand Down Expand Up @@ -656,14 +656,14 @@ let coq_protect e =
(* Richpp.richpp_of_pp msg *)

type parse_opt =
{ ontop : Stateid.t sexp_option }
{ ontop : Stateid.t sexp_option } [@@ocaml.warning "-3"]

type add_opts = {
lim : int sexp_option;
ontop : Stateid.t sexp_option;
newtip : Stateid.t sexp_option;
verb : bool [@default false];
}
} [@@ocaml.warning "-3"]

module ControlUtil = struct

Expand Down Expand Up @@ -773,7 +773,7 @@ type newdoc_opts =
; iload_path : Mltop.coq_path list sexp_option
(* Libs to require in STM init *)
; require_libs : (string * string option * bool option) list sexp_option
}
} [@@ocaml.warning "-3"]

(******************************************************************************)
(* Help *)
Expand Down
9 changes: 4 additions & 5 deletions serapi/serapi_protocol.mli
Original file line number Diff line number Diff line change
Expand Up @@ -300,7 +300,7 @@ type query_opt =
(** Printing format of the query, this can be used to select the type of the answer, as for example to show goals in human-form. *)
route : Feedback.route_id [@default 0];
(** Legacy/Deprecated STM query method *)
}
} [@@ocaml.warning "-3"]

(** Query commands are mostly a tag and some arguments determining the result type.
Expand Down Expand Up @@ -365,8 +365,7 @@ end
type parse_opt =
{ ontop : Stateid.t sexp_option
(** parse [ontop] of the given sentence *)
}

} [@@ocaml.warning "-3"]

(** [Add] will take a string and parse all the sentences on it, until an error of the end is found.
Options for [Add] are: *)
Expand All @@ -379,7 +378,7 @@ type add_opts = {
(** Make [newtip] the new sentence id, very useful to avoid synchronous operations *)
verb : bool [@default false];
(** [verb] internal Coq parameter, be verbose on parsing *)
}
} [@@ocaml.warning "-3"]

(******************************************************************************)
(* Init / new document *)
Expand All @@ -395,7 +394,7 @@ type newdoc_opts =
(** Initial LoadPath for the document *) (* [XXX: Use the coq_pkg record?] *)
; require_libs : (string * string option * bool option) list sexp_option
(** Libraries to load in the initial document state *)
}
} [@@ocaml.warning "-3"]

(******************************************************************************)
(* Help *)
Expand Down
4 changes: 4 additions & 0 deletions sertop/sertop_ser.ml
Original file line number Diff line number Diff line change
Expand Up @@ -185,6 +185,7 @@ type query_opt =
Sexplib.Conv.sexp_option := sexp_option;
]]
[@@deriving sexp]
[@@ocaml.warning "-3"]

type query_cmd =
[%import: Serapi_protocol.query_cmd]
Expand Down Expand Up @@ -257,6 +258,7 @@ type add_opts =
Sexplib.Conv.sexp_option := sexp_option;
]]
[@@deriving sexp]
[@@ocaml.warning "-3"]

type newdoc_opts =
[%import: Serapi_protocol.newdoc_opts
Expand All @@ -266,13 +268,15 @@ type newdoc_opts =
Sexplib.Conv.sexp_option := sexp_option;
]]
[@@deriving sexp]
[@@ocaml.warning "-3"]

type parse_opt =
[%import: Serapi_protocol.parse_opt
[@with
Sexplib.Conv.sexp_option := sexp_option;
]]
[@@deriving sexp]
[@@ocaml.warning "-3"]

type cmd =
[%import: Serapi_protocol.cmd]
Expand Down

0 comments on commit 000dac6

Please sign in to comment.