diff options
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | .travis.yml | 14 | ||||
| -rw-r--r-- | CHANGES | 9 | ||||
| -rw-r--r-- | INSTALL | 6 | ||||
| -rw-r--r-- | configure.ml | 8 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 14 | ||||
| -rw-r--r-- | dev/doc/profiling.txt | 2 | ||||
| -rw-r--r-- | kernel/nativelib.ml | 11 | ||||
| -rw-r--r-- | test-suite/coqchk/cumulativity.v | 42 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 43 | ||||
| -rw-r--r-- | vernac/mltop.ml | 10 | ||||
| -rw-r--r-- | vernac/mltop.mli | 3 |
12 files changed, 54 insertions, 110 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index a6b17fd148..6a3f27f293 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-09-24-V01" + CACHEKEY: "bionic_coq-V2018-09-25-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/.travis.yml b/.travis.yml index 1a2c909c7d..52e5e051d2 100644 --- a/.travis.yml +++ b/.travis.yml @@ -37,15 +37,15 @@ addons: env: global: - NJOBS=2 - # system is == 4.02.3 - - COMPILER="system" + - COMPILER="4.05.0" - COMPILER_BE="4.07.0" - DUNE_VER=".1.1.1" - - CAMLP5_VER=".6.14" + - CAMLP5_VER=".7.01" - CAMLP5_VER_BE=".7.06" - - FINDLIB_VER=".1.4.1" + # ounit forces FINDLIB here + - FINDLIB_VER=".1.7.3" - FINDLIB_VER_BE=".1.8.0" - - LABLGTK="lablgtk.2.18.3 conf-gtksourceview.2" + - LABLGTK="lablgtk.2.18.6 conf-gtksourceview.2" - LABLGTK_BE="lablgtk.2.18.6 conf-gtksourceview.2" - NATIVE_COMP="yes" - COQ_DEST="-local" @@ -56,13 +56,13 @@ matrix: include: - if: NOT (type = pull_request) env: - - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" EXTRA_OPAM="ounit" + - TEST_TARGET="test-suite" COMPILER="4.05.0+32bit" EXTRA_OPAM="ounit" - if: NOT (type = pull_request) env: - TEST_TARGET="validate" TW="travis_wait" - if: NOT (type = pull_request) env: - - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait" + - TEST_TARGET="validate" COMPILER="4.05.0+32bit" TW="travis_wait" - if: NOT (type = pull_request) env: - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}" @@ -1,5 +1,10 @@ -Changes beyond 8.9 -================== +Changes from 8.9 to 8.10 +======================== + +OCaml + +- Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the + INSTALL file for more information on dependencies. Plugins @@ -29,7 +29,7 @@ WHAT DO YOU NEED ? To compile Coq yourself, you need: - - OCaml (version >= 4.02.3) + - OCaml (version >= 4.05.0) (available at https://ocaml.org/) (This version of Coq has been tested up to OCaml 4.07.0) @@ -39,7 +39,7 @@ WHAT DO YOU NEED ? - Findlib (version >= 1.4.1) (available at http://projects.camlcity.org/projects/findlib.html) - - Camlp5 (version >= 6.14) + - Camlp5 (version >= 7.01) (available at https://camlp5.github.io/) - GNU Make version 3.81 or later @@ -88,7 +88,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). computer and that "ocamlc" (or, better, its native code version "ocamlc.opt") lies in a directory which is present in your $PATH environment variable. At the time of writing this sentence, all - versions of Objective Caml later or equal to 4.02.3 are + versions of Objective Caml later or equal to 4.05.0 are supported. To get Coq in native-code, (it runs 4 to 10 times faster than diff --git a/configure.ml b/configure.ml index 1c2edefc5c..e5db520de3 100644 --- a/configure.ml +++ b/configure.ml @@ -600,14 +600,14 @@ let caml_version_nums = "Is it installed properly?") let check_caml_version () = - if caml_version_nums >= [4;2;3] then + if caml_version_nums >= [4;5;0] then cprintf "You have OCaml %s. Good!" caml_version else let () = cprintf "Your version of OCaml is %s." caml_version in if !prefs.force_caml_version then warn "Your version of OCaml is outdated." else - die "You need OCaml 4.02.3 or later." + die "You need OCaml 4.05.0 or later." let _ = check_caml_version () @@ -647,7 +647,6 @@ let camltag = match caml_version_list with 45: "open" shadowing a label or constructor: see 44 48: implicit elimination of optional arguments: too common 50: unexpected documentation comment: too common and annoying to avoid - 56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3 58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9 59: "potential assignment to a non-mutable value": See Coq's issue #8043 *) @@ -655,9 +654,6 @@ let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-58-59" let coq_warn_error = if !prefs.warn_error then "-warn-error +a" - ^ (if caml_version_nums > [4;2;3] - then "-56" - else "") else "" (* Flags used to compile Coq and plugins (via coq_makefile) *) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 8d0f69626e..fcfa591ce1 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-09-24-V01" +# CACHEKEY: "bionic_coq-V2018-09-25-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -32,33 +32,31 @@ ENV NJOBS="2" \ OPAMYES="true" # Base opam is the set of base packages required by Coq -ENV COMPILER="4.02.3" +ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8" \ +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8 odoc.1.2.0" \ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. -ENV CAMLP5_VER="6.14" \ +ENV CAMLP5_VER="7.01" \ COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" -# The separate `opam install ocamlfind` workarounds an OPAM repository bug in 4.02.3 +# base switch RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \ - opam install ocamlfind.1.8.0 && \ opam install $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM # base+32bit switch RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ - opam install ocamlfind.1.8.0 && \ opam install $BASE_OPAM camlp5.$CAMLP5_VER # EDGE switch ENV COMPILER_EDGE="4.07.0" \ CAMLP5_VER_EDGE="7.06" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ - BASE_OPAM_EDGE="odoc.1.2.0 dune-release.0.3.0" + BASE_OPAM_EDGE="dune-release.0.3.0" RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt index 45766293c7..29e87df6b8 100644 --- a/dev/doc/profiling.txt +++ b/dev/doc/profiling.txt @@ -7,7 +7,7 @@ want to profile time or memory consumption. AFAIK, this only works for Linux. In Coq source folder: -opam switch 4.02.3+fp +opam switch 4.05.0+trunk+fp ./configure -local -debug make perf record -g bin/coqtop -compile file.v diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index b4126dd68c..6edb387bb1 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -89,16 +89,7 @@ let call_compiler ?profile:(profile=false) ml_filename = else [] in - let flambda_args = - if Coq_config.caml_version_nums >= [4;3;0] && Dynlink.is_native then - (* We play safe for now, and use the native compiler - with -Oclassic, however it is likely that `native_compute` - users can benefit from tweaking here. - *) - ["-Oclassic"] - else - [] - in + let flambda_args = if Sys.(backend_type = Native) then ["-Oclassic"] else [] in let args = initial_args @ profile_args @ diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v index 034684054d..c3f6bebcbe 100644 --- a/test-suite/coqchk/cumulativity.v +++ b/test-suite/coqchk/cumulativity.v @@ -27,41 +27,35 @@ End ListLower. Lemma LowerL_Lem@{i j|j<i+} (A : Type@{j}) (l : List@{i} A) : l = LowerL@{j i} l. Proof. reflexivity. Qed. -(* -I disable these tests because cqochk can't process them when compiled with - ocaml-4.02.3+32bit and camlp5-4.16 which is the case for Travis! - I have added this file (including the commented parts below) in - test-suite/success/cumulativity.v which doesn't run coqchk on them. -*) -(* Inductive Tp := tp : Type -> Tp. *) +Inductive Tp := tp : Type -> Tp. -(* Section TpLift. *) -(* Universe i j. *) +Section TpLift. -(* Constraint i < j. *) + Universe i j. -(* Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. *) + Constraint i < j. -(* End TpLift. *) + Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. -(* Lemma LiftC_Lem (t : Tp) : LiftTp t = t. *) -(* Proof. reflexivity. Qed. *) +End TpLift. -(* Section TpLower. *) -(* Universe i j. *) +Lemma LiftC_Lem (t : Tp) : LiftTp t = t. +Proof. reflexivity. Qed. -(* Constraint i < j. *) +Section TpLower. + Universe i j. -(* Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. *) + Constraint i < j. -(* End TpLower. *) + Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. +End TpLower. -(* Section subtyping_test. *) -(* Universe i j. *) -(* Constraint i < j. *) +Section subtyping_test. + Universe i j. + Constraint i < j. -(* Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. *) + Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. -(* End subtyping_test. *) +End subtyping_test. diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index ab60920fbc..691f37b414 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -92,41 +92,6 @@ module Aux = struct | None -> DirMap.remove key map | Some x -> DirMap.add key x map - (* Available in OCaml >= 4.04 *) - let split_on_char sep s = - let open String in - let r = ref [] in - let j = ref (length s) in - for i = length s - 1 downto 0 do - if unsafe_get s i = sep then begin - r := sub s (i + 1) (!j - i - 1) :: !r; - j := i - end - done; - sub s 0 !j :: !r - - (* Available in OCaml >= 4.04 *) - let is_dir_sep = match Sys.os_type with - | "Win32" -> fun s i -> s.[i] = '\\' - | _ -> fun s i -> s.[i] = '/' - - let extension_len name = - let rec check i0 i = - if i < 0 || is_dir_sep name i then 0 - else if name.[i] = '.' then check i0 (i - 1) - else String.length name - i0 - in - let rec search_dot i = - if i < 0 || is_dir_sep name i then 0 - else if name.[i] = '.' then check i (i - 1) - else search_dot (i - 1) - in - search_dot (String.length name - 1) - - let remove_extension name = - let l = extension_len name in - if l = 0 then name else String.sub name 0 (String.length name - l) - end let add_map_list key elem map = @@ -205,18 +170,18 @@ let pp_vo_dep dir fmt vo = (* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *) let deps = List.map (fun s -> sdir ^ s) (edep @ vo.deps) in (* The source file is also corrected as we will call coqtop from the top dir *) - let source = String.concat "/" dir ^ "/" ^ Legacy.(remove_extension vo.target) ^ ".v" in + let source = String.concat "/" dir ^ "/" ^ Filename.(remove_extension vo.target) ^ ".v" in (* The final build rule *) let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s -compile %s))" eflag cflag source in pp_rule fmt [vo.target] deps action let pp_ml4_dep _dir fmt ml = - let target = Legacy.(remove_extension ml) ^ ".ml" in + let target = Filename.(remove_extension ml) ^ ".ml" in let ml4_rule = "(run coqp5 -loc loc -impl %{pp-file} -o %{targets})" in pp_rule fmt [target] [ml] ml4_rule let pp_mlg_dep _dir fmt ml = - let target = Legacy.(remove_extension ml) ^ ".ml" in + let target = Filename.(remove_extension ml) ^ ".ml" in let ml4_rule = "(run coqpp %{pp-file})" in pp_rule fmt [target] [ml] ml4_rule @@ -274,7 +239,7 @@ let parse_coqdep_line l = begin match targets with | [target] -> let dir, target = Filename.(dirname target, basename target) in - Some (Legacy.split_on_char '/' dir, VO { target; deps; }) + Some (String.split_on_char '/' dir, VO { target; deps; }) (* Otherwise a vio file, we ignore *) | _ -> None end diff --git a/vernac/mltop.ml b/vernac/mltop.ml index d25dea1413..3620e177fe 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -69,9 +69,6 @@ type kind_load = (* Must be always initialized *) let load = ref WithoutTop -(* Are we in a native version of Coq? *) -let is_native = Dynlink.is_native - (* Sets and initializes a toplevel (if any) *) let set_top toplevel = load := WithTop toplevel; @@ -89,7 +86,7 @@ let is_ocaml_top () = |_ -> false (* Tests if we can load ML files *) -let has_dynlink = Coq_config.has_natdynlink || not is_native +let has_dynlink = Coq_config.has_natdynlink || not Sys.(backend_type = Native) (* Runs the toplevel loop of Ocaml *) let ocaml_toploop () = @@ -149,7 +146,7 @@ let dir_ml_use s = | WithTop t -> t.use_file s | _ -> let moreinfo = - if Dynlink.is_native then " Loading ML code works only in bytecode." + if Sys.(backend_type = Native) then " Loading ML code works only in bytecode." else "" in user_err ~hdr:"Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo) @@ -257,7 +254,8 @@ let file_of_name name = str"Loadpath: " ++ str(String.concat ":" !coq_mlpath_copy)) in if not (Filename.is_relative name) then if Sys.file_exists name then name else fail name - else if is_native then + else if Sys.(backend_type = Native) then + (* XXX: Dynlink.adapt_filename does the same? *) let name = match suffix with | Some ((".cmo"|".cma") as suffix) -> (Filename.chop_suffix name suffix) ^ ".cmxs" diff --git a/vernac/mltop.mli b/vernac/mltop.mli index ed1f9a12d8..3d796aa4aa 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -21,9 +21,6 @@ type toplevel = { (** Sets and initializes a toplevel (if any) *) val set_top : toplevel -> unit -(** Are we in a native version of Coq? *) -val is_native : bool - (** Removes the toplevel (if any) *) val remove : unit -> unit |