aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml2
-rwxr-xr-xdev/bench/gitlab.sh2
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile2
-rw-r--r--dev/ci/user-overlays/13847-gares-elpi-1.13-coq-elpi-1.9.0.sh1
-rw-r--r--doc/changelog/08-cli-tools/13822-rm-depr-cmdline.rst4
-rw-r--r--doc/changelog/09-coqide/13810-shift-return-search-backwards.rst3
-rw-r--r--ide/coqide/wg_Find.ml16
-rw-r--r--plugins/micromega/certificate.ml70
-rw-r--r--plugins/micromega/polynomial.ml293
-rw-r--r--plugins/micromega/polynomial.mli4
-rw-r--r--sysinit/coqargs.ml39
-rw-r--r--sysinit/coqargs.mli9
-rw-r--r--sysinit/coqinit.ml14
-rw-r--r--sysinit/usage.ml1
-rw-r--r--test-suite/micromega/bug_13794.v39
-rw-r--r--test-suite/output/bug_13821_native_command_line_warn.out0
-rw-r--r--test-suite/output/bug_13821_native_command_line_warn.v1
-rw-r--r--toplevel/coqtop.ml10
-rw-r--r--vernac/vernacentries.mli1
19 files changed, 291 insertions, 220 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4f58dc5aac..10ec39da12 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -20,7 +20,7 @@ variables:
# Format: $IMAGE-V$DATE-$hash
# The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
# echo $(md5sum dev/ci/docker/bionic_coq/Dockerfile | head -c 10)
- CACHEKEY: "bionic_coq-V2020-12-25-95a34df128"
+ CACHEKEY: "bionic_coq-V2021-02-11-b601de5a7b"
IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
# By default, jobs run in the base switch; override to select another switch
OPAM_SWITCH: "base"
diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh
index 2ce3cb77be..569977f76b 100755
--- a/dev/bench/gitlab.sh
+++ b/dev/bench/gitlab.sh
@@ -52,7 +52,7 @@ check_variable "CI_JOB_URL"
: "${new_coq_opam_archive_git_branch:=master}"
: "${old_coq_opam_archive_git_branch:=master}"
: "${num_of_iterations:=1}"
-: "${coq_opam_packages:=coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast coq-perennial coq-vst}"
+: "${coq_opam_packages:=coq-performance-tests-lite coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast coq-perennial coq-vst}"
new_coq_commit=$(git rev-parse HEAD^2)
old_coq_commit=$(git merge-base HEAD^1 $new_coq_commit)
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index b4b6411d28..8f14625c63 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -44,7 +44,7 @@ ENV COMPILER="4.05.0"
# Common OPAM packages
ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \
CI_OPAM="ocamlgraph.1.8.8" \
- BASE_ONLY_OPAM="elpi.1.12.0"
+ BASE_ONLY_OPAM="elpi.1.13.0"
# BASE switch; CI_OPAM contains Coq's CI dependencies.
ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0"
diff --git a/dev/ci/user-overlays/13847-gares-elpi-1.13-coq-elpi-1.9.0.sh b/dev/ci/user-overlays/13847-gares-elpi-1.13-coq-elpi-1.9.0.sh
new file mode 100644
index 0000000000..6847bde6d8
--- /dev/null
+++ b/dev/ci/user-overlays/13847-gares-elpi-1.13-coq-elpi-1.9.0.sh
@@ -0,0 +1 @@
+overlay elpi https://github.com/LPCIC/coq-elpi coq-master+1.9.0 13847
diff --git a/doc/changelog/08-cli-tools/13822-rm-depr-cmdline.rst b/doc/changelog/08-cli-tools/13822-rm-depr-cmdline.rst
new file mode 100644
index 0000000000..e3333f8a9a
--- /dev/null
+++ b/doc/changelog/08-cli-tools/13822-rm-depr-cmdline.rst
@@ -0,0 +1,4 @@
+- **Removed:** previously deprecated command line options
+ ``-sprop-cumulative`` and ``-input-state`` and its alias ``-is``
+ (`#13822 <https://github.com/coq/coq/pull/13822>`_,
+ by Gaëtan Gilbert).
diff --git a/doc/changelog/09-coqide/13810-shift-return-search-backwards.rst b/doc/changelog/09-coqide/13810-shift-return-search-backwards.rst
new file mode 100644
index 0000000000..e78280d91d
--- /dev/null
+++ b/doc/changelog/09-coqide/13810-shift-return-search-backwards.rst
@@ -0,0 +1,3 @@
+- **Added:**
+ Shift-return in the Find dialog now searches backwards (`#13810 <https://github.com/coq/coq/pull/13810>`_,
+ by slrnsc).
diff --git a/ide/coqide/wg_Find.ml b/ide/coqide/wg_Find.ml
index 7e89191bd1..7f30cc8c6c 100644
--- a/ide/coqide/wg_Find.ml
+++ b/ide/coqide/wg_Find.ml
@@ -219,16 +219,18 @@ class finder name (view : GText.view) =
let _ = replace_all_button#connect#clicked ~callback:self#replace_all in
(* Keypress interaction *)
- let generic_cb esc_cb ret_cb ev =
+ let dispatch_key_cb esc_cb ret_cb shift_ret_cb ev =
let ev_key = GdkEvent.Key.keyval ev in
- let (return, _) = GtkData.AccelGroup.parse "Return" in
- let (esc, _) = GtkData.AccelGroup.parse "Escape" in
- if ev_key = return then (ret_cb (); true)
- else if ev_key = esc then (esc_cb (); true)
+ let ev_modifiers = GdkEvent.Key.state ev in
+ if ev_key = GdkKeysyms._Return then
+ (if List.mem `SHIFT ev_modifiers then
+ shift_ret_cb ()
+ else ret_cb (); true)
+ else if ev_key = GdkKeysyms._Escape then (esc_cb (); true)
else false
in
- let find_cb = generic_cb self#hide self#find_forward in
- let replace_cb = generic_cb self#hide self#replace in
+ let find_cb = dispatch_key_cb self#hide self#find_forward self#find_backward in
+ let replace_cb = dispatch_key_cb self#hide self#replace self#replace in
let _ = find_entry#event#connect#key_press ~callback:find_cb in
let _ = replace_entry#event#connect#key_press ~callback:replace_cb in
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index ed608bb1df..53aa619d10 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -223,6 +223,28 @@ let find_point l =
let optimise v l =
if use_simplex () then Simplex.optimise v l else Mfourier.Fourier.optimise v l
+let output_cstr_sys o sys =
+ List.iter
+ (fun (c, wp) ->
+ Printf.fprintf o "%a by %a\n" output_cstr c ProofFormat.output_prf_rule wp)
+ sys
+
+let output_sys o sys =
+ List.iter (fun s -> Printf.fprintf o "%a\n" WithProof.output s) sys
+
+let tr_sys str f sys =
+ let sys' = f sys in
+ if debug then
+ Printf.fprintf stdout "[%s\n%a=>\n%a]\n" str output_sys sys output_sys sys';
+ sys'
+
+let tr_cstr_sys str f sys =
+ let sys' = f sys in
+ if debug then
+ Printf.fprintf stdout "[%s\n%a=>\n%a]\n" str output_cstr_sys sys
+ output_cstr_sys sys';
+ sys'
+
let dual_raw_certificate l =
if debug then begin
Printf.printf "dual_raw_certificate\n";
@@ -375,25 +397,7 @@ let elim_simple_linear_equality sys0 =
in
iterate_until_stable elim sys0
-let output_sys o sys =
- List.iter (fun s -> Printf.fprintf o "%a\n" WithProof.output s) sys
-
-let subst sys =
- let sys' = WithProof.subst sys in
- if debug then
- Printf.fprintf stdout "[subst:\n%a\n==>\n%a\n]" output_sys sys output_sys
- sys';
- sys'
-
-let tr_sys str f sys =
- let sys' = f sys in
- if debug then (
- Printf.fprintf stdout "[%s\n" str;
- List.iter (fun s -> Printf.fprintf stdout "%a\n" WithProof.output s) sys;
- Printf.fprintf stdout "\n => \n";
- List.iter (fun s -> Printf.fprintf stdout "%a\n" WithProof.output s) sys';
- Printf.fprintf stdout "]\n" );
- sys'
+let subst sys = tr_sys "subst" WithProof.subst sys
(** [saturate_linear_equality sys] generate new constraints
obtained by eliminating linear equalities by pivoting.
@@ -489,12 +493,10 @@ let nlinear_preprocess (sys : WithProof.t list) =
ISet.fold (fun i acc -> square_of_var i :: acc) collect_vars sys
in
let sys = sys @ all_pairs WithProof.product sys in
- if debug then begin
- Printf.fprintf stdout "Preprocessed\n";
- List.iter (fun s -> Printf.fprintf stdout "%a\n" WithProof.output s) sys
- end;
List.map (WithProof.annot "P") sys
+let nlinear_preprocess = tr_sys "nlinear_preprocess" nlinear_preprocess
+
let nlinear_prover prfdepth sys =
let sys = develop_constraints prfdepth q_spec sys in
let sys1 = elim_simple_linear_equality sys in
@@ -698,6 +700,15 @@ let pivot v (c1, p1) (c2, p2) =
Some (xpivot cv1 cv2)
else None
+let pivot v c1 c2 =
+ let res = pivot v c1 c2 in
+ ( match res with
+ | None -> ()
+ | Some (c, _) ->
+ if Vect.get v c.coeffs =/ Q.zero then ()
+ else Printf.printf "pivot error %a\n" output_cstr c );
+ res
+
(* op2 could be Eq ... this might happen *)
let simpl_sys sys =
@@ -762,6 +773,8 @@ let reduce_coprime psys =
in
Some (pivot_sys v (cstr, prf) ((c1, p1) :: sys))
+(*let pivot_sys v pc sys = tr_cstr_sys "pivot_sys" (pivot_sys v pc) sys*)
+
(** If there is an equation [eq] of the form 1.x + e = c, do a pivot over x with equation [eq] *)
let reduce_unary psys =
let is_unary_equation (cstr, prf) =
@@ -820,6 +833,8 @@ let reduction_equations psys =
[reduce_unary; reduce_coprime; reduce_var_change (*; reduce_pivot*)])
psys
+let reduction_equations = tr_cstr_sys "reduction_equations" reduction_equations
+
(** [get_bound sys] returns upon success an interval (lb,e,ub) with proofs *)
let get_bound sys =
let is_small (v, i) =
@@ -891,11 +906,6 @@ let check_sys sys =
open ProofFormat
-let output_cstr_sys sys =
- (pp_list ";" (fun o (c, wp) ->
- Printf.fprintf o "%a by %a" output_cstr c ProofFormat.output_prf_rule wp))
- sys
-
let xlia (can_enum : bool) reduction_equations sys =
let rec enum_proof (id : int) (sys : prf_sys) =
if debug then (
@@ -1170,7 +1180,9 @@ let nlia enum prfdepth sys =
No: if a wrong equation is chosen, the proof may fail.
It would only be safe if the variable is linear...
*)
- let sys1 = elim_simple_linear_equality sys in
+ let sys1 =
+ elim_simple_linear_equality (WithProof.subst_constant true sys)
+ in
let sys2 = saturate_by_linear_equalities sys1 in
let sys3 = nlinear_preprocess (sys1 @ sys2) in
let sys4 = make_cstr_system (*sys2@*) sys3 in
diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index 7b29aa15f9..024fc6dade 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.ml
@@ -485,7 +485,7 @@ module ProofFormat = struct
let rec output_proof o = function
| Done -> Printf.fprintf o "."
| Step (i, p, pf) ->
- Printf.fprintf o "%i:= %a ; %a" i output_prf_rule p output_proof pf
+ Printf.fprintf o "%i:= %a\n ; %a" i output_prf_rule p output_proof pf
| Split (i, v, p1, p2) ->
Printf.fprintf o "%i:=%a ; { %a } { %a }" i Vect.pp v output_proof p1
output_proof p2
@@ -496,6 +496,48 @@ module ProofFormat = struct
Printf.fprintf o "%i := %i = %i - %i ; %i := %i >= 0 ; %i := %i >= 0 ; %a"
i x z t j z k t output_proof pr
+ module OrdPrfRule = struct
+ type t = prf_rule
+
+ let id_of_constr = function
+ | Annot _ -> 0
+ | Hyp _ -> 1
+ | Def _ -> 2
+ | Cst _ -> 3
+ | Zero -> 4
+ | Square _ -> 5
+ | MulC _ -> 6
+ | Gcd _ -> 7
+ | MulPrf _ -> 8
+ | AddPrf _ -> 9
+ | CutPrf _ -> 10
+
+ let cmp_pair c1 c2 (x1, x2) (y1, y2) =
+ match c1 x1 y1 with 0 -> c2 x2 y2 | i -> i
+
+ let rec compare p1 p2 =
+ match (p1, p2) with
+ | Annot (s1, p1), Annot (s2, p2) ->
+ if s1 = s2 then compare p1 p2 else String.compare s1 s2
+ | Hyp i, Hyp j -> Int.compare i j
+ | Def i, Def j -> Int.compare i j
+ | Cst n, Cst m -> Q.compare n m
+ | Zero, Zero -> 0
+ | Square v1, Square v2 -> Vect.compare v1 v2
+ | MulC (v1, p1), MulC (v2, p2) ->
+ cmp_pair Vect.compare compare (v1, p1) (v2, p2)
+ | Gcd (b1, p1), Gcd (b2, p2) ->
+ cmp_pair Z.compare compare (b1, p1) (b2, p2)
+ | MulPrf (p1, q1), MulPrf (p2, q2) ->
+ cmp_pair compare compare (p1, q1) (p2, q2)
+ | AddPrf (p1, q1), AddPrf (p2, q2) ->
+ cmp_pair compare compare (p1, q1) (p2, q2)
+ | CutPrf p, CutPrf p' -> compare p p'
+ | _, _ -> Int.compare (id_of_constr p1) (id_of_constr p2)
+ end
+
+ module PrfRuleMap = Map.Make (OrdPrfRule)
+
let rec pr_size = function
| Annot (_, p) -> pr_size p
| Zero | Square _ -> Q.zero
@@ -537,33 +579,38 @@ module ProofFormat = struct
(** [pr_rule_def_cut id pr] gives an explicit [id] to cut rules.
This is because the Coq proof format only accept they as a proof-step *)
- let rec pr_rule_def_cut id = function
- | Annot (_, p) -> pr_rule_def_cut id p
- | MulC (p, prf) ->
- let bds, id', prf' = pr_rule_def_cut id prf in
- (bds, id', MulC (p, prf'))
- | MulPrf (p1, p2) ->
- let bds1, id, p1 = pr_rule_def_cut id p1 in
- let bds2, id, p2 = pr_rule_def_cut id p2 in
- (bds2 @ bds1, id, MulPrf (p1, p2))
- | AddPrf (p1, p2) ->
- let bds1, id, p1 = pr_rule_def_cut id p1 in
- let bds2, id, p2 = pr_rule_def_cut id p2 in
- (bds2 @ bds1, id, AddPrf (p1, p2))
- | CutPrf p ->
- let bds, id, p = pr_rule_def_cut id p in
- ((id, p) :: bds, id + 1, Def id)
- | Gcd (c, p) ->
- let bds, id, p = pr_rule_def_cut id p in
- ((id, p) :: bds, id + 1, Def id)
- | (Square _ | Cst _ | Def _ | Hyp _ | Zero) as x -> ([], id, x)
+ let pr_rule_def_cut m id p =
+ let rec pr_rule_def_cut m id = function
+ | Annot (_, p) -> pr_rule_def_cut m id p
+ | MulC (p, prf) ->
+ let bds, m, id', prf' = pr_rule_def_cut m id prf in
+ (bds, m, id', MulC (p, prf'))
+ | MulPrf (p1, p2) ->
+ let bds1, m, id, p1 = pr_rule_def_cut m id p1 in
+ let bds2, m, id, p2 = pr_rule_def_cut m id p2 in
+ (bds2 @ bds1, m, id, MulPrf (p1, p2))
+ | AddPrf (p1, p2) ->
+ let bds1, m, id, p1 = pr_rule_def_cut m id p1 in
+ let bds2, m, id, p2 = pr_rule_def_cut m id p2 in
+ (bds2 @ bds1, m, id, AddPrf (p1, p2))
+ | CutPrf p | Gcd (_, p) -> (
+ let bds, m, id, p = pr_rule_def_cut m id p in
+ try
+ let id' = PrfRuleMap.find p m in
+ (bds, m, id, Def id')
+ with Not_found ->
+ let m = PrfRuleMap.add p id m in
+ ((id, p) :: bds, m, id + 1, Def id) )
+ | (Square _ | Cst _ | Def _ | Hyp _ | Zero) as x -> ([], m, id, x)
+ in
+ pr_rule_def_cut m id p
(* Do not define top-level cuts *)
- let pr_rule_def_cut id = function
+ let pr_rule_def_cut m id = function
| CutPrf p ->
- let bds, ids, p' = pr_rule_def_cut id p in
- (bds, ids, CutPrf p')
- | p -> pr_rule_def_cut id p
+ let bds, m, ids, p' = pr_rule_def_cut m id p in
+ (bds, m, ids, CutPrf p')
+ | p -> pr_rule_def_cut m id p
let rec implicit_cut p = match p with CutPrf p -> implicit_cut p | _ -> p
@@ -577,6 +624,69 @@ module ProofFormat = struct
| MulPrf (p1, p2) | AddPrf (p1, p2) ->
ISet.union (pr_rule_collect_defs p1) (pr_rule_collect_defs p2)
+ let add_proof x y =
+ match (x, y) with Zero, p | p, Zero -> p | _ -> AddPrf (x, y)
+
+ let rec mul_cst_proof c p =
+ match p with
+ | Annot (s, p) -> Annot (s, mul_cst_proof c p)
+ | MulC (v, p') -> MulC (Vect.mul c v, p')
+ | _ -> (
+ match Q.sign c with
+ | 0 -> Zero (* This is likely to be a bug *)
+ | -1 ->
+ MulC (LinPoly.constant c, p) (* [p] should represent an equality *)
+ | 1 -> if Q.one =/ c then p else MulPrf (Cst c, p)
+ | _ -> assert false )
+
+ let sMulC v p =
+ let c, v' = Vect.decomp_cst v in
+ if Vect.is_null v' then mul_cst_proof c p else MulC (v, p)
+
+ let mul_proof p1 p2 =
+ match (p1, p2) with
+ | Zero, _ | _, Zero -> Zero
+ | Cst c, p | p, Cst c -> mul_cst_proof c p
+ | _, _ -> MulPrf (p1, p2)
+
+ let prf_rule_of_map m =
+ PrfRuleMap.fold (fun k v acc -> add_proof (sMulC v k) acc) m Zero
+
+ let rec dev_prf_rule p =
+ match p with
+ | Annot (s, p) -> dev_prf_rule p
+ | Hyp _ | Def _ | Cst _ | Zero | Square _ ->
+ PrfRuleMap.singleton p (LinPoly.constant Q.one)
+ | MulC (v, p) ->
+ PrfRuleMap.map (fun v1 -> LinPoly.product v v1) (dev_prf_rule p)
+ | AddPrf (p1, p2) ->
+ PrfRuleMap.merge
+ (fun k o1 o2 ->
+ match (o1, o2) with
+ | None, None -> None
+ | None, Some v | Some v, None -> Some v
+ | Some v1, Some v2 -> Some (LinPoly.addition v1 v2))
+ (dev_prf_rule p1) (dev_prf_rule p2)
+ | MulPrf (p1, p2) -> (
+ let p1' = dev_prf_rule p1 in
+ let p2' = dev_prf_rule p2 in
+ let p1'' = prf_rule_of_map p1' in
+ let p2'' = prf_rule_of_map p2' in
+ match p1'' with
+ | Cst c -> PrfRuleMap.map (fun v1 -> Vect.mul c v1) p2'
+ | _ -> PrfRuleMap.singleton (MulPrf (p1'', p2'')) (LinPoly.constant Q.one)
+ )
+ | Gcd (c, p) ->
+ PrfRuleMap.singleton
+ (Gcd (c, prf_rule_of_map (dev_prf_rule p)))
+ (LinPoly.constant Q.one)
+ | CutPrf p ->
+ PrfRuleMap.singleton
+ (CutPrf (prf_rule_of_map (dev_prf_rule p)))
+ (LinPoly.constant Q.one)
+
+ let simplify_prf_rule p = prf_rule_of_map (dev_prf_rule p)
+
(** [simplify_proof p] removes proof steps that are never re-used. *)
let rec simplify_proof p =
match p with
@@ -618,7 +728,9 @@ module ProofFormat = struct
| Done -> (id, Done)
| Step (i, Gcd (c, p), Done) -> normalise_proof id (Step (i, p, Done))
| Step (i, p, prf) ->
- let bds, id, p' = pr_rule_def_cut id p in
+ let bds, m, id, p' =
+ pr_rule_def_cut PrfRuleMap.empty id (simplify_prf_rule p)
+ in
let id, prf = normalise_proof id prf in
let prf =
List.fold_left
@@ -642,8 +754,10 @@ module ProofFormat = struct
(List.fold_left max 0 ids ,
Enum(i,p1,v,p2,prfs))
*)
- let bds1, id, p1' = pr_rule_def_cut id (implicit_cut p1) in
- let bds2, id, p2' = pr_rule_def_cut id (implicit_cut p2) in
+ let bds1, m, id, p1' =
+ pr_rule_def_cut PrfRuleMap.empty id (implicit_cut p1)
+ in
+ let bds2, m, id, p2' = pr_rule_def_cut m id (implicit_cut p2) in
let ids, prfs = List.split (List.map (normalise_proof id) pl) in
( List.fold_left max 0 ids
, List.fold_left
@@ -659,104 +773,6 @@ module ProofFormat = struct
(snd res);
res
- module OrdPrfRule = struct
- type t = prf_rule
-
- let id_of_constr = function
- | Annot _ -> 0
- | Hyp _ -> 1
- | Def _ -> 2
- | Cst _ -> 3
- | Zero -> 4
- | Square _ -> 5
- | MulC _ -> 6
- | Gcd _ -> 7
- | MulPrf _ -> 8
- | AddPrf _ -> 9
- | CutPrf _ -> 10
-
- let cmp_pair c1 c2 (x1, x2) (y1, y2) =
- match c1 x1 y1 with 0 -> c2 x2 y2 | i -> i
-
- let rec compare p1 p2 =
- match (p1, p2) with
- | Annot (s1, p1), Annot (s2, p2) ->
- if s1 = s2 then compare p1 p2 else String.compare s1 s2
- | Hyp i, Hyp j -> Int.compare i j
- | Def i, Def j -> Int.compare i j
- | Cst n, Cst m -> Q.compare n m
- | Zero, Zero -> 0
- | Square v1, Square v2 -> Vect.compare v1 v2
- | MulC (v1, p1), MulC (v2, p2) ->
- cmp_pair Vect.compare compare (v1, p1) (v2, p2)
- | Gcd (b1, p1), Gcd (b2, p2) ->
- cmp_pair Z.compare compare (b1, p1) (b2, p2)
- | MulPrf (p1, q1), MulPrf (p2, q2) ->
- cmp_pair compare compare (p1, p2) (q1, q2)
- | AddPrf (p1, q1), AddPrf (p2, q2) ->
- cmp_pair compare compare (p1, p2) (q1, q2)
- | CutPrf p, CutPrf p' -> compare p p'
- | _, _ -> Int.compare (id_of_constr p1) (id_of_constr p2)
- end
-
- let add_proof x y =
- match (x, y) with Zero, p | p, Zero -> p | _ -> AddPrf (x, y)
-
- let rec mul_cst_proof c p =
- match p with
- | Annot (s, p) -> Annot (s, mul_cst_proof c p)
- | MulC (v, p') -> MulC (Vect.mul c v, p')
- | _ -> (
- match Q.sign c with
- | 0 -> Zero (* This is likely to be a bug *)
- | -1 ->
- MulC (LinPoly.constant c, p) (* [p] should represent an equality *)
- | 1 -> if Q.one =/ c then p else MulPrf (Cst c, p)
- | _ -> assert false )
-
- let sMulC v p =
- let c, v' = Vect.decomp_cst v in
- if Vect.is_null v' then mul_cst_proof c p else MulC (v, p)
-
- let mul_proof p1 p2 =
- match (p1, p2) with
- | Zero, _ | _, Zero -> Zero
- | Cst c, p | p, Cst c -> mul_cst_proof c p
- | _, _ -> MulPrf (p1, p2)
-
- module PrfRuleMap = Map.Make (OrdPrfRule)
-
- let prf_rule_of_map m =
- PrfRuleMap.fold (fun k v acc -> add_proof (sMulC v k) acc) m Zero
-
- let rec dev_prf_rule p =
- match p with
- | Annot (s, p) -> dev_prf_rule p
- | Hyp _ | Def _ | Cst _ | Zero | Square _ ->
- PrfRuleMap.singleton p (LinPoly.constant Q.one)
- | MulC (v, p) ->
- PrfRuleMap.map (fun v1 -> LinPoly.product v v1) (dev_prf_rule p)
- | AddPrf (p1, p2) ->
- PrfRuleMap.merge
- (fun k o1 o2 ->
- match (o1, o2) with
- | None, None -> None
- | None, Some v | Some v, None -> Some v
- | Some v1, Some v2 -> Some (LinPoly.addition v1 v2))
- (dev_prf_rule p1) (dev_prf_rule p2)
- | MulPrf (p1, p2) -> (
- let p1' = dev_prf_rule p1 in
- let p2' = dev_prf_rule p2 in
- let p1'' = prf_rule_of_map p1' in
- let p2'' = prf_rule_of_map p2' in
- match p1'' with
- | Cst c -> PrfRuleMap.map (fun v1 -> Vect.mul c v1) p2'
- | _ -> PrfRuleMap.singleton (MulPrf (p1'', p2'')) (LinPoly.constant Q.one)
- )
- | _ -> PrfRuleMap.singleton p (LinPoly.constant Q.one)
-
- let simplify_prf_rule p = prf_rule_of_map (dev_prf_rule p)
-
(*
let mul_proof p1 p2 =
let res = mul_proof p1 p2 in
@@ -835,7 +851,8 @@ module ProofFormat = struct
Printf.printf "cmpl_pol_z %s %a\n" (Printexc.to_string x) LinPoly.pp lp;
raise x
- let rec cmpl_proof env = function
+ let rec cmpl_proof env prf =
+ match prf with
| Done -> Mc.DoneProof
| Step (i, p, prf) -> (
match p with
@@ -1097,15 +1114,33 @@ module WithProof = struct
in
List.sort cmp (List.rev_map (fun wp -> (size wp, wp)) sys)
- let subst sys0 =
+ let iterate_pivot p sys0 =
let elim sys =
- let oeq, sys' = extract (is_substitution true) sys in
+ let oeq, sys' = extract p sys in
match oeq with
| None -> None
| Some (v, pc) -> simplify (linear_pivot sys0 pc v) sys'
in
iterate_until_stable elim (List.map snd (sort sys0))
+ let subst_constant is_int sys =
+ let is_integer q = Q.(q =/ floor q) in
+ let is_constant ((c, o), p) =
+ match o with
+ | Ge | Gt -> None
+ | Eq -> (
+ Vect.Bound.(
+ match of_vect c with
+ | None -> None
+ | Some b ->
+ if (not is_int) || is_integer (b.cst // b.coeff) then
+ Monomial.get_var (LinPoly.MonT.retrieve b.var)
+ else None) )
+ in
+ iterate_pivot is_constant sys
+
+ let subst sys0 = iterate_pivot (is_substitution true) sys0
+
let saturate_subst b sys0 =
let select = is_substitution b in
let gen (v, pc) ((c, op), prf) =
diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli
index 84b5421207..81c131fe78 100644
--- a/plugins/micromega/polynomial.mli
+++ b/plugins/micromega/polynomial.mli
@@ -393,6 +393,10 @@ module WithProof : sig
val subst : t list -> t list
+ (** [subst_constant b sys] performs the equivalent of the 'subst' tactic of Coq
+ only if there is an equation a.x = c for a,c a constant and a divides c if b= true*)
+ val subst_constant : bool -> t list -> t list
+
(** [subst1 sys] performs a single substitution *)
val subst1 : t list -> t list
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index c4f12f6bb7..56d88e6bd6 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -44,6 +44,7 @@ type option_command =
type injection_command =
| OptionInjection of (Goptions.option_name * option_command)
| RequireInjection of (string * string option * bool option)
+ | WarnNoNative of string
type coqargs_logic_config = {
impredicative_set : Declarations.set_predicativity;
@@ -75,8 +76,6 @@ type coqargs_pre = {
load_vernacular_list : (string * bool) list;
injections : injection_command list;
-
- inputstate : string option;
}
type coqargs_query =
@@ -133,7 +132,6 @@ let default_pre = {
vo_includes = [];
load_vernacular_list = [];
injections = [];
- inputstate = None;
}
let default_queries = []
@@ -184,18 +182,6 @@ let set_query opts q =
| Queries queries -> Queries (queries@[q])
}
-let warn_deprecated_sprop_cumul =
- CWarnings.create ~name:"deprecated-spropcumul" ~category:"deprecated"
- (fun () -> Pp.strbrk "Use the \"Cumulative StrictProp\" flag instead.")
-
-let warn_deprecated_inputstate =
- CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
- (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.")
-
-let set_inputstate opts s =
- warn_deprecated_inputstate ();
- { opts with pre = { opts.pre with inputstate = Some s }}
-
(******************************************************************************)
(* Parsing helpers *)
(******************************************************************************)
@@ -255,12 +241,6 @@ let parse_option_set opt =
let v = String.sub opt (eqi+1) (len - eqi - 1) in
to_opt_key (String.sub opt 0 eqi), Some v
-let warn_no_native_compiler =
- CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
- Pp.(fun s -> strbrk "Native compiler is disabled," ++
- strbrk " -native-compiler " ++ strbrk s ++
- strbrk " option ignored.")
-
let get_native_compiler s =
(* We use two boolean flags because the four states make sense, even if
only three are accessible to the user at the moment. The selection of the
@@ -274,10 +254,8 @@ let get_native_compiler s =
| _ ->
error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in
if Coq_config.native_compiler = NativeOff && n <> NativeOff then
- let () = warn_no_native_compiler s in
- NativeOff
- else
- n
+ NativeOff, Some (WarnNoNative s)
+ else n, None
(* Main parsing routine *)
(*s Parsing of the command line *)
@@ -333,9 +311,6 @@ let parse_args ~usage ~init arglist : t * string list =
|"-init-file" ->
{ oval with config = { oval.config with rcfile = Some (next ()); }}
- |"-inputstate"|"-is" ->
- set_inputstate oval (next ())
-
|"-load-vernac-object" ->
add_vo_require oval (next ()) None None
@@ -385,8 +360,9 @@ let parse_args ~usage ~init arglist : t * string list =
{ oval with config = { oval.config with enable_VM = get_bool ~opt (next ()) }}
|"-native-compiler" ->
- let native_compiler = get_native_compiler (next ()) in
- { oval with config = { oval.config with native_compiler }}
+ let native_compiler, warn = get_native_compiler (next ()) in
+ { oval with config = { oval.config with native_compiler };
+ pre = { oval.pre with injections = Option.List.cons warn oval.pre.injections }}
| "-set" ->
let opt, v = parse_option_set @@ next() in
@@ -419,9 +395,6 @@ let parse_args ~usage ~init arglist : t * string list =
add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None)
|"-disallow-sprop" ->
add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset
- |"-sprop-cumulative" ->
- warn_deprecated_sprop_cumul();
- add_set_option oval Vernacentries.cumul_sprop_opt_name (OptionSet None)
|"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
|"-m"|"--memory" -> { oval with post = { memory_stat = true }}
|"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli
index aef50193f2..9725a849a4 100644
--- a/sysinit/coqargs.mli
+++ b/sysinit/coqargs.mli
@@ -28,7 +28,12 @@ type injection_command =
ready. Parameters follow [Library], that is to say,
[lib,prefix,import_export] means require library [lib] from
optional [prefix] and [import_export] if [Some false/Some true]
- is used. *)
+ is used. *)
+ | WarnNoNative of string
+ (** Used so that "-w -native-compiler-disabled -native-compiler yes"
+ does not cause a warning. The native option must be processed
+ before injections (because it affects require), so the
+ instruction to emit a message is separated. *)
type coqargs_logic_config = {
impredicative_set : Declarations.set_predicativity;
@@ -60,8 +65,6 @@ type coqargs_pre = {
load_vernacular_list : (string * bool) list;
injections : injection_command list;
-
- inputstate : string option;
}
type coqargs_query =
diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml
index 16c8389de5..25da2c5302 100644
--- a/sysinit/coqinit.ml
+++ b/sysinit/coqinit.ml
@@ -126,10 +126,16 @@ let require_file (dir, from, exp) =
let mfrom = Option.map Libnames.qualid_of_string from in
Flags.silently (Vernacentries.vernac_require mfrom exp) [mp]
-let handle_injection = function
- | Coqargs.RequireInjection r -> require_file r
- (* | LoadInjection l -> *)
- | Coqargs.OptionInjection o -> Coqargs.set_option o
+let warn_no_native_compiler =
+ CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
+ Pp.(fun s -> strbrk "Native compiler is disabled," ++
+ strbrk " -native-compiler " ++ strbrk s ++
+ strbrk " option ignored.")
+
+let handle_injection = let open Coqargs in function
+ | RequireInjection r -> require_file r
+ | OptionInjection o -> set_option o
+ | WarnNoNative s -> warn_no_native_compiler s
let start_library ~top injections =
Flags.verbosely Declaremods.start_library top;
diff --git a/sysinit/usage.ml b/sysinit/usage.ml
index 1831a3f9b2..763cd54137 100644
--- a/sysinit/usage.ml
+++ b/sysinit/usage.ml
@@ -79,7 +79,6 @@ let print_usage_common co command =
\n -impredicative-set set sort Set impredicative\
\n -allow-sprop allow using the proof irrelevant SProp sort\
\n -disallow-sprop forbid using the proof irrelevant SProp sort\
-\n -sprop-cumulative make sort SProp cumulative with the rest of the hierarchy\
\n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\
\n -type-in-type disable universe consistency checking\
\n -mangle-names x mangle auto-generated names using prefix x\
diff --git a/test-suite/micromega/bug_13794.v b/test-suite/micromega/bug_13794.v
new file mode 100644
index 0000000000..5e303a0b7f
--- /dev/null
+++ b/test-suite/micromega/bug_13794.v
@@ -0,0 +1,39 @@
+From Coq Require Import Lia ZArith.ZArith NArith.NArith.
+Unset Nia Cache.
+
+Open Scope N_scope.
+
+
+Lemma over (n0 n1 n2 n3 n4 n5 n6 : N)
+ (e0 : 1 + 8 * n0 = n1 * n1 + n2)
+ (e1 : n1 - 1 = 2 * n3 + n4)
+ (e2 : n3 * (1 + n3) = 2 * n5)
+ (e3 : n2 + 2 * n4 * n1 - n4 = 8 * n6)
+ (o0 : n4 = 0 \/ n4 = 1) :
+ n6 = n0 - n5.
+Proof.
+ Time nia.
+Qed.
+
+Lemma over2 (n0 n1 n2 n3 n4 n5 n6 : N)
+ (e0 : 1 + 8 * n0 = n1 * n1 + n2)
+ (e1 : n1 + 1 = 2 * n3 + n4)
+ (e2 : n3 * (1 + n3) = 2 * n5)
+ (e3 : n2 + 2 * n4 * n1 + n4 = 8 * n6)
+ (o0 : n4 = 0) :
+ n6 = n0 + n5.
+Proof.
+ Fail nia.
+Abort.
+
+Open Scope Z_scope.
+
+Lemma over3 (n1 n2 n3 n4 n5 : Z)
+ (e : 0 <= n1 /\ 0 <= n2 /\ 0 <= n3 /\ 0 <= n4
+ /\ 0 <= n5)
+ (e1 : n1 + 1 = 20 * n3 + n4)
+ (e3 : n2 + 2 * n4 * n1 + n4 = 8 * n5) :
+ n5 = 0.
+Proof.
+Time Fail nia.
+Abort.
diff --git a/test-suite/output/bug_13821_native_command_line_warn.out b/test-suite/output/bug_13821_native_command_line_warn.out
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/output/bug_13821_native_command_line_warn.out
diff --git a/test-suite/output/bug_13821_native_command_line_warn.v b/test-suite/output/bug_13821_native_command_line_warn.v
new file mode 100644
index 0000000000..a28210b6c2
--- /dev/null
+++ b/test-suite/output/bug_13821_native_command_line_warn.v
@@ -0,0 +1 @@
+(* -*- coq-prog-args: ("-w" "-native-compiler-disabled" "-native-compiler" "ondemand"); -*- *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index caf86ef870..16028be910 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -35,14 +35,6 @@ let print_header () =
(******************************************************************************)
-(* Input/Output State *)
-(******************************************************************************)
-let inputstate opts =
- Option.iter (fun istate_file ->
- let fname = Loadpath.locate_file (CUnix.make_suffix istate_file ".coq") in
- Vernacstate.System.load fname) opts.inputstate
-
-(******************************************************************************)
(* Fatal Errors *)
(******************************************************************************)
@@ -70,8 +62,6 @@ let init_toplevel { parse_extra; init_extra; usage; initial_args } =
let opts, customopts = Coqinit.parse_arguments ~parse_extra ~usage ~initial_args () in
Stm.init_process (snd customopts);
let injections = Coqinit.init_runtime opts in
- (* Allow the user to load an arbitrary state here *)
- inputstate opts.pre;
(* This state will be shared by all the documents *)
Stm.init_core ();
let customstate = init_extra ~opts customopts injections in
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index cf233248d7..2ac8458ad5 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -26,4 +26,3 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
val command_focus : unit Proof.focus_kind
val allow_sprop_opt_name : string list
-val cumul_sprop_opt_name : string list
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 05:11:38 +0000