aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml2
-rw-r--r--Makefile.ci2
-rwxr-xr-xdev/ci/ci-fiat-crypto.sh8
-rw-r--r--doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst9
-rw-r--r--doc/sphinx/addendum/micromega.rst6
-rw-r--r--kernel/safe_typing.ml10
-rw-r--r--kernel/safe_typing.mli4
-rw-r--r--library/global.mli4
-rw-r--r--plugins/micromega/coq_micromega.ml30
-rw-r--r--plugins/micromega/coq_micromega.mli2
-rw-r--r--plugins/micromega/g_micromega.mlg7
-rw-r--r--plugins/micromega/simplex.ml142
-rw-r--r--plugins/micromega/simplex.mli14
-rw-r--r--tactics/declare.ml74
-rw-r--r--test-suite/bugs/closed/bug_5617.v8
-rw-r--r--test-suite/micromega/bug_11436.v19
-rw-r--r--test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v4
-rw-r--r--test-suite/micromega/square.v10
18 files changed, 255 insertions, 100 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 73b979c6a3..b39e74ffee 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -632,13 +632,11 @@ library:ci-fiat-crypto:
stage: stage-4
needs:
- build:edge+flambda
- - library:ci-bedrock2
- library:ci-coqprime
- plugin:ci-bignums
- plugin:ci-rewriter
dependencies:
- build:edge+flambda
- - library:ci-bedrock2
- library:ci-coqprime
- plugin:ci-rewriter
diff --git a/Makefile.ci b/Makefile.ci
index 4fc0e69748..10c3b027c3 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -65,7 +65,7 @@ ci-math-classes: ci-bignums
ci-corn: ci-math-classes
-ci-fiat-crypto: ci-bedrock2 ci-coqprime ci-rewriter
+ci-fiat-crypto: ci-coqprime ci-rewriter
ci-simple-io: ci-ext-lib
ci-quickchick: ci-ext-lib ci-simple-io
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 000c418137..811fefda35 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -9,11 +9,15 @@ git_download fiat_crypto
# We need a larger stack size to not overflow ocamlopt+flambda when
# building the executables.
# c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241
+fiat_crypto_CI_STACKSIZE=32768
-fiat_crypto_CI_MAKE_ARGS="EXTERNAL_DEPENDENCIES=1"
+# fiat-crypto is not guaranteed to build with the latest version of
+# bedrock2, so we use the pinned version of bedrock2, but the external
+# version of other developments
+fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1"
fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml c-files rust-files printlite lite"
fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all"
( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
- ulimit -s 32768 && \
+ ulimit -s ${fiat_crypto_CI_STACKSIZE} && \
make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} )
diff --git a/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst b/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst
new file mode 100644
index 0000000000..2a341261e5
--- /dev/null
+++ b/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst
@@ -0,0 +1,9 @@
+- **Added:**
+ :cmd:`Show Lia Profile` prints some statistics about :tacn:`lia` calls.
+ (`#11474 <https://github.com/coq/coq/pull/11474>`_, by Frédéric Besson).
+
+- **Fixed:**
+ Efficiency regression of ``lia``
+ (`#11474 <https://github.com/coq/coq/pull/11474>`_,
+ fixes `#11436 <https://github.com/coq/coq/issues/11436>`_,
+ by Frédéric Besson).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index cc19c8b6a9..b0197c500c 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -35,6 +35,12 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`,
use the Simplex method for solving linear goals. If it is not set,
the decision procedures are using Fourier elimination.
+.. cmd:: Show Lia Profile
+
+ This command prints some statistics about the amount of pivoting
+ operations needed by :tacn:`lia` and may be useful to detect
+ inefficiencies (only meaningful if flag :flag:`Simplex` is set).
+
.. flag:: Lia Cache
This flag (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache`
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e8adde2605..8db8a044a8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -759,7 +759,7 @@ let translate_direct_opaque env kn ce =
let () = assert (is_empty_private u) in
{ cb with const_body = OpaqueDef c }
-let export_side_effects mb env (b_ctx, eff) =
+let export_side_effects mb env eff =
let not_exists e = not (Environ.mem_constant e.seff_constant env) in
let aux (acc,sl) e =
if not (not_exists e) then acc, sl
@@ -776,7 +776,7 @@ let export_side_effects mb env (b_ctx, eff) =
in
let rec translate_seff sl seff acc env =
match seff with
- | [] -> List.rev acc, b_ctx
+ | [] -> List.rev acc
| eff :: rest ->
if Int.equal sl 0 then
let env, cb =
@@ -805,8 +805,8 @@ let push_opaque_proof pf senv =
let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
senv, o
-let export_private_constants ce senv =
- let exported, ce = export_side_effects senv.revstruct senv.env ce in
+let export_private_constants eff senv =
+ let exported = export_side_effects senv.revstruct senv.env eff in
let map senv (kn, c) = match c.const_body with
| OpaqueDef p ->
let local = empty_private c.const_universes in
@@ -819,7 +819,7 @@ let export_private_constants ce senv =
let exported = List.map (fun (kn, _) -> kn) exported in
(* No delayed constants to declare *)
let senv = List.fold_left add_constant_aux senv bodies in
- (ce, exported), senv
+ exported, senv
let add_constant l decl senv =
let kn = Constant.make2 senv.modpath l in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index e6f2fc4a5d..e472dfd5e5 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -86,8 +86,8 @@ type side_effect_declaration =
type exported_private_constant = Constant.t
val export_private_constants :
- private_constants Entries.proof_output ->
- (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer
+ private_constants ->
+ exported_private_constant list safe_transformer
(** returns the main constant *)
val add_constant :
diff --git a/library/global.mli b/library/global.mli
index a38fde41a5..b6bd69c17c 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -47,8 +47,8 @@ val push_named_def : (Id.t * Entries.section_def_entry) -> unit
val push_section_context : (Name.t array * Univ.UContext.t) -> unit
val export_private_constants :
- Safe_typing.private_constants Entries.proof_output ->
- Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list
+ Safe_typing.private_constants ->
+ Safe_typing.exported_private_constant list
val add_constant :
Id.t -> Safe_typing.global_declaration -> Constant.t
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 92a2222cfa..cdadde8621 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -2416,6 +2416,36 @@ let nqa =
(fun _ x -> x)
Mc.cnfQ qq_domain_spec dump_qexpr nlinear_prover_R
+let print_lia_profile () =
+ Simplex.(
+ let { number_of_successes
+ ; number_of_failures
+ ; success_pivots
+ ; failure_pivots
+ ; average_pivots
+ ; maximum_pivots } =
+ Simplex.get_profile_info ()
+ in
+ Feedback.msg_notice
+ Pp.(
+ (* successes *)
+ str "number of successes: "
+ ++ int number_of_successes ++ fnl ()
+ (* success pivots *)
+ ++ str "number of success pivots: "
+ ++ int success_pivots ++ fnl ()
+ (* failure *)
+ ++ str "number of failures: "
+ ++ int number_of_failures ++ fnl ()
+ (* failure pivots *)
+ ++ str "number of failure pivots: "
+ ++ int failure_pivots ++ fnl ()
+ (* Other *)
+ ++ str "average number of pivots: "
+ ++ int average_pivots ++ fnl ()
+ ++ str "maximum number of pivots: "
+ ++ int maximum_pivots ++ fnl ()))
+
(* Local Variables: *)
(* coding: utf-8 *)
(* End: *)
diff --git a/plugins/micromega/coq_micromega.mli b/plugins/micromega/coq_micromega.mli
index 37ea560241..bcfc47357f 100644
--- a/plugins/micromega/coq_micromega.mli
+++ b/plugins/micromega/coq_micromega.mli
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-(*val is_ground_tac : EConstr.constr -> unit Proofview.tactic*)
val psatz_Z : int -> unit Proofview.tactic -> unit Proofview.tactic
val psatz_Q : int -> unit Proofview.tactic -> unit Proofview.tactic
val psatz_R : int -> unit Proofview.tactic -> unit Proofview.tactic
@@ -21,6 +20,7 @@ val sos_Q : unit Proofview.tactic -> unit Proofview.tactic
val sos_R : unit Proofview.tactic -> unit Proofview.tactic
val lra_Q : unit Proofview.tactic -> unit Proofview.tactic
val lra_R : unit Proofview.tactic -> unit Proofview.tactic
+val print_lia_profile : unit -> unit
(** {5 Use Micromega independently from tactics. } *)
diff --git a/plugins/micromega/g_micromega.mlg b/plugins/micromega/g_micromega.mlg
index edf8106f30..d0f70bceac 100644
--- a/plugins/micromega/g_micromega.mlg
+++ b/plugins/micromega/g_micromega.mlg
@@ -28,10 +28,6 @@ open Tacarg
DECLARE PLUGIN "micromega_plugin"
-TACTIC EXTEND RED
-| [ "myred" ] -> { Tactics.red_in_concl }
-END
-
TACTIC EXTEND PsatzZ
| [ "psatz_Z" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Z i
(Tacinterp.tactic_of_value ist t))
@@ -87,3 +83,6 @@ TACTIC EXTEND PsatzQ
| [ "psatz_Q" tactic(t) ] -> { (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) }
END
+VERNAC COMMAND EXTEND ShowLiaProfile CLASSIFIED AS QUERY
+| [ "Show" "Lia" "Profile" ] -> { Coq_micromega.print_lia_profile () }
+END
diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml
index ade8143f3c..54976221bc 100644
--- a/plugins/micromega/simplex.ml
+++ b/plugins/micromega/simplex.ml
@@ -18,6 +18,49 @@ type ('a, 'b) sum = Inl of 'a | Inr of 'b
let debug = false
+(** Exploiting profiling information *)
+
+let profile_info = ref []
+let nb_pivot = ref 0
+
+type profile_info =
+ { number_of_successes : int
+ ; number_of_failures : int
+ ; success_pivots : int
+ ; failure_pivots : int
+ ; average_pivots : int
+ ; maximum_pivots : int }
+
+let init_profile =
+ { number_of_successes = 0
+ ; number_of_failures = 0
+ ; success_pivots = 0
+ ; failure_pivots = 0
+ ; average_pivots = 0
+ ; maximum_pivots = 0 }
+
+let get_profile_info () =
+ let update_profile
+ { number_of_successes
+ ; number_of_failures
+ ; success_pivots
+ ; failure_pivots
+ ; average_pivots
+ ; maximum_pivots } (b, i) =
+ { number_of_successes = (number_of_successes + if b then 1 else 0)
+ ; number_of_failures = (number_of_failures + if b then 0 else 1)
+ ; success_pivots = (success_pivots + if b then i else 0)
+ ; failure_pivots = (failure_pivots + if b then 0 else i)
+ ; average_pivots = average_pivots + 1 (* number of proofs *)
+ ; maximum_pivots = max maximum_pivots i }
+ in
+ let p = List.fold_left update_profile init_profile !profile_info in
+ profile_info := [];
+ { p with
+ average_pivots =
+ ( try (p.success_pivots + p.failure_pivots) / p.average_pivots
+ with Division_by_zero -> 0 ) }
+
type iset = unit IMap.t
type tableau = Vect.t IMap.t
@@ -60,10 +103,7 @@ let output_tableau o t =
t
let output_env o t =
- IMap.iter
- (fun k v ->
- Printf.fprintf o "%a : %a\n" LinPoly.pp_var k WithProof.output v)
- t
+ IMap.iter (fun k v -> Printf.fprintf o "%i : %a\n" k WithProof.output v) t
let output_vars o m =
IMap.iter (fun k _ -> Printf.fprintf o "%a " LinPoly.pp_var k) m
@@ -224,6 +264,7 @@ let pivot_with (m : tableau) (v : var) (p : Vect.t) =
IMap.map (fun (r : Vect.t) -> pivot_row r v p) m
let pivot (m : tableau) (r : var) (c : var) =
+ incr nb_pivot;
let row = safe_find "pivot" r m in
let piv = solve_column c r row in
IMap.add c piv (pivot_with (IMap.remove r m) c piv)
@@ -477,8 +518,11 @@ let make_farkas_proof (env : WithProof.t IMap.t) vm v =
try
let x', b = IMap.find x vm in
let n = if b then n else Num.minus_num n in
- WithProof.mult (Vect.cst n) (IMap.find x' env)
- with Not_found -> WithProof.mult (Vect.cst n) (IMap.find x env)
+ let prf = IMap.find x' env in
+ WithProof.mult (Vect.cst n) prf
+ with Not_found ->
+ let prf = IMap.find x env in
+ WithProof.mult (Vect.cst n) prf
end)
WithProof.zero v
@@ -493,21 +537,43 @@ type ('a, 'b) hitkind =
let cut env rmin sol vm (rst : Restricted.t) tbl (x, v) =
let n, r = Vect.decomp_cst v in
- let f = frac_num n in
- if f =/ Int 0 then Forget (* The solution is integral *)
+ let fn = frac_num n in
+ if fn =/ Int 0 then Forget (* The solution is integral *)
else
- (* This is potentially a cut *)
- let t =
- if f </ Int 1 // Int 2 then
- let t' = Int 1 // f in
- if Num.is_integer_num t' then t' -/ Int 1 else Num.floor_num t'
- else Int 1
- in
- let cut_coeff1 v =
+ (* The cut construction is from:
+ Letchford and Lodi. Strengthening Chvatal-Gomory cuts and Gomory fractional cuts.
+
+ We implement the classic Proposition 2 from the "known results"
+ *)
+
+ (* Proposition 3 requires all the variables to be restricted and is
+ therefore not always applicable. *)
+ (* let ccoeff_prop1 v = frac_num v in
+ let ccoeff_prop3 v =
+ (* mixed integer cut *)
let fv = frac_num v in
- if fv <=/ Int 1 -/ f then fv // (Int 1 -/ f) else (Int 1 -/ fv) // f
+ Num.min_num fv (fn */ (Int 1 -/ fv) // (Int 1 -/ fn))
in
- let cut_coeff2 v = frac_num (t */ v) in
+ let ccoeff_prop3 =
+ if Restricted.is_restricted x rst then ("Prop3", ccoeff_prop3)
+ else ("Prop1", ccoeff_prop1)
+ in *)
+ let n0_5 = Int 1 // Int 2 in
+ (* If the fractional part [fn] is small, we construct the t-cut.
+ If the fractional part [fn] is big, we construct the t-cut of the negated row.
+ (This is only a cut if all the fractional variables are restricted.)
+ *)
+ let ccoeff_prop2 =
+ let tmin =
+ if fn </ n0_5 then (* t-cut *)
+ Num.ceiling_num (n0_5 // fn)
+ else
+ (* multiply by -1 & t-cut *)
+ minus_num (Num.ceiling_num (n0_5 // (Int 1 -/ fn)))
+ in
+ ("Prop2", fun v -> frac_num (v */ tmin))
+ in
+ let ccoeff = ccoeff_prop2 in
let cut_vector ccoeff =
Vect.fold
(fun acc x n ->
@@ -516,35 +582,31 @@ let cut env rmin sol vm (rst : Restricted.t) tbl (x, v) =
Vect.null r
in
let lcut =
- List.map
- (fun cv -> Vect.normalise (cut_vector cv))
- [cut_coeff1; cut_coeff2]
+ ( fst ccoeff
+ , make_farkas_proof env vm (Vect.normalise (cut_vector (snd ccoeff))) )
in
- let lcut = List.map (make_farkas_proof env vm) lcut in
- let check_cutting_plane c =
+ let check_cutting_plane (p, c) =
match WithProof.cutting_plane c with
| None ->
if debug then
- Printf.printf "This is not a cutting plane for %a\n%a:" LinPoly.pp_var
- x WithProof.output c;
+ Printf.printf "%s: This is not a cutting plane for %a\n%a:" p
+ LinPoly.pp_var x WithProof.output c;
None
| Some (v, prf) ->
if debug then (
- Printf.printf "This is a cutting plane for %a:" LinPoly.pp_var x;
+ Printf.printf "%s: This is a cutting plane for %a:" p LinPoly.pp_var x;
Printf.printf " %a\n" WithProof.output (v, prf) );
- if snd v = Eq then (* Unsat *) Some (x, (v, prf))
- else
- let vl = Vect.dotproduct (fst v) (Vect.set 0 (Int 1) sol) in
- if eval_op Ge vl (Int 0) then (
- if debug then
- Printf.printf "The cut is feasible %s >= 0 \n"
- (Num.string_of_num vl);
- None )
- else Some (x, (v, prf))
+ Some (x, (v, prf))
in
- match find_some check_cutting_plane lcut with
+ match check_cutting_plane lcut with
| Some r -> Hit r
- | None -> Keep (x, v)
+ | None ->
+ let has_unrestricted =
+ Vect.fold
+ (fun acc v vl -> acc || not (Restricted.is_restricted v rst))
+ false r
+ in
+ if has_unrestricted then Keep (x, v) else Forget
let merge_result_old oldr f x =
match oldr with
@@ -681,12 +743,16 @@ let integer_solver lp =
isolve env None vr res
let integer_solver lp =
+ nb_pivot := 0;
if debug then
Printf.printf "Input integer solver\n%a\n" WithProof.output_sys
(List.map WithProof.of_cstr lp);
match integer_solver lp with
- | None -> None
+ | None ->
+ profile_info := (false, !nb_pivot) :: !profile_info;
+ None
| Some prf ->
+ profile_info := (true, !nb_pivot) :: !profile_info;
if debug then
Printf.fprintf stdout "Proof %a\n" ProofFormat.output_proof prf;
Some prf
diff --git a/plugins/micromega/simplex.mli b/plugins/micromega/simplex.mli
index 19bcce3590..ff672edafd 100644
--- a/plugins/micromega/simplex.mli
+++ b/plugins/micromega/simplex.mli
@@ -9,6 +9,20 @@
(************************************************************************)
open Polynomial
+(** Profiling *)
+
+type profile_info =
+ { number_of_successes : int
+ ; number_of_failures : int
+ ; success_pivots : int
+ ; failure_pivots : int
+ ; average_pivots : int
+ ; maximum_pivots : int }
+
+val get_profile_info : unit -> profile_info
+
+(** Simplex interface *)
+
val optimise : Vect.t -> cstr list -> (Num.num option * Num.num option) option
val find_point : cstr list -> Vect.t option
val find_unsat_certificate : cstr list -> Vect.t option
diff --git a/tactics/declare.ml b/tactics/declare.ml
index c7581fb0e0..ce2f3ec2c5 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -160,6 +160,18 @@ let register_side_effect (c, role) =
| None -> ()
| Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|]
+let get_roles export eff =
+ let map c =
+ let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in
+ (c, role)
+ in
+ List.map map export
+
+let export_side_effects eff =
+ let export = Global.export_private_constants eff.Evd.seff_private in
+ let export = get_roles export eff in
+ List.iter register_side_effect export
+
let record_aux env s_ty s_bo =
let open Environ in
let in_ty = keep_hyps env s_ty in
@@ -278,13 +290,6 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo
opaque_entry_universes = univs;
}
-let get_roles export eff =
- let map c =
- let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in
- (c, role)
- in
- List.map map export
-
let feedback_axiom () = Feedback.(feedback AddedAxiom)
let is_unsafe_typing_flags () =
@@ -293,37 +298,36 @@ let is_unsafe_typing_flags () =
let define_constant ~name cd =
(* Logically define the constant and its subproofs, no libobject tampering *)
- let export, decl, unsafe = match cd with
- | DefinitionEntry de ->
- (* We deal with side effects *)
- if not de.proof_entry_opaque then
- (* This globally defines the side-effects in the environment. *)
- let body, eff = Future.force de.proof_entry_body in
- let body, export = Global.export_private_constants (body, eff.Evd.seff_private) in
- let export = get_roles export eff in
- let de = { de with proof_entry_body = Future.from_val (body, ()) } in
- let cd = Entries.DefinitionEntry (cast_proof_entry de) in
- export, ConstantEntry cd, false
- else
- let map (body, eff) = body, eff.Evd.seff_private in
- let body = Future.chain de.proof_entry_body map in
- let de = { de with proof_entry_body = body } in
- let de = cast_opaque_proof_entry EffectEntry de in
- [], OpaqueEntry de, false
- | ParameterEntry e ->
- [], ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict())
- | PrimitiveEntry e ->
- [], ConstantEntry (Entries.PrimitiveEntry e), false
+ let decl, unsafe = match cd with
+ | DefinitionEntry de ->
+ (* We deal with side effects *)
+ if not de.proof_entry_opaque then
+ let body, eff = Future.force de.proof_entry_body in
+ (* This globally defines the side-effects in the environment
+ and registers their libobjects. *)
+ let () = export_side_effects eff in
+ let de = { de with proof_entry_body = Future.from_val (body, ()) } in
+ let cd = Entries.DefinitionEntry (cast_proof_entry de) in
+ ConstantEntry cd, false
+ else
+ let map (body, eff) = body, eff.Evd.seff_private in
+ let body = Future.chain de.proof_entry_body map in
+ let de = { de with proof_entry_body = body } in
+ let de = cast_opaque_proof_entry EffectEntry de in
+ OpaqueEntry de, false
+ | ParameterEntry e ->
+ ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict())
+ | PrimitiveEntry e ->
+ ConstantEntry (Entries.PrimitiveEntry e), false
in
let kn = Global.add_constant name decl in
if unsafe || is_unsafe_typing_flags() then feedback_axiom();
- kn, export
+ kn
let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
let () = check_exists name in
- let kn, export = define_constant ~name cd in
- (* Register the libobjects attached to the constants and its subproofs *)
- let () = List.iter register_side_effect export in
+ let kn = define_constant ~name cd in
+ (* Register the libobjects attached to the constants *)
let () = register_constant kn kind local in
kn
@@ -377,10 +381,8 @@ let declare_variable ~name ~kind d =
| SectionLocalDef (de) ->
(* The body should already have been forced upstream because it is a
section-local definition, but it's not enforced by typing *)
- let (body, eff) = Future.force de.proof_entry_body in
- let ((body, uctx), export) = Global.export_private_constants (body, eff.Evd.seff_private) in
- let eff = get_roles export eff in
- let () = List.iter register_side_effect eff in
+ let ((body, uctx), eff) = Future.force de.proof_entry_body in
+ let () = export_side_effects eff in
let poly, univs = match de.proof_entry_universes with
| Monomorphic_entry uctx -> false, uctx
| Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
diff --git a/test-suite/bugs/closed/bug_5617.v b/test-suite/bugs/closed/bug_5617.v
new file mode 100644
index 0000000000..c18e79295c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5617.v
@@ -0,0 +1,8 @@
+Set Primitive Projections.
+Record T X := { F : X }.
+
+Fixpoint f (n : nat) : nat :=
+match n with
+| 0 => 0
+| S m => F _ {| F := f |} m
+end.
diff --git a/test-suite/micromega/bug_11436.v b/test-suite/micromega/bug_11436.v
new file mode 100644
index 0000000000..fc6ccbb233
--- /dev/null
+++ b/test-suite/micromega/bug_11436.v
@@ -0,0 +1,19 @@
+Require Import ZArith Lia.
+Local Open Scope Z_scope.
+
+Unset Lia Cache.
+
+Goal forall a q q0 q1 r r0 r1: Z,
+ 0 <= a < 2 ^ 64 ->
+ r1 = 4 * q + r ->
+ 0 <= r < 4 ->
+ a = 4 * q0 + r0 ->
+ 0 <= r0 < 4 ->
+ a + 4 = 2 ^ 64 * q1 + r1 ->
+ 0 <= r1 < 2 ^ 64 ->
+ r = r0.
+Proof.
+ intros.
+ (* subst. *)
+ Time lia.
+Qed.
diff --git a/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v b/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v
new file mode 100644
index 0000000000..a53c160e45
--- /dev/null
+++ b/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v
@@ -0,0 +1,4 @@
+Require Import Lia.
+Goal forall n (B: n >= 0), exists Goal1 Goal2 Goal3,
+ (0 * (Goal1 * Goal2 + Goal1) <> Goal3 * 0 * (Goal1 * S Goal2)).
+Proof. eexists _, _, _. Fail lia. Abort.
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index 9efb81a901..36b4243ef8 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -11,15 +11,14 @@ Open Scope Z_scope.
Lemma Zabs_square : forall x, (Z.abs x)^2 = x^2.
Proof.
- intros ; case (Zabs_dec x) ; intros ; nia.
+ intros ; nia.
Qed.
-Hint Resolve Z.abs_nonneg Zabs_square.
Lemma integer_statement : ~exists n, exists p, n^2 = 2*p^2 /\ n <> 0.
Proof.
intros [n [p [Heq Hnz]]]; pose (n' := Z.abs n); pose (p':=Z.abs p).
assert (facts : 0 <= Z.abs n /\ 0 <= Z.abs p /\ Z.abs n^2=n^2
- /\ Z.abs p^2 = p^2) by auto.
+ /\ Z.abs p^2 = p^2) by auto using Z.abs_nonneg, Zabs_square.
assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by
(destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; nia).
generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear.
@@ -45,10 +44,7 @@ Proof.
intros.
destruct x.
simpl.
- unfold Z.pow_pos.
- simpl.
- rewrite Pos.mul_1_r.
- reflexivity.
+ lia.
Qed.
Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 08:52:06 +0000