diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-30 23:48:30 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-13 18:11:22 +0100 |
commit | 6bd240fce21c172680a0cec5346b66e08c76418a (patch) | |
tree | 640407a38cc96645a66ccb7754ace80092fdfe22 | |
parent | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (diff) |
[ci] [coq] Complete 4.06.0 support.
Due to an API change in laglgtk, we need to update CoqIDE. We use a
makefile hack so it can compile with lablgtk < 2.8.16, another option
would be to require 2.8.16 as a minimal dependency.
We also refactor travis to test more lablgtk versions.
We also need to account for improved attribute handling in 4.06.0, in
particular module aliases will propagate the deprecation status.
Fixes #6140.
-rw-r--r-- | .gitlab-ci.yml | 4 | ||||
-rw-r--r-- | .travis.yml | 38 | ||||
-rw-r--r-- | API/API.ml | 4 | ||||
-rw-r--r-- | API/API.mli | 92 | ||||
-rw-r--r-- | Makefile.ide | 9 | ||||
-rw-r--r-- | ide/ideutils.ml | 3 | ||||
-rw-r--r-- | kernel/term.mli | 6 |
7 files changed, 131 insertions, 25 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1742660c8..3117b2b9a 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,8 +18,8 @@ variables: # some useful values COMPILER_32BIT: "4.02.3+32bit" - COMPILER_BLEEDING_EDGE: "4.05.0" - CAMLP5_VER_BLEEDING_EDGE: "7.01" + COMPILER_BLEEDING_EDGE: "4.06.0" + CAMLP5_VER_BLEEDING_EDGE: "7.03" TIMING_PACKAGES: "time python" diff --git a/.travis.yml b/.travis.yml index 7d7a08161..3ebfbefd2 100644 --- a/.travis.yml +++ b/.travis.yml @@ -30,17 +30,21 @@ env: - NJOBS=2 # system is == 4.02.3 - COMPILER="system" + - COMPILER_BE="4.06.0" - CAMLP5_VER="6.14" + - CAMLP5_VER_BE="7.03" - FINDLIB_VER="1.4.1" + - FINDLIB_VER_BE="1.7.3" + - LABLGTK="lablgtk.2.16.0 lablgtk-extras.1.5" + - LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6" - NATIVE_COMP="yes" - COQ_DEST="-local" # Main test suites matrix: - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" - - TEST_TARGET="test-suite" COMPILER="4.06.0+trunk" CAMLP5_VER="7.03" EXTRA_OPAM="num" FINDLIB_VER="1.7.3" - TEST_TARGET="validate" TW="travis_wait" - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait" - - TEST_TARGET="validate" COMPILER="4.06.0+trunk+flambda" CAMLP5_VER="7.03" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" EXTRA_OPAM="num" FINDLIB_VER="1.7.3" + - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" EXTRA_OPAM="num" FINDLIB_VER="${FINDLIB_VER_BE}" - TEST_TARGET="ci-bignums TIMED=1" - TEST_TARGET="ci-color TIMED=1" - TEST_TARGET="ci-compcert TIMED=1" @@ -82,7 +86,7 @@ matrix: - env: - TEST_TARGET="test-suite" - EXTRA_CONF="-coqide opt -with-doc yes" - - EXTRA_OPAM="lablgtk-extras hevea" + - EXTRA_OPAM="hevea ${LABLGTK}" addons: apt: sources: @@ -106,11 +110,11 @@ matrix: - env: - TEST_TARGET="test-suite" - - COMPILER="4.05.0" - - FINDLIB_VER="1.7.3" - - CAMLP5_VER="7.03" + - COMPILER="${COMPILER_BE}" + - FINDLIB_VER="${FINDLIB_VER_BE}" + - CAMLP5_VER="${CAMLP5_VER_BE}" - EXTRA_CONF="-coqide opt -with-doc yes" - - EXTRA_OPAM="lablgtk-extras hevea" + - EXTRA_OPAM="num hevea ${LABLGTK_BE}" addons: apt: sources: @@ -120,12 +124,12 @@ matrix: # Full test-suite with flambda - env: - TEST_TARGET="test-suite" - - COMPILER="4.05.0+flambda" - - FINDLIB_VER="1.7.3" - - CAMLP5_VER="7.03" + - COMPILER="${COMPILER_BE}+flambda" + - FINDLIB_VER="${FINDLIB_VER_BE}" + - CAMLP5_VER="${CAMLP5_VER_BE}" - NATIVE_COMP="no" - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3" - - EXTRA_OPAM="lablgtk-extras hevea" + - EXTRA_OPAM="num hevea ${LABLGTK_BE}" addons: apt: sources: @@ -136,7 +140,7 @@ matrix: - env: - TEST_TARGET="coqocaml" - EXTRA_CONF="-coqide opt -warn-error" - - EXTRA_OPAM="lablgtk-extras hevea" + - EXTRA_OPAM="hevea ${LABLGTK}" # dummy target - BUILD_TARGET="clean" addons: @@ -151,11 +155,11 @@ matrix: - env: - TEST_TARGET="coqocaml" - - COMPILER="4.05.0" - - CAMLP5_VER="7.03" - - FINDLIB_VER="1.7.3" + - COMPILER="${COMPILER_BE}" + - FINDLIB_VER="${FINDLIB_VER_BE}" + - CAMLP5_VER="${CAMLP5_VER_BE}" - EXTRA_CONF="-coqide opt -warn-error" - - EXTRA_OPAM="lablgtk-extras hevea" + - EXTRA_OPAM="num hevea ${LABLGTK_BE}" # dummy target - BUILD_TARGET="clean" addons: @@ -184,7 +188,7 @@ matrix: - NATIVE_COMP="no" - COQ_DEST="-prefix ${PWD}/_install" - EXTRA_CONF="-coqide opt -warn-error" - - EXTRA_OPAM="lablgtk-extras" + - EXTRA_OPAM="${LABLGTK}" before_install: - brew update - brew install opam gnu-time gtk+ expat gtksourceview libxml2 gdk-pixbuf python3 diff --git a/API/API.ml b/API/API.ml index 9a67e3111..f588fe193 100644 --- a/API/API.ml +++ b/API/API.ml @@ -20,6 +20,10 @@ (******************************************************************************) module Coq_config = Coq_config +(* Reexporting deprecated symbols throu module aliases triggers a + warning in 4.06.0 *) +[@@@ocaml.warning "-3"] + (******************************************************************************) (* Kernel *) (******************************************************************************) diff --git a/API/API.mli b/API/API.mli index d0564f9ec..cb945179f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -20,6 +20,10 @@ See below in the file for their concrete position. *) +(* Reexporting deprecated symbols throu module aliases triggers a + warning in 4.06.0 *) +[@@@ocaml.warning "-3"] + (************************************************************************) (* Modules from config/ *) (************************************************************************) @@ -300,21 +304,31 @@ sig [@@ocaml.deprecated "alias of API.Names.Constant.make3"] val debug_pr_con : Constant.t -> Pp.t + [@@ocaml.deprecated "Alias of Names"] val debug_pr_mind : MutInd.t -> Pp.t + [@@ocaml.deprecated "Alias of Names"] val pr_con : Constant.t -> Pp.t + [@@ocaml.deprecated "Alias of Names"] val string_of_con : Constant.t -> string + [@@ocaml.deprecated "Alias of Names"] val string_of_mind : MutInd.t -> string + [@@ocaml.deprecated "Alias of Names"] val debug_string_of_mind : MutInd.t -> string + [@@ocaml.deprecated "Alias of Names"] val debug_string_of_con : Constant.t -> string + [@@ocaml.deprecated "Alias of Names"] type identifier = Id.t + [@@ocaml.deprecated "Alias of Names"] + module Idset : Set.S with type elt = identifier and type t = Id.Set.t + [@@ocaml.deprecated "Alias of Id.Set.t"] end @@ -329,6 +343,7 @@ sig end type universe_level = Level.t + [@@ocaml.deprecated "Deprecated form, see univ.ml"] module LSet : sig @@ -343,6 +358,7 @@ sig end type universe = Universe.t + [@@ocaml.deprecated "Deprecated form, see univ.ml"] module Instance : sig @@ -374,6 +390,7 @@ sig end type universe_context = UContext.t + [@@ocaml.deprecated "Deprecated form, see univ.ml"] module AUContext : sig @@ -382,6 +399,7 @@ sig end type abstract_universe_context = AUContext.t + [@@ocaml.deprecated "Deprecated form, see univ.ml"] module CumulativityInfo : sig @@ -389,12 +407,14 @@ sig end type cumulativity_info = CumulativityInfo.t + [@@ocaml.deprecated "Deprecated form, see univ.ml"] module ACumulativityInfo : sig type t end type abstract_cumulativity_info = ACumulativityInfo.t + [@@ocaml.deprecated "Deprecated form, see univ.ml"] module ContextSet : sig @@ -408,8 +428,10 @@ sig type 'a in_universe_context = 'a * UContext.t type universe_context_set = ContextSet.t + [@@ocaml.deprecated "Deprecated form, see univ.ml"] type universe_set = LSet.t + [@@ocaml.deprecated "Deprecated form, see univ.ml"] type 'a constraint_function = 'a -> 'a -> Constraint.t -> Constraint.t @@ -586,6 +608,10 @@ val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool val mkApp : t * t array -> t val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses + type rec_declaration = Name.t array * types array * constr array + type fixpoint = (int array * int) * rec_declaration + val mkFix : fixpoint -> constr + val mkConst : Constant.t -> t val mkConstU : pconstant -> t @@ -831,8 +857,10 @@ module Term : sig type sorts_family = Sorts.family = InProp | InSet | InType + [@@ocaml.deprecated "Alias of Sorts.family"] type contents = Sorts.contents = Pos | Null + [@@ocaml.deprecated "Alias of Sorts.contents"] type sorts = Sorts.t = | Prop of contents @@ -840,35 +868,48 @@ sig [@@ocaml.deprecated "alias of API.Sorts.t"] type constr = Constr.t + [@@ocaml.deprecated "Alias of Constr.t"] type types = Constr.t + [@@ocaml.deprecated "Alias of Constr.types"] type metavariable = int + [@@ocaml.deprecated "Alias of Constr.metavariable"] type ('constr, 'types) prec_declaration = Names.Name.t array * 'types array * 'constr array + [@@ocaml.deprecated "Alias of Constr.prec_declaration"] type 'constr pexistential = 'constr Constr.pexistential + [@@ocaml.deprecated "Alias of Constr.pexistential"] + type cast_kind = Constr.cast_kind = | VMcast | NATIVEcast | DEFAULTcast | REVERTcast + [@@ocaml.deprecated "Alias of Constr.cast_kind"] type 'a puniverses = 'a Univ.puniverses + [@@ocaml.deprecated "Alias of Constr.puniverses"] type pconstant = Names.Constant.t puniverses + [@@ocaml.deprecated "Alias of Constr.pconstant"] type pinductive = Names.inductive puniverses + [@@ocaml.deprecated "Alias of Constr.pinductive"] type pconstructor = Names.constructor puniverses + [@@ocaml.deprecated "Alias of Constr.pconstructor"] type case_style = Constr.case_style = | LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle + [@@ocaml.deprecated "Alias of Constr.case_style"] type case_printing = Constr.case_printing = { ind_tags : bool list; cstr_tags : bool list array; style : case_style } + [@@ocaml.deprecated "Alias of Constr.case_printing"] type case_info = Constr.case_info = { ci_ind : Names.inductive; @@ -877,12 +918,15 @@ sig ci_cstr_nargs : int array; ci_pp_info : case_printing } + [@@ocaml.deprecated "Alias of Constr.case_info"] type ('constr, 'types) pfixpoint = (int array * int) * ('constr, 'types) prec_declaration + [@@ocaml.deprecated "Alias of Constr.pfixpoint"] type ('constr, 'types) pcofixpoint = int * ('constr, 'types) prec_declaration + [@@ocaml.deprecated "Alias of Constr.pcofixpoint"] type ('constr, 'types, 'sort, 'univs) kind_of_term = ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = | Rel of int @@ -902,11 +946,17 @@ sig | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint | Proj of Names.Projection.t * 'constr + [@@ocaml.deprecated "Alias of Constr.kind_of_term"] type existential = Constr.existential_key * constr array + [@@ocaml.deprecated "Alias of Constr.existential"] type rec_declaration = Names.Name.t array * constr array * constr array + [@@ocaml.deprecated "Alias of Constr.rec_declaration"] type fixpoint = (int array * int) * rec_declaration + [@@ocaml.deprecated "Alias of Constr.fixpoint"] type cofixpoint = int * rec_declaration + [@@ocaml.deprecated "Alias of Constr.cofixpoint"] val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term + [@@ocaml.deprecated "Alias of Constr.kind"] val applistc : constr -> constr list -> constr val applist : constr * constr list -> constr @@ -914,29 +964,52 @@ sig val mkArrow : types -> types -> constr val mkRel : int -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkVar : Names.Id.t -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkMeta : Constr.metavariable -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkEvar : existential -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkSort : Sorts.t -> types + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkProp : types + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkSet : types + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkType : Univ.Universe.t -> types + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkCast : constr * cast_kind * constr -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkProd : Names.Name.t * types * types -> types + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkLambda : Names.Name.t * types * constr -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkLetIn : Names.Name.t * constr * types * constr -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkApp : constr * constr array -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkConst : Names.Constant.t -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkProj : Names.Projection.t * constr -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkInd : Names.inductive -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkConstruct : Names.constructor -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkConstructU : Names.constructor puniverses -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkConstructUi : (pinductive * int) -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkCase : case_info * constr * constr * constr array -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkFix : fixpoint -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkCoFix : cofixpoint -> constr + [@@ocaml.deprecated "Alias of similarly named Constr function"] + val mkNamedLambda : Names.Id.t -> types -> constr -> constr val mkNamedLetIn : Names.Id.t -> constr -> types -> constr -> constr val mkNamedProd : Names.Id.t -> types -> types -> types @@ -975,26 +1048,37 @@ sig val isApp : constr -> bool val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a + [@@ocaml.deprecated "Alias of Constr.fold"] val eq_constr : constr -> constr -> bool + [@@ocaml.deprecated "Alias of Constr.equal"] val hash_constr : constr -> int + [@@ocaml.deprecated "Alias of Constr.hash"] + val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr val it_mkProd_or_LetIn : types -> Context.Rel.t -> types val prod_applist : constr -> constr list -> constr exception DestKO val map_constr : (constr -> constr) -> constr -> constr + [@@ocaml.deprecated "Alias of Constr.map"] val mkIndU : pinductive -> constr + [@@ocaml.deprecated "Alias of Constr.mkIndU"] val mkConstU : pconstant -> constr + [@@ocaml.deprecated "Alias of Constr.mkConstU"] val map_constr_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr + [@@ocaml.deprecated "Alias of Constr.map_with_binders"] + val iter_constr : (constr -> unit) -> constr -> unit + [@@ocaml.deprecated "Alias of Constr.iter."] (* Quotients away universes: really needed? * Can't we just call eq_c_univs_infer and discard the inferred csts? *) val eq_constr_nounivs : constr -> constr -> bool + [@@ocaml.deprecated "Alias of Constr.qe_constr_nounivs."] type ('constr, 'types) kind_of_type = | SortType of Sorts.t @@ -1009,13 +1093,16 @@ sig [@@ocaml.deprecated "alias of API.Sorts.is_prop"] type existential_key = Constr.existential_key + [@@ocaml.deprecated "Alias of Constr.existential_key"] val family_of_sort : Sorts.t -> Sorts.family + [@@ocaml.deprecated "Alias of Sorts.family"] val compare : constr -> constr -> int + [@@ocaml.deprecated "Alias of Constr.compare."] val constr_ord : constr -> constr -> int - [@@ocaml.deprecated "alias of API.Term.compare"] + [@@ocaml.deprecated "alias of Term.compare"] val destInd : constr -> Names.inductive puniverses val univ_of_sort : Sorts.t -> Univ.Universe.t @@ -1027,6 +1114,8 @@ sig val destFix : constr -> fixpoint val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool + [@@ocaml.deprecated "Alias of Constr.compare_head."] + end module Mod_subst : @@ -1673,6 +1762,7 @@ sig | LetPatternStyle | MatchStyle | RegularStyle (** infer printing form from number of constructor *) + [@@ocaml.deprecated "Alias for Constr.case_style."] type 'a cast_type = | CastConv of 'a diff --git a/Makefile.ide b/Makefile.ide index 7593a9f2e..7d809f67a 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -123,6 +123,15 @@ ide/%.cmx: ide/%.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $< +# We need to compile this file without -safe-string due mess with +# lablgtk API. Other option is to require lablgtk >= 2.8.16 +ide/ideutils.cmo: ide/ideutils.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(filter-out -safe-string,$(OCAMLC)) $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + +ide/ideutils.cmx: ide/ideutils.ml + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(filter-out -safe-string,$(OCAMLOPT)) $(COQIDEFLAGS) $(filter-out -safe-string,$(OPTFLAGS)) -c $< #################### ## Install targets diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 83e5da950..0977a1890 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -372,8 +372,7 @@ let read_file name buf = let io_read_all chan = Buffer.clear read_buffer; let read_once () = - (* XXX: Glib.Io must be converted to bytes / -safe-string upstream *) - let len = Glib.Io.read_chars ~buf:(Bytes.unsafe_to_string read_string) ~pos:0 ~len:maxread chan in + let len = Glib.Io.read_chars ~buf:read_string ~pos:0 ~len:maxread chan in Buffer.add_subbytes read_buffer read_string 0 len in begin diff --git a/kernel/term.mli b/kernel/term.mli index cb782afac..33c6b0b08 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -369,11 +369,11 @@ val mkConstructU : constructor puniverses -> constr val mkConstructUi : (pinductive * int) -> constr [@@ocaml.deprecated "Alias for Constr"] val mkCase : case_info * constr * constr * constr array -> constr -[@@ocaml.deprecated "Alias for Constr"] +[@@ocaml.deprecated "Alias for Constr.mkCase"] val mkFix : fixpoint -> constr -[@@ocaml.deprecated "Alias for Constr"] +[@@ocaml.deprecated "Alias for Constr.mkFix"] val mkCoFix : cofixpoint -> constr -[@@ocaml.deprecated "Alias for Constr"] +[@@ocaml.deprecated "Alias for Constr.mkCoFix"] (** {6 Aliases} *) |