diff options
29 files changed, 174 insertions, 194 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index cfa6f84147..16f82a19ee 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-09-07-V22" + CACHEKEY: "bionic_coq-V2020-09-17-V88" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -242,6 +242,11 @@ before_script: - make -f Makefile.ci -j "$NJOBS" "${CI_JOB_NAME#*:}" - echo 'end:coq.test' - set +e + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build_ci + when: always needs: - build:base dependencies: @@ -600,7 +605,7 @@ test-suite:edge:dune:dev: - opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git - opam update - opam install ocaml-variants=$OCAMLVER - - opam install dune num zarith + - opam install dune zarith - eval $(opam env) - export COQ_UNIT_TEST=noop - make -f Makefile.dune test-suite @@ -683,10 +688,6 @@ library:ci-bbv: library:ci-bedrock2: extends: .ci-template-flambda - artifacts: - name: "$CI_JOB_NAME" - paths: - - _build_ci variables: NJOBS: "1" @@ -712,10 +713,6 @@ library:ci-coq_tools: library:ci-coqprime: stage: stage-3 extends: .ci-template-flambda - artifacts: - name: "$CI_JOB_NAME" - paths: - - _build_ci needs: - build:edge+flambda - plugin:ci-bignums @@ -741,10 +738,6 @@ library:ci-fcsl_pcm: library:ci-fiat_crypto: extends: .ci-template-flambda stage: stage-4 - artifacts: - name: "$CI_JOB_NAME" - paths: - - _build_ci needs: - build:edge+flambda - library:ci-coqprime @@ -781,10 +774,6 @@ library:ci-fiat_crypto_ocaml: library:ci-flocq: extends: .ci-template-flambda - artifacts: - name: "$CI_JOB_NAME" - paths: - - _build_ci library:ci-corn: extends: .ci-template-flambda @@ -809,10 +798,6 @@ library:ci-iris: library:ci-math_classes: extends: .ci-template-flambda stage: stage-3 - artifacts: - name: "$CI_JOB_NAME" - paths: - - _build_ci needs: - build:edge+flambda - plugin:ci-bignums @@ -855,10 +840,6 @@ plugin:ci-aac_tactics: plugin:ci-bignums: extends: .ci-template-flambda - artifacts: - name: "$CI_JOB_NAME" - paths: - - _build_ci plugin:ci-coq_dpdgraph: extends: .ci-template @@ -871,10 +852,6 @@ plugin:ci-elpi: plugin:ci-equations: extends: .ci-template - artifacts: - name: "$CI_JOB_NAME" - paths: - - _build_ci plugin:ci-fiat_parsers: extends: .ci-template @@ -920,7 +897,3 @@ plugin:ci-relation_algebra: plugin:ci-rewriter: extends: .ci-template-flambda - artifacts: - name: "$CI_JOB_NAME" - paths: - - _build_ci 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/INSTALL.md b/INSTALL.md index 05a92ca005..51d59e1638 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -15,10 +15,7 @@ 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.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) @@ -35,15 +32,15 @@ To compile Coq yourself, you need: (version >= 3.0.beta8), and the corresponding GTK 3.x libraries, as of today (gtk+3 >= 3.18 and gtksourceview3 >= 3.18) -The IEEE-754 compliance is required by primitive floating-point -numbers (`Require Import Floats`). Common sources of incompatibility -are checked at configure time, preventing compilation. In the, -unlikely, event an incompatibility remains undetected, using Floats -would enable to prove False on this architecture. +Primitive floating-point numbers require IEEE-754 compliance +(`Require Import Floats`). Common sources of incompatibility +are checked at configure time, preventing compilation. In the +unlikely event an incompatibility remains undetected, using `Floats` +would enable proving `False` on this architecture. -Note that `num` and `lablgtk3-sourceview3` should be properly -registered with `findlib/ocamlfind` as Coq's makefile will use it to -locate the libraries during the build. +Note that OCaml dependencies (`zarith` and `lablgtk3-sourceview3` at +this moment) must be properly registered with `findlib/ocamlfind` +since Coq's build system uses `findlib` to locate them. Debian / Ubuntu users can get the necessary system packages for CoqIDE with: @@ -55,7 +52,7 @@ the corresponding packages. $ opam switch create coq 4.11.1+flambda $ eval $(opam env) - $ opam install num ocamlfind lablgtk3-sourceview3 + $ opam install ocamlfind zarith lablgtk3-sourceview3 should get you a reasonable OCaml environment to compile Coq. See the OPAM documentation for more help. diff --git a/META.coq.in b/META.coq.in index 5aaa8cc8a6..a6747c614b 100644 --- a/META.coq.in +++ b/META.coq.in @@ -223,7 +223,7 @@ package "toplevel" ( description = "Coq Toplevel" version = "8.13" - requires = "num, coq.stm" + requires = "coq.stm" directory = "toplevel" archive(byte) = "toplevel.cma" @@ -327,7 +327,7 @@ package "plugins" ( description = "Coq micromega plugin" version = "8.13" - requires = "num, coq.plugins.ltac" + requires = "coq.plugins.ltac" directory = "micromega" archive(byte) = "micromega_plugin.cmo" diff --git a/Makefile.build b/Makefile.build index 061489f47f..eed3c2813a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -302,7 +302,7 @@ $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^ endef # Main packages linked by Coq. -SYSMOD:=-package str,unix,dynlink,threads,num,zarith +SYSMOD:=-package str,unix,dynlink,threads,zarith ########################################################################### # Infrastructure for the rest of the Makefile @@ -587,11 +587,11 @@ CSDPCERTCMO:=clib/clib.cma $(addprefix plugins/micromega/, \ $(CSDPCERT): $(call bestobj, $(CSDPCERTCMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, -package num,unix) + $(HIDE)$(call bestocaml, -package unix) $(CSDPCERTBYTE): $(CSDPCERTCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(call ocamlbyte, -package num,unix) + $(HIDE)$(call ocamlbyte, -package unix) ########################################################################### # tests @@ -707,7 +707,7 @@ COND_OPTFLAGS= \ plugins/micromega/%.cmi: plugins/micromega/%.mli $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< + $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix -c $< %.cmi: %.mli $(SHOW)'OCAMLC $<' @@ -715,7 +715,7 @@ plugins/micromega/%.cmi: plugins/micromega/%.mli plugins/micromega/%.cmo: plugins/micromega/%.ml $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< + $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix -c $< %.cmo: %.ml $(SHOW)'OCAMLC $<' @@ -752,7 +752,7 @@ plugins/micromega/csdpcert_FORPACK:= plugins/micromega/%.cmx: plugins/micromega/%.ml $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix,num -c $< + $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix -c $< plugins/%.cmx: plugins/%.ml $(SHOW)'OCAMLOPT $<' diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 17228bda8a..41b5210f45 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -80,7 +80,7 @@ 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" ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 zarith.1.10 opam list displayName: 'Install OCaml dependencies' env: diff --git a/configure.ml b/configure.ml index 2dbc01651e..43c55af495 100644 --- a/configure.ml +++ b/configure.ml @@ -688,23 +688,16 @@ let operating_system = else (try Sys.getenv "OS" with Not_found -> "") -(** Zarith and num libraries *) - -let check_for_numlib () = - (if caml_version_nums >= [4;6;0] then - let numlib,_ = tryrun camlexec.find ["query";"num"] in - match numlib with - | "" -> - die "Num library not installed, required for OCaml 4.06 or later" - | _ -> cprintf "You have the Num library installed. Good!"); +(** Zarith library *) + +let check_for_zarith () = let zarith,_ = tryrun camlexec.find ["query";"zarith"] in match zarith with | "" -> die "Zarith library not installed, required" | _ -> cprintf "You have the Zarith library installed. Good!" -let numlib = - check_for_numlib () +let numlib = check_for_zarith () (** * lablgtk3 and CoqIDE *) @@ -24,8 +24,7 @@ depends: [ "ocaml" { >= "4.05.0" } "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..74ca68ac0b 100644 --- a/coq.opam.docker +++ b/coq.opam.docker @@ -23,8 +23,7 @@ version: "dev" 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..ffee77f1f7 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; [ 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/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index ee50d25318..f672ead807 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-09-07-V22" +# CACHEKEY: "bionic_coq-V2020-09-17-V88" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -40,10 +40,8 @@ ENV NJOBS="2" \ # Base opam is the set of base packages required by Coq 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.1" \ +# Common OPAM packages +ENV BASE_OPAM="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,7 +57,7 @@ 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 diff --git a/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst b/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst new file mode 100644 index 0000000000..c142eec561 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst @@ -0,0 +1,4 @@ +- **Removed:** + The `num` library is not linked to Coq anymore + (`#13007 <https://github.com/coq/coq/pull/13007>`_, + by Emilio Jesus Gallego Arias). 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/dune b/plugins/micromega/dune index 33ad3a0138..204125ab56 100644 --- a/plugins/micromega/dune +++ b/plugins/micromega/dune @@ -4,7 +4,7 @@ ; be careful not to link the executable to the plugin! (modules (:standard \ csdpcert g_zify zify)) (synopsis "Coq's micromega plugin") - (libraries num coq.plugins.ltac)) + (libraries coq.plugins.ltac)) (executable (name csdpcert) 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 03d2a2d233..aeb9d14555 100644 --- a/plugins/micromega/sos.ml +++ b/plugins/micromega/sos.ml @@ -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 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. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 02ababd928..0ebb97d0bf 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -104,7 +104,7 @@ BEFORE ?= AFTER ?= # FIXME this should be generated by Coq (modules already linked by Coq) -CAMLDONTLINK=str,unix,dynlink,threads,num,zarith +CAMLDONTLINK=str,unix,dynlink,threads,zarith # OCaml binaries CAMLC ?= "$(OCAMLFIND)" ocamlc -c diff --git a/toplevel/dune b/toplevel/dune index 5f10346ac4..98f4ba2edf 100644 --- a/toplevel/dune +++ b/toplevel/dune @@ -3,8 +3,7 @@ (public_name coq.toplevel) (synopsis "Coq's Interactive Shell [terminal-based]") (wrapped false) - ; num still here due to some plugins using it - (libraries num coq.stm)) + (libraries coq.stm)) ; Interp provides the `zarith` library to plugins, we could also use ; -linkall in the plugins file, to be discussed. |