diff options
29 files changed, 173 insertions, 154 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 2b430c156e..4a57c6bc68 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -19,7 +19,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2020-08-28-V92" + CACHEKEY: "bionic_coq-V2020-09-16-V38" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/.merlin.in b/.merlin.in index fa3473765d..80b0b600eb 100644 --- a/.merlin.in +++ b/.merlin.in @@ -54,3 +54,4 @@ S plugins/** B plugins/** PKG threads.posix +PKG zarith
\ No newline at end of file diff --git a/.ocamlformat b/.ocamlformat index a0d4ef6bbb..93f5ab4007 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,4 +1,4 @@ -version=0.14.2 +version=0.15.0 profile=ocamlformat # to enable a whole directory, put "disable=false" in dir/.ocamlformat diff --git a/INSTALL.md b/INSTALL.md index abc38390e0..adc0f557ac 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -13,12 +13,12 @@ Build Requirements To compile Coq yourself, you need: - [OCaml](https://ocaml.org/) (version >= 4.05.0) - (This version of Coq has been tested up to OCaml 4.10.0) + (This version of Coq has been tested up to OCaml 4.11.1) - The [num](https://github.com/ocaml/num) library; note that it is included in the OCaml distribution for OCaml versions < 4.06.0 -- The [ZArith library](https://github.com/ocaml/Zarith) >= 1.8 +- The [ZArith library](https://github.com/ocaml/Zarith) >= 1.10 - The [findlib](http://projects.camlcity.org/projects/findlib.html) library (version >= 1.8.0) @@ -53,7 +53,7 @@ CoqIDE with: Opam (https://opam.ocaml.org/) is recommended to install OCaml and the corresponding packages. - $ opam switch create coq 4.10.0+flambda + $ opam switch create coq 4.11.1+flambda $ eval $(opam env) $ opam install num ocamlfind lablgtk3-sourceview3 diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 5830095861..be9e774381 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -80,11 +80,11 @@ jobs: opam switch set ocaml-base-compiler.$COMPILER eval $(opam env) opam update - opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 zarith.1.9.1 + opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 zarith.1.10 opam list displayName: 'Install OCaml dependencies' env: - COMPILER: "4.10.0" + COMPILER: "4.11.1" FINDLIB_VER: ".1.8.1" OPAMYES: "true" @@ -25,7 +25,7 @@ depends: [ "dune" { >= "2.5.0" } "ocamlfind" { build } "num" - "zarith" { >= "1.9.1" } + "zarith" { >= "1.10" } ] build: [ diff --git a/coq.opam.docker b/coq.opam.docker index ac1869f344..09065fdffd 100644 --- a/coq.opam.docker +++ b/coq.opam.docker @@ -24,7 +24,7 @@ depends: [ "ocaml" { >= "4.05.0" } "ocamlfind" { build } "num" - "zarith" { >= "1.9.1" } + "zarith" { >= "1.10" } "conf-findutils" {build} ] diff --git a/default.nix b/default.nix index ef969acd31..e383d214e0 100644 --- a/default.nix +++ b/default.nix @@ -43,7 +43,7 @@ stdenv.mkDerivation rec { hostname python3 time # coq-makefile timing tools ] - ++ (with ocamlPackages; [ ocaml findlib num zarith ]) + ++ (with ocamlPackages; [ ocaml findlib ]) ++ optionals buildIde [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook @@ -71,9 +71,8 @@ stdenv.mkDerivation rec { # Since #12604, ocamlfind looks for num when building plugins # This follows a similar change in the nixpkgs repo (cf. NixOS/nixpkgs#94230) - propagatedBuildInputs = [ - ocamlPackages.num - ]; + # Same for zarith which is needed since its introduction as a dependency of Coq + propagatedBuildInputs = with ocamlPackages; [ num zarith ]; src = if shell then null diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index cde1d798a0..fcc585117b 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1026,7 +1026,7 @@ function make_num { function make_zarith { make_ocaml - if build_prep https://github.com/ocaml/Zarith/archive release-1.9.1 tar.gz 1 zarith-1.9.1; then + if build_prep https://github.com/ocaml/Zarith/archive release-1.10 tar.gz 1 zarith-1.10; then logn configure ./configure log1 make log2 make install diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh index 17d71ac52a..f2397cdcee 100755 --- a/dev/ci/azure-opam.sh +++ b/dev/ci/azure-opam.sh @@ -2,7 +2,7 @@ set -e -x -OPAM_VARIANT=ocaml-variants.4.10.0+mingw64c +OPAM_VARIANT=ocaml-variants.4.11.1+mingw64c wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz tar -xf opam64.tar.xz diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 78c8673299..2fcd69e130 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-08-28-V92" +# CACHEKEY: "bionic_coq-V2020-09-16-V38" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -43,7 +43,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages, num to be removed once the migration to # micromega is complete, `num` also does not have a version number as # the right version to install varies with the compiler version. -ENV BASE_OPAM="num zarith.1.9.1 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.0" \ +ENV BASE_OPAM="num zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ BASE_ONLY_OPAM="elpi.1.11.0" @@ -59,12 +59,12 @@ RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opa # base+32bit switch, note the zarith hack RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ - i386 env CC='gcc -m32' opam install zarith.1.9.1 && \ + i386 env CC='gcc -m32' opam install zarith.1.10 && \ opam install $BASE_OPAM # EDGE switch -ENV COMPILER_EDGE="4.10.0" \ - BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3 ocamlformat.0.14.2" +ENV COMPILER_EDGE="4.11.1" \ + BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3 ocamlformat.0.15.0" # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all index d6348a3624..679b3d1f79 100644 --- a/dev/dune-workspace.all +++ b/dev/dune-workspace.all @@ -3,5 +3,5 @@ ; Add custom flags here. Default developer profile is `dev` (context (opam (switch 4.05.0))) (context (opam (switch 4.05.0+32bit))) -(context (opam (switch 4.10.0))) -(context (opam (switch 4.10.0+flambda))) +(context (opam (switch 4.11.1))) +(context (opam (switch 4.11.1+flambda))) diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index bfb25e72dd..e798645ed0 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/17812e653d89c46d68b7b10e290b1c16758f4e47.tar.gz"; - sha256 = "1zcb70dyfqc8l2ywpbvxmpfshapdi0g365m3rhmwpagqg47pnyxs"; + url = "https://github.com/NixOS/nixpkgs/archive/3c0e3697520cbe7d9eb3a64bfd87de840bf4aa77.tar.gz"; + sha256 = "1vx7kyaq0i287dragjgfdj94ggwr3ky2b7bq32l8rkd2k3vc3gl5"; }) diff --git a/doc/changelog/07-commands-and-options/13016-remove-Ocaml-value.rst b/doc/changelog/07-commands-and-options/13016-remove-Ocaml-value.rst new file mode 100644 index 0000000000..c67b0f6e80 --- /dev/null +++ b/doc/changelog/07-commands-and-options/13016-remove-Ocaml-value.rst @@ -0,0 +1,4 @@ +- **Removed:** + In the :cmd:`Extraction Language` command, remove `Ocaml` as a valid value. + Use `OCaml` instead. This was deprecated in Coq 8.8, `#6261 <https://github.com/coq/coq/pull/6261>`_ + (`#13016 <https://github.com/coq/coq/pull/13016>`_, by Jim Fehrle). diff --git a/doc/changelog/11-infrastructure-and-dependencies/12972-ocaml+4_11.rst b/doc/changelog/11-infrastructure-and-dependencies/12972-ocaml+4_11.rst new file mode 100644 index 0000000000..855aa360f1 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/12972-ocaml+4_11.rst @@ -0,0 +1,4 @@ +- **Added:** + Coq is now tested against OCaml 4.11.1 + (`#12972 <https://github.com/coq/coq/pull/12972>`_, + by Emilio Jesus Gallego Arias). diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index 094f87f154..da7ed7be64 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -60,16 +60,10 @@ let pr_language = function | Scheme -> str "Scheme" | JSON -> str "JSON" -let warn_deprecated_ocaml_spelling = - CWarnings.create ~name:"deprecated-ocaml-spelling" ~category:"deprecated" - (fun () -> - strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\".")) - } VERNAC ARGUMENT EXTEND language PRINTED BY { pr_language } -| [ "Ocaml" ] -> { let _ = warn_deprecated_ocaml_spelling () in Ocaml } | [ "OCaml" ] -> { Ocaml } | [ "Haskell" ] -> { Haskell } | [ "Scheme" ] -> { Scheme } diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 148c1772bf..9008691bca 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -354,7 +354,7 @@ let is_linear_for v pc = *) let is_linear_substitution sys ((p, o), prf) = - let pred v = v =/ Q.one || v =/ Q.neg_one in + let pred v = v =/ Q.one || v =/ Q.minus_one in match o with | Eq -> ( match @@ -761,7 +761,7 @@ let reduce_unary psys = let is_unary_equation (cstr, prf) = if cstr.op == Eq then Vect.find - (fun v n -> if n =/ Q.one || n =/ Q.neg_one then Some v else None) + (fun v n -> if n =/ Q.one || n =/ Q.minus_one then Some v else None) cstr.coeffs else None in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 44bc20e55f..d2c49c4432 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -2141,6 +2141,7 @@ let really_call_csdpcert : List.fold_left Filename.concat (Envars.coqlib ()) ["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in + let cmdname = if Sys.file_exists cmdname then cmdname else "csdpcert" in match (command cmdname [|cmdname|] (provername, poly) : csdp_certificate) with | F str -> if debug then Printf.fprintf stdout "really_call_csdpcert : %s\n" str; diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 3d1770a541..f4d17b8940 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -190,6 +190,7 @@ let system_list sys = let add (v1, c1) (v2, c2) = assert (c1 <>/ Q.zero && c2 <>/ Q.zero); + (* XXX Can use Q.inv now *) let res = mul_add (Q.one // c1) v1 (Q.one // c2) v2 in (res, count res) @@ -569,7 +570,7 @@ module Fourier = struct (* We add a dummy (fresh) variable for vector *) let fresh = List.fold_left (fun fr c -> max fr (Vect.fresh c.coeffs)) 0 l in let cstr = - {coeffs = Vect.set fresh Q.neg_one vect; op = Eq; cst = Q.zero} + {coeffs = Vect.set fresh Q.minus_one vect; op = Eq; cst = Q.zero} in match solve fresh choose_equality_var choose_variable (cstr :: l) with | Inr prf -> None (* This is an unsatisfiability proof *) diff --git a/plugins/micromega/numCompat.ml b/plugins/micromega/numCompat.ml index 4cb91ea520..02c4bab497 100644 --- a/plugins/micromega/numCompat.ml +++ b/plugins/micromega/numCompat.ml @@ -31,37 +31,24 @@ module type ZArith = sig end module Z = struct - type t = Big_int.big_int - - open Big_int - - let zero = zero_big_int - let one = unit_big_int - let two = big_int_of_int 2 - let add = Big_int.add_big_int - let sub = Big_int.sub_big_int - let mul = Big_int.mult_big_int - let div = Big_int.div_big_int - let neg = Big_int.minus_big_int - let sign = Big_int.sign_big_int - let equal = eq_big_int - let compare = compare_big_int - let power_int = power_big_int_positive_int - let quomod = quomod_big_int + (* Beware this only works fine in ZArith >= 1.10 due to + https://github.com/ocaml/Zarith/issues/58 *) + include Z - let ppcm x y = - let g = gcd_big_int x y in - let x' = div_big_int x g in - let y' = div_big_int y g in - mult_big_int g (mult_big_int x' y') - - let gcd = gcd_big_int + (* Constants *) + let two = Z.of_int 2 + let ten = Z.of_int 10 + let power_int = Big_int_Z.power_big_int_positive_int + let quomod = Big_int_Z.quomod_big_int - let lcm x y = - if eq_big_int x zero && eq_big_int y zero then zero - else abs_big_int (div_big_int (mult_big_int x y) (gcd x y)) + (* zarith fails with division by zero if x == 0 && y == 0 *) + let lcm x y = if Z.equal x zero && Z.equal y zero then zero else Z.lcm x y - let to_string = string_of_big_int + let ppcm x y = + let g = gcd x y in + let x' = Z.div x g in + let y' = Z.div y g in + Z.mul g (Z.mul x' y') end module type QArith = sig @@ -74,7 +61,7 @@ module type QArith = sig val one : t val two : t val ten : t - val neg_one : t + val minus_one : t module Notations : sig val ( // ) : t -> t -> t @@ -119,56 +106,64 @@ end module Q : QArith with module Z = Z = struct module Z = Z - type t = Num.num + let pow_check_exp x y = + let z_res = + if y = 0 then Z.one + else if y > 0 then Z.pow x y + else (* s < 0 *) + Z.pow x (abs y) + in + let z_res = Q.of_bigint z_res in + if 0 <= y then z_res else Q.inv z_res - open Num + include Q - let of_int x = Int x - let zero = Int 0 - let one = Int 1 - let two = Int 2 - let ten = Int 10 - let neg_one = Int (-1) + let two = Q.(of_int 2) + let ten = Q.(of_int 10) module Notations = struct - let ( // ) = div_num - let ( +/ ) = add_num - let ( -/ ) = sub_num - let ( */ ) = mult_num - let ( =/ ) = eq_num - let ( <>/ ) = ( <>/ ) - let ( >/ ) = ( >/ ) - let ( >=/ ) = ( >=/ ) - let ( </ ) = ( </ ) - let ( <=/ ) = ( <=/ ) + let ( // ) = Q.div + let ( +/ ) = Q.add + let ( -/ ) = Q.sub + let ( */ ) = Q.mul + let ( =/ ) = Q.equal + let ( <>/ ) x y = not (Q.equal x y) + let ( >/ ) = Q.gt + let ( >=/ ) = Q.geq + let ( </ ) = Q.lt + let ( <=/ ) = Q.leq end - let compare = compare_num - let make x y = Big_int x // Big_int y - - let numdom r = - let r' = Ratio.normalize_ratio (ratio_of_num r) in - (Ratio.numerator_ratio r', Ratio.denominator_ratio r') - - let num x = numdom x |> fst - let den x = numdom x |> snd - let of_bigint x = Big_int x - let to_bigint = big_int_of_num - let neg = minus_num - - (* let inv = *) - let max = max_num - let min = min_num - let sign = sign_num - let abs = abs_num - let mod_ = mod_num - let floor = floor_num - let ceiling = ceiling_num - let round = round_num - let pow2 n = power_num two (Int n) - let pow10 n = power_num ten (Int n) - let power x = power_num (Int x) - let to_string = string_of_num - let of_string = num_of_string - let to_float = float_of_num + (* XXX: review / improve *) + let floorZ q : Z.t = Z.fdiv (num q) (den q) + let floor q : t = floorZ q |> Q.of_bigint + let ceiling q : t = Z.cdiv (Q.num q) (Q.den q) |> Q.of_bigint + let half = Q.make Z.one Z.two + + (* We imitate Num's round which is to the nearest *) + let round q = floor (Q.add half q) + + (* XXX: review / improve *) + let quo x y = + let s = sign y in + let res = floor (x / abs y) in + if Int.equal s (-1) then neg res else res + + let mod_ x y = x - (y * quo x y) + + (* XXX: review / improve *) + (* Note that Z.pow doesn't support negative exponents *) + + let pow2 y = pow_check_exp Z.two y + let pow10 y = pow_check_exp Z.ten y + + let power (x : int) (y : t) : t = + let y = + try Q.to_int y + with Z.Overflow -> + (* XXX: make doesn't link Pp / CErrors for csdpcert, that could be fixed *) + raise (Invalid_argument "[micromega] overflow in exponentiation") + (* CErrors.user_err (Pp.str "[micromega] overflow in exponentiation") *) + in + pow_check_exp (Z.of_int x) y end diff --git a/plugins/micromega/numCompat.mli b/plugins/micromega/numCompat.mli index acc6be6ce0..0b4d52708f 100644 --- a/plugins/micromega/numCompat.mli +++ b/plugins/micromega/numCompat.mli @@ -25,8 +25,15 @@ module type ZArith = sig val power_int : t -> int -> t val quomod : t -> t -> t * t val ppcm : t -> t -> t + + (** [gcd x y] Greatest Common Divisor. Must always return a + positive number *) val gcd : t -> t -> t + + (** [lcm x y] Least Common Multiplier. Must always return a + positive number *) val lcm : t -> t -> t + val to_string : t -> string end @@ -40,7 +47,9 @@ module type QArith = sig val one : t val two : t val ten : t - val neg_one : t + + (** -1 constant *) + val minus_one : t module Notations : sig val ( // ) : t -> t -> t diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index afef41d67e..5c0aa9ef0d 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -156,7 +156,7 @@ let pp_mon o (m, i) = if Monomial.is_const m then if Q.zero =/ i then () else Printf.fprintf o "%s" (Q.to_string i) else if Q.one =/ i then Monomial.pp o m - else if Q.neg_one =/ i then Printf.fprintf o "-%a" Monomial.pp m + else if Q.minus_one =/ i then Printf.fprintf o "-%a" Monomial.pp m else if Q.zero =/ i then () else Printf.fprintf o "%s*%a" (Q.to_string i) Monomial.pp m @@ -912,7 +912,7 @@ module WithProof = struct else match o with | Eq -> - Some ((Vect.set 0 Q.neg_one Vect.null, Eq), ProofFormat.Gcd (g, prf)) + Some ((Vect.set 0 Q.minus_one Vect.null, Eq), ProofFormat.Gcd (g, prf)) | Gt -> failwith "cutting_plane ignore strict constraints" | Ge -> (* This is a non-trivial common divisor *) @@ -999,7 +999,7 @@ module WithProof = struct | Some (c, p) -> Some (c, ProofFormat.simplify_prf_rule p) let is_substitution strict ((p, o), prf) = - let pred v = if strict then v =/ Q.one || v =/ Q.neg_one else true in + let pred v = if strict then v =/ Q.one || v =/ Q.minus_one else true in match o with Eq -> LinPoly.search_linear pred p | _ -> None let subst1 sys0 = diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml index eaa26ded62..f59d65085a 100644 --- a/plugins/micromega/simplex.ml +++ b/plugins/micromega/simplex.ml @@ -247,8 +247,8 @@ let solve_column (c : var) (r : var) (e : Vect.t) : Vect.t = let a = Vect.get c e in if a =/ Q.zero then failwith "Cannot solve column" else - let a' = Q.neg_one // a in - Vect.mul a' (Vect.set r Q.neg_one (Vect.set c Q.zero e)) + let a' = Q.minus_one // a in + Vect.mul a' (Vect.set r Q.minus_one (Vect.set c Q.zero e)) (** [pivot_row r c e] @param c is such that c = e @@ -364,7 +364,8 @@ let push_real (opt : bool) (nw : var) (v : Vect.t) (rst : Restricted.t) if n >=/ Q.zero then Sat (t', None) else let v' = safe_find "push_real" nw t' in - Unsat (Vect.set nw Q.one (Vect.set 0 Q.zero (Vect.mul Q.neg_one v'))) ) + Unsat (Vect.set nw Q.one (Vect.set 0 Q.zero (Vect.mul Q.minus_one v'))) + ) (** One complication is that equalities needs some pre-processing. *) @@ -399,7 +400,7 @@ let eliminate_equalities (vr0 : var) (l : Polynomial.cstr list) = elim (idx + 1) (vr + 1) (IMap.add vr (idx, true) vm) l ((vr, v) :: acc) | Eq -> let v1 = Vect.set 0 (Q.neg c.cst) c.coeffs in - let v2 = Vect.mul Q.neg_one v1 in + let v2 = Vect.mul Q.minus_one v1 in let vm = IMap.add vr (idx, true) (IMap.add (vr + 1) (idx, false) vm) in elim (idx + 1) (vr + 2) vm l ((vr, v1) :: (vr + 1, v2) :: acc) | Gt -> raise Strict ) diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml index 2b04bb80e2..aeb9d14555 100644 --- a/plugins/micromega/sos.ml +++ b/plugins/micromega/sos.ml @@ -80,7 +80,7 @@ let is_zero (d, v) = match v with Empty -> true | _ -> false (* Vectors. Conventionally indexed 1..n. *) (* ------------------------------------------------------------------------- *) -let vector_0 n = ((n, undefined) : vector) +let vector_0 n : vector = (n, undefined) let dim (v : vector) = fst v let vector_const c n = @@ -99,7 +99,7 @@ let vector_of_list l = (* Matrices; again rows and columns indexed from 1. *) (* ------------------------------------------------------------------------- *) -let matrix_0 (m, n) = (((m, n), undefined) : matrix) +let matrix_0 (m, n) : matrix = ((m, n), undefined) let dimensions (m : matrix) = fst m let matrix_cmul c (m : matrix) = @@ -107,7 +107,7 @@ let matrix_cmul c (m : matrix) = if c =/ Q.zero then matrix_0 (i, j) else ((i, j), mapf (fun x -> c */ x) (snd m)) -let matrix_neg (m : matrix) = ((dimensions m, mapf Q.neg (snd m)) : matrix) +let matrix_neg (m : matrix) : matrix = (dimensions m, mapf Q.neg (snd m)) let matrix_add (m1 : matrix) (m2 : matrix) = let d1 = dimensions m1 and d2 = dimensions m2 in @@ -138,7 +138,7 @@ let diagonal (v : vector) = (* Monomials. *) (* ------------------------------------------------------------------------- *) let monomial_1 = (undefined : monomial) -let monomial_var x = (x |=> 1 : monomial) +let monomial_var x : monomial = x |=> 1 let (monomial_mul : monomial -> monomial -> monomial) = combine ( + ) (fun x -> false) @@ -152,16 +152,16 @@ let monomial_variables m = dom m (* ------------------------------------------------------------------------- *) let poly_0 = (undefined : poly) let poly_isconst (p : poly) = foldl (fun a m c -> m = monomial_1 && a) true p -let poly_var x = (monomial_var x |=> Q.one : poly) +let poly_var x : poly = monomial_var x |=> Q.one let poly_const c = if c =/ Q.zero then poly_0 else monomial_1 |=> c let poly_cmul c (p : poly) = if c =/ Q.zero then poly_0 else mapf (fun x -> c */ x) p -let poly_neg (p : poly) = (mapf Q.neg p : poly) +let poly_neg (p : poly) : poly = mapf Q.neg p -let poly_add (p1 : poly) (p2 : poly) = - (combine ( +/ ) (fun x -> x =/ Q.zero) p1 p2 : poly) +let poly_add (p1 : poly) (p2 : poly) : poly = + combine ( +/ ) (fun x -> x =/ Q.zero) p1 p2 let poly_sub p1 p2 = poly_add p1 (poly_neg p2) @@ -576,7 +576,7 @@ let eliminate_all_equations one = else let v = choose_variable eq in let a = apply eq v in - let eq' = equation_cmul (Q.neg_one // a) (undefine v eq) in + let eq' = equation_cmul (Q.minus_one // a) (undefine v eq) in let elim e = let b = tryapplyd e v Q.zero in if b =/ Q.zero then e @@ -814,7 +814,7 @@ let bmatrix_add = combine ( +/ ) (fun x -> x =/ Q.zero) let bmatrix_cmul c bm = if c =/ Q.zero then undefined else mapf (fun x -> c */ x) bm -let bmatrix_neg = bmatrix_cmul Q.neg_one +let bmatrix_neg = bmatrix_cmul Q.minus_one (* ------------------------------------------------------------------------- *) (* Smash a block matrix into components. *) @@ -943,7 +943,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = List.fold_right (fun k -> List.nth pvs (k - 1) |-> element vec k) (1 -- dim vec) - ((0, 0, 0) |=> Q.neg_one) + ((0, 0, 0) |=> Q.minus_one) in let finalassigs = foldl (fun a v e -> (v |-> equation_eval newassigs e) a) newassigs allassig @@ -1166,7 +1166,7 @@ let sumofsquares_general_symmetry tool pol = match cls with | [] -> raise Sanity | [h] -> acc - | h :: t -> List.map (fun k -> (k |-> Q.neg_one) (h |=> Q.one)) t @ acc + | h :: t -> List.map (fun k -> (k |-> Q.minus_one) (h |=> Q.one)) t @ acc in List.fold_right mk_eq eqvcls [] in @@ -1191,14 +1191,13 @@ let sumofsquares_general_symmetry tool pol = let diagents = end_itlist equation_add (List.map (fun i -> apply allassig (i, i)) (1 -- n)) in - let mk_matrix v = - ( ( (n, n) - , foldl - (fun m (i, j) ass -> - let c = tryapplyd ass v Q.zero in - if c =/ Q.zero then m else ((j, i) |-> c) (((i, j) |-> c) m)) - undefined allassig ) - : matrix ) + let mk_matrix v : matrix = + ( (n, n) + , foldl + (fun m (i, j) ass -> + let c = tryapplyd ass v Q.zero in + if c =/ Q.zero then m else ((j, i) |-> c) (((i, j) |-> c) m)) + undefined allassig ) in let mats = List.map mk_matrix qvars and obj = diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml index 3e0b1f2cd9..4df32f2ba4 100644 --- a/plugins/micromega/vect.ml +++ b/plugins/micromega/vect.ml @@ -52,7 +52,7 @@ let pp_var_num pp_var o {var = v; coe = n} = if Int.equal v 0 then if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n) else if Q.one =/ n then pp_var o v - else if Q.neg_one =/ n then Printf.fprintf o "-%a" pp_var v + else if Q.minus_one =/ n then Printf.fprintf o "-%a" pp_var v else if Q.zero =/ n then () else Printf.fprintf o "%s*%a" (Q.to_string n) pp_var v @@ -60,7 +60,7 @@ let pp_var_num_smt pp_var o {var = v; coe = n} = if Int.equal v 0 then if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n) else if Q.one =/ n then pp_var o v - else if Q.neg_one =/ n then Printf.fprintf o "(- %a)" pp_var v + else if Q.minus_one =/ n then Printf.fprintf o "(- %a)" pp_var v else if Q.zero =/ n then () else Printf.fprintf o "(* %s %a)" (Q.to_string n) pp_var v diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 955a7957bf..f90c143a1a 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -68,7 +68,9 @@ module RelDecl = Context.Rel.Declaration let hid = Id.of_string "H" let xid = Id.of_string "X" let default_id_of_sort = function InSProp | InProp | InSet -> hid | InType -> xid -let fresh env id = next_global_ident_away id Id.Set.empty +let fresh env id avoid = + let freshid = next_global_ident_away id avoid in + freshid, Id.Set.add freshid avoid let with_context_set ctx (b, ctx') = (b, Univ.ContextSet.union ctx ctx') @@ -204,7 +206,7 @@ let build_sym_scheme env ind = let cstr n = mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect mkRel n mib.mind_params_ctxt) in let inds = snd (mind_arity mip) in - let varH = fresh env (default_id_of_sort inds) in + let varH,_ = fresh env (default_id_of_sort inds) Id.Set.empty in let applied_ind = build_dependent_inductive indu specif in let indr = Sorts.relevance_of_sort_family inds in let realsign_ind = @@ -263,7 +265,7 @@ let build_sym_involutive_scheme env ind = let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect mkRel n paramsctxt) in let inds = snd (mind_arity mip) in let indr = Sorts.relevance_of_sort_family inds in - let varH = fresh env (default_id_of_sort inds) in + let varH,_ = fresh env (default_id_of_sort inds) Id.Set.empty in let applied_ind = build_dependent_inductive indu specif in let applied_ind_C = mkApp @@ -380,9 +382,9 @@ let build_l2r_rew_scheme dep env ind kind = rel_vect p nrealargs]) in let inds = snd (mind_arity mip) in let indr = Sorts.relevance_of_sort_family inds in - let varH = fresh env (default_id_of_sort inds) in - let varHC = fresh env (Id.of_string "HC") in - let varP = fresh env (Id.of_string "P") in + let varH,avoid = fresh env (default_id_of_sort inds) Id.Set.empty in + let varHC,avoid = fresh env (Id.of_string "HC") avoid in + let varP,_ = fresh env (Id.of_string "P") avoid in let applied_ind = build_dependent_inductive indu specif in let applied_ind_P = mkApp (mkIndU indu, Array.concat @@ -498,9 +500,9 @@ let build_l2r_forward_rew_scheme dep env ind kind = rel_vect p nrealargs]) in let inds = snd (mind_arity mip) in let indr = Sorts.relevance_of_sort_family inds in - let varH = fresh env (default_id_of_sort inds) in - let varHC = fresh env (Id.of_string "HC") in - let varP = fresh env (Id.of_string "P") in + let varH,avoid = fresh env (default_id_of_sort inds) Id.Set.empty in + let varHC,avoid = fresh env (Id.of_string "HC") avoid in + let varP,_ = fresh env (Id.of_string "P") avoid in let applied_ind = build_dependent_inductive indu specif in let applied_ind_P = mkApp (mkIndU indu, Array.concat @@ -593,9 +595,9 @@ let build_r2l_forward_rew_scheme dep env ind kind = let constrargs_cstr = constrargs@[cstr 0] in let inds = snd (mind_arity mip) in let indr = Sorts.relevance_of_sort_family inds in - let varH = fresh env (default_id_of_sort inds) in - let varHC = fresh env (Id.of_string "HC") in - let varP = fresh env (Id.of_string "P") in + let varH,avoid = fresh env (default_id_of_sort inds) Id.Set.empty in + let varHC,avoid = fresh env (Id.of_string "HC") avoid in + let varP,_ = fresh env (Id.of_string "P") avoid in let applied_ind = build_dependent_inductive indu specif in let realsign_ind = name_context env ((LocalAssum (make_annot (Name varH) indr,applied_ind))::realsign) in @@ -806,9 +808,9 @@ let build_congr env (eq,refl,ctx) ind = if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; let b = List.nth constrargs (i + mib.mind_nparams - 1) in - let varB = fresh env (Id.of_string "B") in - let varH = fresh env (Id.of_string "H") in - let varf = fresh env (Id.of_string "f") in + let varB,avoid = fresh env (Id.of_string "B") Id.Set.empty in + let varH,avoid = fresh env (Id.of_string "H") avoid in + let varf,avoid = fresh env (Id.of_string "f") avoid in let rci = Sorts.Relevant in (* TODO relevance *) let ci = make_case_info (Global.env()) ind rci RegularStyle in let uni, ctx = Univ.extend_in_context_set (UnivGen.new_global_univ ()) ctx in diff --git a/test-suite/.csdp.cache.test-suite b/test-suite/.csdp.cache.test-suite Binary files differindex 046cb067c5..36efdf469e 100644 --- a/test-suite/.csdp.cache.test-suite +++ b/test-suite/.csdp.cache.test-suite diff --git a/test-suite/Makefile b/test-suite/Makefile index 758374c5de..6c373701cf 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -141,7 +141,7 @@ run: $(SUBSYSTEMS) bugs: $(BUGS) clean: - rm -f trace .nia.cache .lia.cache output/MExtraction.out + rm -f trace .csdp.cache .nia.cache .lia.cache output/MExtraction.out rm -f vos/Makefile vos/Makefile.conf $(SHOW) 'RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>' $(HIDE)find . \( \ diff --git a/test-suite/bugs/closed/bug_13003.v b/test-suite/bugs/closed/bug_13003.v new file mode 100644 index 0000000000..570baef2ef --- /dev/null +++ b/test-suite/bugs/closed/bug_13003.v @@ -0,0 +1,9 @@ +Set Mangle Names. +Import EqNotations. +Lemma eq_sigT_sig_eq X P (x1 x2:X) H1 H2 : + forall (E1 : x1=x2), rew E1 in H1 = H2 -> existT P x1 H1 = existT P x2 H2. +Proof. + intros ->. + intros <-. + reflexivity. +Defined. |