From 64e801cce80ac0d3bffcebf414d57785a2c6826f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 30 Aug 2016 09:34:10 +0200 Subject: Setting an unknown option now always a warning. Fixes #4947. Previously, setting an unknown option was an error or a warning, depending on the type of the option. We make it always a warning, for forward compatibility. This was already fixed in 8.6. --- library/goptions.ml | 30 ++++++++++++++---------------- 1 file changed, 14 insertions(+), 16 deletions(-) diff --git a/library/goptions.ml b/library/goptions.ml index 5f6512e117..97da8a1eab 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -304,18 +304,18 @@ let declare_stringopt_option = (* Setting values of options *) let set_option_value locality check_and_cast key v = - let (name, depr, (_,read,write,lwrite,gwrite)) = - try get_option key - with Not_found -> - errorlabstrm "Goptions.set_option_value" - (str "There is no option " ++ str (nickname key) ++ str ".") - in - let write = match locality with - | None -> write - | Some true -> lwrite - | Some false -> gwrite - in - write (check_and_cast v (read ())) + let opt = try Some (get_option key) with Not_found -> None in + match opt with + | None -> + msg_warning + (str "There is no option " ++ str (nickname key) ++ str ".") + | Some (name, depr, (_,read,write,lwrite,gwrite)) -> + let write = match locality with + | None -> write + | Some true -> lwrite + | Some false -> gwrite + in + write (check_and_cast v (read ())) let bad_type_error () = error "Bad type of value for this option." @@ -345,13 +345,11 @@ let check_unset_value v = function let set_int_option_value_gen locality = set_option_value locality check_int_value let set_bool_option_value_gen locality key v = - try set_option_value locality check_bool_value key v - with UserError (_,s) -> msg_warning s + set_option_value locality check_bool_value key v let set_string_option_value_gen locality = set_option_value locality check_string_value let unset_option_value_gen locality key = - try set_option_value locality check_unset_value key () - with UserError (_,s) -> msg_warning s + set_option_value locality check_unset_value key () let set_int_option_value = set_int_option_value_gen None let set_bool_option_value = set_bool_option_value_gen None -- cgit v1.2.3 From 6231f07b2b7b31db93ce9fd4606450e3fa8b747f Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Tue, 30 Aug 2016 11:59:01 +0200 Subject: micromega cache files are now hidden files (cf #4156) csdp.cache -> .csdp.cache lia.cache -> .lia.cache nlia.cache -> .nia.cache --- plugins/micromega/coq_micromega.ml | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index cce0a72805..fdc41eeddc 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1766,7 +1766,7 @@ module Cache = PHashtable(struct let hash = Hashtbl.hash end) -let csdp_cache = "csdp.cache" +let csdp_cache = ".csdp.cache" (** * Build the command to call csdpcert, and launch it. This in turn will call @@ -1960,12 +1960,8 @@ module CacheZ = PHashtable(struct let hash = Hashtbl.hash end) -let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate.lia) -let memo_nlia = CacheZ.memo "nlia.cache" (lift_pexpr_prover Certificate.nlia) - -(*let memo_zlinear_prover = (lift_pexpr_prover Lia.lia)*) -(*let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate.zlinear_prover)*) - +let memo_zlinear_prover = CacheZ.memo ".lia.cache" (lift_pexpr_prover Certificate.lia) +let memo_nlia = CacheZ.memo ".nia.cache" (lift_pexpr_prover Certificate.nlia) let linear_Z = { -- cgit v1.2.3 From 3da141c5dfed50e1b9a4ad5421b4abacdcc23dae Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 30 Aug 2016 14:11:44 +0200 Subject: Fix #4871 - interrupting par:abstract kills coqtop Fix done with Enrico. --- stm/asyncTaskQueue.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 1214fc4da9..613ddb4da5 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -230,10 +230,8 @@ module Make(T : Task) = struct | (Die | TQueue.BeingDestroyed) -> giveback_exec_token (); kill proc; exit () | Sys_error _ | Invalid_argument _ | End_of_file -> - giveback_exec_token (); T.on_task_cancellation_or_expiration_or_slave_death !last_task; - kill proc; - exit () + giveback_exec_token (); kill proc; exit () end module Pool = WorkerPool.Make(Model) -- cgit v1.2.3 From 12268bef28dea57fdbe29dc87d26ef453ad5cfed Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 31 Aug 2016 11:32:28 +0200 Subject: Fix bug #5043: [Admitted] lemmas pick up section variables. We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables. --- stm/lemmas.ml | 18 ++++++++++++++++-- test-suite/bugs/closed/5043.v | 8 ++++++++ theories/Compat/Coq84.v | 4 ++++ 3 files changed, 28 insertions(+), 2 deletions(-) create mode 100644 test-suite/bugs/closed/5043.v diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 1ab695a5f2..40dbe2190b 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -461,6 +461,18 @@ let start_proof_com kind thms hook = (* Saving a proof *) +let keep_admitted_vars = ref true + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "keep section variables in admitted proofs"; + optkey = ["Keep"; "Admitted"; "Variables"]; + optread = (fun () -> !keep_admitted_vars); + optwrite = (fun b -> keep_admitted_vars := b) } + let save_proof ?proof = function | Vernacexpr.Admitted -> let pe = @@ -474,7 +486,8 @@ let save_proof ?proof = function error "Admitted requires an explicit statement"; let typ = Option.get const_entry_type in let ctx = Evd.evar_context_universe_context (fst universes) in - Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes) + let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in + Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes) | None -> let pftree = Pfedit.get_pftreestate () in let id, k, typ = Pfedit.current_proof_statement () in @@ -483,7 +496,8 @@ let save_proof ?proof = function let pproofs, _univs = Proof_global.return_proof ~allow_partial:true () in let sec_vars = - match Pfedit.get_used_variables(), pproofs with + if not !keep_admitted_vars then None + else match Pfedit.get_used_variables(), pproofs with | Some _ as x, _ -> x | None, (pproof, _) :: _ -> let env = Global.env () in diff --git a/test-suite/bugs/closed/5043.v b/test-suite/bugs/closed/5043.v new file mode 100644 index 0000000000..4e6a0f878f --- /dev/null +++ b/test-suite/bugs/closed/5043.v @@ -0,0 +1,8 @@ +Unset Keep Admitted Variables. + +Section a. + Context (x : Type). + Definition foo : Type. + Admitted. +End a. +Check foo : Type. diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index c157c5e85d..4f6118902f 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -72,3 +72,7 @@ Require Coq.Lists.List. Require Coq.Vectors.VectorDef. Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. Notation " [ x ; .. ; y ] " := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope. + +(** In 8.4, the statement of admitted lemmas did not depend on the section + variables. *) +Unset Keep Admitted Variables. -- cgit v1.2.3 From b6c6e953d28d216c6320418885e20605cc69fb92 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 1 Sep 2016 09:16:15 +0200 Subject: Fixing name of internal refine ("simple refine"). --- proofs/proofview.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 57ff777080..483f82113d 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -1105,7 +1105,7 @@ struct let comb = undefined sigma (CList.rev evs) in let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in let open Proof in - InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >> + InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)))) >> Pv.modify (fun ps -> { ps with solution = sigma; comb; }) end -- cgit v1.2.3 From c9c54122d1d9493a965b483939e119d52121d5a6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 1 Sep 2016 10:03:18 +0200 Subject: Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior). (It was reducing also in hypotheses.) --- tactics/tactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 54977dbce7..a66dbd6e88 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4589,7 +4589,7 @@ module New = struct let reduce_after_refine = Proofview.V82.tactic (reduce (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]}) - {onhyps=None; concl_occs=AllOccurrences }) + {onhyps=Some []; concl_occs=AllOccurrences }) let refine ?unsafe c = Proofview.Refine.refine ?unsafe c <*> -- cgit v1.2.3 From af2df1ada04da94a41a400c637788db461a532d9 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 1 Sep 2016 17:40:16 +0200 Subject: Fix test-suite after Frédéric's 6231f07b2. --- test-suite/.csdp.cache | Bin 0 -> 79491 bytes test-suite/csdp.cache | Bin 79491 -> 0 bytes 2 files changed, 0 insertions(+), 0 deletions(-) create mode 100644 test-suite/.csdp.cache delete mode 100644 test-suite/csdp.cache diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache new file mode 100644 index 0000000000..75dd38fde8 Binary files /dev/null and b/test-suite/.csdp.cache differ diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache deleted file mode 100644 index 8e5708cf02..0000000000 Binary files a/test-suite/csdp.cache and /dev/null differ -- cgit v1.2.3