From 26ed8658149d14efa6e4d077c573481281cb610e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 27 Aug 2016 06:48:46 +0200 Subject: Support qualified identifiers in Show Match (bug #5050). --- intf/vernacexpr.mli | 2 +- parsing/g_proofs.ml4 | 2 +- printing/ppvernac.ml | 2 +- toplevel/vernacentries.ml | 11 +++++++---- 4 files changed, 10 insertions(+), 7 deletions(-) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 156e00368d..ed44704df4 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -106,7 +106,7 @@ type showable = | ShowTree | ShowProofNames | ShowIntros of bool - | ShowMatch of lident + | ShowMatch of reference | ShowThesis type comment = diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index b0ff8b64f2..1e3c4b880b 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -88,7 +88,7 @@ GEXTEND Gram | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false) | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true) - | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id) + | IDENT "Show"; IDENT "Match"; id = reference -> VernacShow (ShowMatch id) | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis | IDENT "Guarded" -> VernacCheckGuard (* Hints for Auto and EAuto *) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 0d47b34dfd..40ce28dc0c 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -591,7 +591,7 @@ module Make | ShowTree -> keyword "Show Tree" | ShowProofNames -> keyword "Show Conjectures" | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro") - | ShowMatch id -> keyword "Show Match " ++ pr_lident id + | ShowMatch id -> keyword "Show Match " ++ pr_reference id | ShowThesis -> keyword "Show Thesis" in return (pr_showable s) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index dc098f1f00..33a8609a77 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -120,9 +120,7 @@ let show_intro all = [Not_found] is raised if the given string isn't the qualid of a known inductive type. *) -let make_cases s = - let qualified_name = Libnames.qualid_of_string s in - let glob_ref = Nametab.locate qualified_name in +let make_cases_aux glob_ref = match glob_ref with | Globnames.IndRef i -> let {Declarations.mind_nparams = np} @@ -142,11 +140,16 @@ let make_cases s = carr tarr [] | _ -> raise Not_found +let make_cases s = + let qualified_name = Libnames.qualid_of_string s in + let glob_ref = Nametab.locate qualified_name in + make_cases_aux glob_ref + (** Textual display of a generic "match" template *) let show_match id = let patterns = - try make_cases (Id.to_string (snd id)) + try make_cases_aux (Nametab.global id) with Not_found -> error "Unknown inductive type." in let pr_branch l = -- cgit v1.2.3 From 2b4517cf85432d68e53ac46815309fd8068a40ad Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 28 Aug 2016 19:43:00 +0200 Subject: Fix bug #4764: Syntactic notation externalization breaks. --- interp/notation_ops.ml | 6 ++++-- test-suite/bugs/closed/4764.v | 5 +++++ 2 files changed, 9 insertions(+), 2 deletions(-) create mode 100644 test-suite/bugs/closed/4764.v diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index f3e0682bd7..de56dbe0ab 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1128,13 +1128,15 @@ let match_notation_constr u c (metas,pat) = List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') -> match typ with | NtnTypeConstr -> - ((Id.List.assoc x terms, scl)::terms',termlists',binders') + let term = try Id.List.assoc x terms with Not_found -> raise No_match in + ((term, scl)::terms',termlists',binders') | NtnTypeOnlyBinder -> ((find_binder x, scl)::terms',termlists',binders') | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists',binders') | NtnTypeBinderList -> - (terms',termlists',(Id.List.assoc x binderlists,scl)::binders')) + let bl = try Id.List.assoc x binderlists with Not_found -> raise No_match in + (terms',termlists',(bl, scl)::binders')) metas ([],[],[]) (* Matching cases pattern *) diff --git a/test-suite/bugs/closed/4764.v b/test-suite/bugs/closed/4764.v new file mode 100644 index 0000000000..e545cc1b71 --- /dev/null +++ b/test-suite/bugs/closed/4764.v @@ -0,0 +1,5 @@ +Notation prop_fun x y := (fun (x : Prop) => y). +Definition foo := fun (p : Prop) => p. +Definition bar := fun (_ : Prop) => O. +Print foo. +Print bar. -- cgit v1.2.3 From 812712c0683d03760c10ef7397fb4ff0041c4860 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 28 Aug 2016 19:52:02 +0200 Subject: Fix bug #4750: Change format of inconsistent assumptions message. We now print the file responsible for the incompatibility in require error messages. --- library/library.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/library/library.ml b/library/library.ml index 12090183a7..04b82f2f34 100644 --- a/library/library.ml +++ b/library/library.ml @@ -468,16 +468,18 @@ let rec intern_library (needed, contents) (dir, f) from = pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); - m.library_digests, intern_library_deps (needed, contents) dir m (Some f) + m.library_digests, intern_library_deps (needed, contents) dir m f and intern_library_deps libs dir m from = let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in (dir :: needed, DPMap.add dir m contents ) and intern_mandatory_library caller from libs (dir,d) = - let digest, libs = intern_library libs (dir, None) from in + let digest, libs = intern_library libs (dir, None) (Some from) in if not (Safe_typing.digest_match ~actual:digest ~required:d) then - errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir); + errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ + str " (in file " ++ str from ++ str ") makes inconsistent assumptions \ + over library " ++ pr_dirpath dir); libs let rec_intern_library libs (dir, f) = -- cgit v1.2.3 From f2fb98eabdb2f550c177609ad70ab8ba57821bca Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 29 Aug 2016 10:52:34 +0200 Subject: Send Dependency feedback only if file not already loaded. --- library/library.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/library.ml b/library/library.ml index 04b82f2f34..4bd71888e0 100644 --- a/library/library.ml +++ b/library/library.ml @@ -452,13 +452,13 @@ let intern_from_file f = module DPMap = Map.Make(DirPath) let rec intern_library (needed, contents) (dir, f) from = - Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); (* Look if in the current logical environment *) try (find_library dir).libsum_digests, (needed, contents) with Not_found -> (* Look if already listed and consequently its dependencies too *) try (DPMap.find dir contents).library_digests, (needed, contents) with Not_found -> + Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); (* [dir] is an absolute name which matches [f] which must be in loadpath *) let f = match f with Some f -> f | None -> try_locate_absolute_library dir in let m = intern_from_file f in -- cgit v1.2.3 From aa0ad1713b109da690f9a56358df1f5ba56c65e6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 28 Aug 2016 23:02:23 +0200 Subject: Fix inefficiency in CoqIDE display of tagged text. The helper code in LablGTK is algorithmically slow, so that we rather reimplement it as a small helper function. --- ide/ideutils.ml | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index fe69be9e48..ae668ae8ab 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -46,23 +46,37 @@ let xml_to_string xml = let () = iter (Richpp.repr xml) in Buffer.contents buf -let translate s = s +let insert_with_tags (buf : #GText.buffer_skel) mark tags text = + (** FIXME: LablGTK2 does not export the C insert_with_tags function, so that + it has to reimplement its own helper function. Unluckily, it relies on + a slow algorithm, so that we have to have our own quicker version here. + Alas, it is still much slower than the native version... *) + if CList.is_empty tags then buf#insert text + else + let it = buf#get_iter_at_mark `INSERT in + let () = buf#move_mark (`MARK mark) ~where:it in + let () = buf#insert text in + let start = buf#get_iter_at_mark `INSERT in + let stop = buf#get_iter_at_mark (`MARK mark) in + let iter tag = buf#apply_tag tag start stop in + List.iter iter tags let insert_xml ?(tags = []) (buf : #GText.buffer_skel) msg = let open Xml_datatype in let tag name = - let name = translate name in match GtkText.TagTable.lookup buf#tag_table name with | None -> raise Not_found | Some tag -> new GText.tag tag in + let mark = buf#create_mark buf#start_iter in let rec insert tags = function - | PCData s -> buf#insert ~tags:(List.rev tags) s + | PCData s -> insert_with_tags buf mark tags s | Element (t, _, children) -> let tags = try tag t :: tags with Not_found -> tags in List.iter (fun xml -> insert tags xml) children in - insert tags (Richpp.repr msg) + let () = try insert tags (Richpp.repr msg) with _ -> () in + buf#delete_mark (`MARK mark) let set_location = ref (function s -> failwith "not ready") -- cgit v1.2.3 From 95212aba8ba0ad76e6ee913566040f5c6e2c291d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Aug 2016 12:22:24 +0200 Subject: Fix tagging of notations. We only tag the non-whitespace substrings, rather than the whole terminal token. --- printing/ppconstr.ml | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 935e2d076e..a00e4bab30 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -793,6 +793,22 @@ end let do_not_tag _ x = x +let split_token tag s = + let len = String.length s in + let rec parse_string off i = + if Int.equal i len then + if Int.equal off i then mt () else tag (str (String.sub s off (i - off))) + else if s.[i] == ' ' then + if Int.equal off i then parse_space 1 (succ i) + else tag (str (String.sub s off (i - off))) ++ parse_space 1 (succ i) + else parse_string off (succ i) + and parse_space spc i = + if Int.equal i len then str (String.make spc ' ') + else if s.[i] == ' ' then parse_space (succ spc) (succ i) + else str (String.make spc ' ') ++ parse_string i (succ i) + in + parse_string 0 0 + (** Instantiating Make with tagging functions that only add style information. *) include Make (struct @@ -801,7 +817,7 @@ include Make (struct let tag_evar = tag Tag.evar let tag_type = tag Tag.univ let tag_unparsing = function - | UnpTerminal s -> tag Tag.notation + | UnpTerminal s -> fun _ -> split_token (fun pp -> tag Tag.notation pp) s | _ -> do_not_tag () let tag_constr_expr = do_not_tag let tag_path = tag Tag.path -- cgit v1.2.3 From 85790fe5ffc81aaead5961abac820492e2e2c871 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Aug 2016 14:03:21 +0200 Subject: CoqIDE preserves unknown preferences. This allows a smoother transition between various versions of CoqIDE, by not erasing options which are unknown at the present time. --- ide/preferences.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/ide/preferences.ml b/ide/preferences.ml index 3241a962dc..64327d74f5 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -33,6 +33,7 @@ type obj = { } let preferences : obj Util.String.Map.t ref = ref Util.String.Map.empty +let unknown_preferences : string list Util.String.Map.t ref = ref Util.String.Map.empty class type ['a] repr = object @@ -617,19 +618,19 @@ let save_pref () = then Unix.mkdir (Minilib.coqide_config_home ()) 0o700; let () = try GtkData.AccelMap.save accel_file with _ -> () in let add = Util.String.Map.add in - let (++) x f = f x in let fold key obj accu = add key (obj.get ()) accu in - - (Util.String.Map.fold fold !preferences Util.String.Map.empty) ++ - Config_lexer.print_file pref_file + let prefs = Util.String.Map.fold fold !preferences Util.String.Map.empty in + let prefs = Util.String.Map.fold Util.String.Map.add !unknown_preferences prefs in + Config_lexer.print_file pref_file prefs let load_pref () = let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in let m = Config_lexer.load_file loaded_pref_file in let iter name v = - try (Util.String.Map.find name !preferences).set v - with _ -> () + if Util.String.Map.mem name !preferences then + try (Util.String.Map.find name !preferences).set v with _ -> () + else unknown_preferences := Util.String.Map.add name v !unknown_preferences in Util.String.Map.iter iter m -- cgit v1.2.3 From 58107b74ba65947129aff8203a821d146ecd18ac Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Aug 2016 14:19:42 +0200 Subject: Fix bug #4421: Messages dialog in Coqide resets. --- ide/coqOps.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 50b3f2c0a0..5b6bad3496 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -785,7 +785,6 @@ object(self) method private handle_failure_aux ?(move_insert=false) (safe_id, (loc : (int * int) option), msg) = - messages#clear; messages#push Feedback.Error msg; ignore(self#process_feedback ()); if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ()) -- cgit v1.2.3 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 0d5abcf9e17b4fe0462ffa60d04a321d2707ccf6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 30 Aug 2016 13:42:25 +0200 Subject: Missing .PHONY targets. --- Makefile.dev | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile.dev b/Makefile.dev index 501a7744a1..1f81edc2c9 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -167,7 +167,7 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \ .PHONY: init theories-light noreal .PHONY: logic arith bool narith zarith qarith lists strings sets .PHONY: fsets relations wellfounded reals setoids sorting numbers -.PHONY: msets mmaps compat +.PHONY: msets mmaps compat parith classes program unicode structures vectors ################ ### 4) plugins -- 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 cc6957b0dbb19a4c0ca505650d252d9486088a5f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 30 Aug 2016 16:40:30 +0200 Subject: Fix #4941 - ~/.coqrc file confusing locations --- parsing/cLexer.ml4 | 3 +++ parsing/cLexer.mli | 8 +++++++- toplevel/vernac.ml | 9 ++++++++- 3 files changed, 18 insertions(+), 2 deletions(-) diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 2acccfdf55..bec891f7f1 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -103,6 +103,9 @@ open Error let current_file = ref "" +let get_current_file () = + !current_file + let set_current_file ~fname = current_file := fname diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index d99ba35573..3b4891d9ac 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -17,7 +17,13 @@ type location_table val location_table : unit -> location_table val restore_location_table : location_table -> unit -(** [set_current_file fname] sets the filename in locations emitted by the lexer *) + +(** [get_current_file fname] returns the filename used in locations emitted by + the lexer *) +val get_current_file : unit -> string + +(** [set_current_file fname] sets the filename used in locations emitted by the + lexer *) val set_current_file : fname:string -> unit val check_ident : string -> unit diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 6dba2c51ea..de3d144838 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -81,7 +81,6 @@ let open_file_twice_if verbosely longfname = let in_chan = open_utf8_file_in longfname in let verb_ch = if verbosely then Some (open_utf8_file_in longfname) else None in - CLexer.set_current_file longfname; let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in (in_chan, longfname, (po, verb_ch)) @@ -190,6 +189,8 @@ let rec vernac_com checknav (loc,com) = let fname = CUnix.make_suffix fname ".v" in let f = Loadpath.locate_file fname in let st = save_translator_coqdoc () in + let old_lexer_file = CLexer.get_current_file () in + CLexer.set_current_file f; if !Flags.beautify_file then begin chan_beautify := open_out (f^beautify_suffix); @@ -199,9 +200,11 @@ let rec vernac_com checknav (loc,com) = try Flags.silently (read_vernac_file verbosely) f; restore_translator_coqdoc st; + CLexer.set_current_file old_lexer_file; with reraise -> let reraise = CErrors.push reraise in restore_translator_coqdoc st; + CLexer.set_current_file old_lexer_file; iraise reraise end @@ -271,12 +274,16 @@ let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore () let load_vernac verb file = chan_beautify := if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout; + let old_lexer_file = CLexer.get_current_file () in try + CLexer.set_current_file file; Flags.silently (read_vernac_file verb) file; if !Flags.beautify_file then close_out !chan_beautify; + CLexer.set_current_file old_lexer_file; with any -> let (e, info) = CErrors.push any in if !Flags.beautify_file then close_out !chan_beautify; + CLexer.set_current_file old_lexer_file; iraise (disable_drop e, info) let warn_file_no_extension = -- cgit v1.2.3 From dea5e8a7ecb2120cccd2d2631ddbf892e99bffda Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 30 Aug 2016 17:29:44 +0200 Subject: Emit a warning on Require inside a module. --- library/library.ml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/library/library.ml b/library/library.ml index 4bd71888e0..d44f796a7a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -553,12 +553,20 @@ let in_require : require_obj -> obj = let (f_xml_require, xml_require) = Hook.make ~default:ignore () +let warn_require_in_module = + CWarnings.create ~name:"require-in-module" ~category:"deprecated" + (fun () -> strbrk "Require inside a module is" ++ + strbrk " deprecated and strongly discouraged. " ++ + strbrk "You can Require a module at toplevel " ++ + strbrk "and optionally Import it inside another one.") + let require_library_from_dirpath modrefl export = let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in let modrefl = List.map fst modrefl in if Lib.is_module_or_modtype () then begin + warn_require_in_module (); add_anonymous_leaf (in_require (needed,modrefl,None)); Option.iter (fun exp -> add_anonymous_leaf (in_import_library (modrefl,exp))) -- cgit v1.2.3 From 44ada644ef50563aa52cfcd7717d44bde29e5a20 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 30 Aug 2016 17:37:27 +0200 Subject: Fix bug #3920: eapply masks an hypothesis name. The problem came from the fact that the legacy beta-reduction occurring after a rewrite was wrongly applied to the side-conditions of the rewriting step. We restrict it to the correct goal in this patch. --- ltac/rewrite.ml | 21 ++++++++++++--------- test-suite/bugs/closed/3920.v | 7 +++++++ 2 files changed, 19 insertions(+), 9 deletions(-) create mode 100644 test-suite/bugs/closed/3920.v diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 7acad20d20..8cc50684e2 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1561,6 +1561,10 @@ let newfail n s = let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let open Proofview.Notations in + (** For compatibility *) + let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in + let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in + let beta_hyp id = Tactics.reduct_in_hyp beta_red (id, InHyp) in let treat sigma res = match res with | None -> newfail 0 (str "Nothing to rewrite") @@ -1572,12 +1576,17 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let gls = List.rev (Evd.fold_undefined fold undef []) in match clause, prf with | Some id, Some p -> - let tac = Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in + let tac = Tacticals.New.tclTHENLIST [ + Refine.refine ~unsafe:false { run = fun h -> Sigma.here p h }; + beta_hyp id; + Proofview.Unsafe.tclNEWGOALS gls; + ] in Proofview.Unsafe.tclEVARS undef <*> assert_replacing id newt tac | Some id, None -> Proofview.Unsafe.tclEVARS undef <*> - convert_hyp_no_check (LocalAssum (id, newt)) + convert_hyp_no_check (LocalAssum (id, newt)) <*> + beta_hyp id | None, Some p -> Proofview.Unsafe.tclEVARS undef <*> Proofview.Goal.enter { enter = begin fun gl -> @@ -1592,12 +1601,6 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = Proofview.Unsafe.tclEVARS undef <*> convert_concl_no_check newt DEFAULTcast in - let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in - let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in - let opt_beta = match clause with - | None -> Proofview.tclUNIT () - | Some id -> Tactics.reduct_in_hyp beta_red (id, InHyp) - in Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in @@ -1622,7 +1625,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let sigma = match origsigma with None -> sigma | Some sigma -> sigma in treat sigma res <*> (** For compatibility *) - beta <*> opt_beta <*> Proofview.shelve_unifiable + beta <*> Proofview.shelve_unifiable with | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) -> raise (RewriteFailure (Himsg.explain_pretype_error env evd e)) diff --git a/test-suite/bugs/closed/3920.v b/test-suite/bugs/closed/3920.v new file mode 100644 index 0000000000..a4adb23cc2 --- /dev/null +++ b/test-suite/bugs/closed/3920.v @@ -0,0 +1,7 @@ +Require Import Setoid. +Axiom P : nat -> Prop. +Axiom P_or : forall x y, P (x + y) <-> P x \/ P y. +Lemma foo (H : P 3) : False. +eapply or_introl in H. +erewrite <- P_or in H. +(* Error: No such hypothesis: H *) -- cgit v1.2.3 From 721637c98514a77d05d080f53f226cab3a8da1e7 Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Tue, 30 Aug 2016 17:12:27 +0200 Subject: plugin micromega : nra also handles non-linear rational arithmetic over Q (Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R. --- doc/refman/Micromega.tex | 90 +++++++++++++++++++++----------------- plugins/micromega/Lqa.v | 55 +++++++++++++++++++++++ plugins/micromega/Lra.v | 56 ++++++++++++++++++++++++ plugins/micromega/Psatz.v | 40 +++++++++-------- plugins/micromega/coq_micromega.ml | 20 ++++----- plugins/micromega/g_micromega.ml4 | 10 ++++- plugins/micromega/vo.itarget | 4 +- test-suite/micromega/qexample.v | 17 +++---- test-suite/micromega/rexample.v | 12 ++--- 9 files changed, 218 insertions(+), 86 deletions(-) create mode 100644 plugins/micromega/Lqa.v create mode 100644 plugins/micromega/Lra.v diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index 1efed6ef76..4daf98f87a 100644 --- a/doc/refman/Micromega.tex +++ b/doc/refman/Micromega.tex @@ -4,16 +4,19 @@ \asection{Short description of the tactics} -\tacindex{psatz} \tacindex{lra} +\tacindex{psatz} \tacindex{lra} \tacindex{lia} \tacindex{nia} \tacindex{nra} \label{sec:psatz-hurry} The {\tt Psatz} module ({\tt Require Import Psatz.}) gives access to several tactics for solving arithmetic goals over {\tt Z}, {\tt Q}, and {\tt R}:\footnote{Support for {\tt nat} and {\tt N} is obtained by - pre-processing the goal with the {\tt zify} tactic.} + pre-processing the goal with the {\tt zify} tactic.}. +It also possible to get the tactics for integers by a {\tt Require Import Lia}, rationals {\tt Require Import Lqa} +and reals {\tt Require Import Lra}. \begin{itemize} \item {\tt lia} is a decision procedure for linear integer arithmetic (see Section~\ref{sec:lia}); \item {\tt nia} is an incomplete proof procedure for integer non-linear arithmetic (see Section~\ref{sec:nia}); -\item {\tt lra} is a decision procedure for linear (real or rational) arithmetic goals (see Section~\ref{sec:lra}); +\item {\tt lra} is a decision procedure for linear (real or rational) arithmetic (see Section~\ref{sec:lra}); +\item {\tt nra} is an incomplete proof procedure for non-linear (real or rational) arithmetic (see Section~\ref{sec:nra}); \item {\tt psatz D n} where {\tt D} is {\tt Z} or {\tt Q} or {\tt R}, and {\tt n} is an optional integer limiting the proof search depth is is an incomplete proof procedure for non-linear arithmetic. It is based on @@ -114,36 +117,6 @@ The deductive power of {\tt lra} is the combined deductive power of {\tt ring\_s % There is also an overlap with the {\tt field} tactic {\emph e.g.}, {\tt x = 10 * x / 10} is solved by {\tt lra}. -\asection{{\tt psatz}: a proof procedure for non-linear arithmetic} -\label{sec:psatz} -The {\tt psatz} tactic explores the $\mathit{Cone}$ by increasing degrees -- hence the depth parameter $n$. -In theory, such a proof search is complete -- if the goal is provable the search eventually stops. -Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a -refutation. - -To illustrate the working of the tactic, consider we wish to prove the following Coq goal. -\begin{coq_eval} -Require Import ZArith Psatz. -Open Scope Z_scope. -\end{coq_eval} -\begin{coq_example*} -Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. -\end{coq_example*} -\begin{coq_eval} -intro x; psatz Z 2. -\end{coq_eval} -Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the -cone expression $2 \times (\mathbf{x-1}) + (\mathbf{x-1}) \times -(\mathbf{x-1}) + \mathbf{-x^2}$ (polynomial hypotheses are printed in -bold). By construction, this expression belongs to $\mathit{Cone}(\{-x^2, -x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By -Theorem~\ref{thm:psatz}, the goal is valid. -% - -%% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a -%% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$. -%% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$. -% \asection{{\tt lia}: a tactic for linear integer arithmetic} \tacindex{lia} @@ -219,22 +192,61 @@ Our current oracle tries to find an expression $e$ with a small range $[c_1,c_2] We generate $c_2 - c_1$ subgoals which contexts are enriched with an equation $e = i$ for $i \in [c_1,c_2]$ and recursively search for a proof. -\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic} -\tacindex{nia} -\label{sec:nia} -The {\tt nia} tactic is an {\emph experimental} proof procedure for non-linear integer arithmetic. + +\asection{{\tt nra}: a proof procedure for non-linear arithmetic} +\tacindex{nra} +\label{sec:nra} +The {\tt nra} tactic is an {\emph experimental} proof procedure for non-linear arithmetic. % The tactic performs a limited amount of non-linear reasoning before running the -linear prover of {\tt lia}. +linear prover of {\tt lra}. This pre-processing does the following: \begin{itemize} \item If the context contains an arithmetic expression of the form $e[x^2]$ where $x$ is a monomial, the context is enriched with $x^2\ge 0$; \item For all pairs of hypotheses $e_1\ge 0$, $e_2 \ge 0$, the context is enriched with $e_1 \times e_2 \ge 0$. \end{itemize} -After pre-processing, the linear prover of {\tt lia} searches for a proof +After this pre-processing, the linear prover of {\tt lra} searches for a proof by abstracting monomials by variables. +\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic} +\tacindex{nia} +\label{sec:nia} +The {\tt nia} tactic is a proof procedure for non-linear integer arithmetic. +% +It performs a pre-processing similar to {\tt nra}. The obtained goal is solved using the linear integer prover {\tt lia}. + +\asection{{\tt psatz}: a proof procedure for non-linear arithmetic} +\label{sec:psatz} +The {\tt psatz} tactic explores the $\mathit{Cone}$ by increasing degrees -- hence the depth parameter $n$. +In theory, such a proof search is complete -- if the goal is provable the search eventually stops. +Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a +refutation. + +To illustrate the working of the tactic, consider we wish to prove the following Coq goal. +\begin{coq_eval} +Require Import ZArith Psatz. +Open Scope Z_scope. +\end{coq_eval} +\begin{coq_example*} +Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. +\end{coq_example*} +\begin{coq_eval} +intro x; psatz Z 2. +\end{coq_eval} +Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the +cone expression $2 \times (\mathbf{x-1}) + (\mathbf{x-1}) \times +(\mathbf{x-1}) + \mathbf{-x^2}$ (polynomial hypotheses are printed in +bold). By construction, this expression belongs to $\mathit{Cone}(\{-x^2, +x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By +Theorem~\ref{thm:psatz}, the goal is valid. +% + +%% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a +%% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$. +%% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$. +% + %%% Local Variables: diff --git a/plugins/micromega/Lqa.v b/plugins/micromega/Lqa.v new file mode 100644 index 0000000000..0055600a08 --- /dev/null +++ b/plugins/micromega/Lqa.v @@ -0,0 +1,55 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + (sos_Q || psatz_Q d) ; + (* If csdp is not installed, the previous step might not produce any + progress: the rest of the tactical will then fail. Hence the 'try'. *) + try (abstract(intros __wit __varmap __ff ; + change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; + apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) + | _ => fail "Unsupported domain" + end in tac. + +Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n. +Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1). + + + + +(* Local Variables: *) +(* coding: utf-8 *) +(* End: *) diff --git a/plugins/micromega/Lra.v b/plugins/micromega/Lra.v new file mode 100644 index 0000000000..7ffe1e4ed0 --- /dev/null +++ b/plugins/micromega/Lra.v @@ -0,0 +1,56 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + (sos_R || psatz_R d) ; + (* If csdp is not installed, the previous step might not produce any + progress: the rest of the tactical will then fail. Hence the 'try'. *) + try (abstract(intros __wit __varmap __ff ; + change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; + apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) + | _ => fail "Unsupported domain" + end in tac. + +Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n. +Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1). + + +(* Local Variables: *) +(* coding: utf-8 *) +(* End: *) diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index fafd8a5f21..b1f242f58a 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -8,7 +8,7 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) -(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* Frédéric Besson (Irisa/Inria) 2006-2016 *) (* *) (************************************************************************) @@ -75,35 +75,39 @@ Ltac psatzl dom := let tac := lazymatch dom with | Z => lia | Q => - psatzl_Q ; - (* If csdp is not installed, the previous step might not produce any - progress: the rest of the tactical will then fail. Hence the 'try'. *) - try (abstract(intros __wit __varmap __ff ; - change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; - apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) + lra_Q ; + (abstract(intros __wit __varmap __ff ; + change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; + apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) | R => unfold Rdiv in * ; - psatzl_R ; - (* If csdp is not installed, the previous step might not produce any - progress: the rest of the tactical will then fail. Hence the 'try'. *) - try abstract((intros __wit __varmap __ff ; - change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; - apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) - | _ => fail "Unsupported domain" + lra_R ; + (abstract((intros __wit __varmap __ff ; + change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; + apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))) +| _ => fail "Unsupported domain" end in tac. Ltac lra := first [ psatzl R | psatzl Q ]. -Ltac nra := +Ltac nra_R := unfold Rdiv in * ; xnra ; abstract (intros __wit __varmap __ff ; - change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; - apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity). - + change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; + apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity). + +Ltac nra_Q := + xnqa ; + (abstract(intros __wit __varmap __ff ; + change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; + apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))). + +Ltac nra := + first [ nra_R | nra_Q ]. (* Local Variables: *) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index b8e5e66cab..edcb00b90b 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -2100,11 +2100,7 @@ let tauto_lia ff = * solvers *) -let psatzl_Z = - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec - [ linear_Z ] - -let psatzl_Q = +let lra_Q = micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec [ linear_prover_Q ] @@ -2112,7 +2108,7 @@ let psatz_Q i = micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] -let psatzl_R = +let lra_R = micromega_genr [ linear_prover_R ] let psatz_R i = @@ -2136,21 +2132,21 @@ let sos_R = micromega_genr [ non_linear_prover_R "pure_sos" None ] -let xlia = - try - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec +let xlia = micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec [ linear_Z ] - with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise let xnlia = - try micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec [ nlinear_Z ] - with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise let nra = micromega_genr [ nlinear_prover_R ] +let nqa = + micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec + [ nlinear_prover_R ] + + (* Local Variables: *) (* coding: utf-8 *) diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index e6b5cc60d4..974dcee870 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -37,6 +37,12 @@ TACTIC EXTEND NRA [ "xnra" ] -> [ (Coq_micromega.nra)] END +TACTIC EXTEND NQA +[ "xnqa" ] -> [ (Coq_micromega.nqa)] +END + + + TACTIC EXTEND Sos_Z | [ "sos_Z" ] -> [ (Coq_micromega.sos_Z) ] END @@ -50,11 +56,11 @@ TACTIC EXTEND Sos_R END TACTIC EXTEND LRA_Q -[ "psatzl_Q" ] -> [ (Coq_micromega.psatzl_Q) ] +[ "lra_Q" ] -> [ (Coq_micromega.lra_Q) ] END TACTIC EXTEND LRA_R -[ "psatzl_R" ] -> [ (Coq_micromega.psatzl_R) ] +[ "lra_R" ] -> [ (Coq_micromega.lra_R) ] END TACTIC EXTEND PsatzR diff --git a/plugins/micromega/vo.itarget b/plugins/micromega/vo.itarget index bf6a1a7db2..cb4b2b8a55 100644 --- a/plugins/micromega/vo.itarget +++ b/plugins/micromega/vo.itarget @@ -10,4 +10,6 @@ Tauto.vo VarMap.vo ZCoeff.vo ZMicromega.vo -Lia.vo \ No newline at end of file +Lia.vo +Lqa.vo +Lra.vo \ No newline at end of file diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v index 47e6005b94..d001e8f7fc 100644 --- a/test-suite/micromega/qexample.v +++ b/test-suite/micromega/qexample.v @@ -6,32 +6,29 @@ (* *) (************************************************************************) -Require Import Psatz. +Require Import Lqa. Require Import QArith. Lemma plus_minus : forall x y, 0 == x + y -> 0 == x -y -> 0 == x /\ 0 == y. Proof. intros. - psatzl Q. + lra. Qed. - - - (* Other (simple) examples *) Open Scope Q_scope. Lemma binomial : forall x y:Q, ((x+y)^2 == x^2 + (2 # 1) *x*y + y^2). Proof. intros. - psatzl Q. + lra. Qed. Lemma hol_light19 : forall m n, (2 # 1) * m + n == (n + m) + m. Proof. - intros ; psatzl Q. + intros ; lra. Qed. Open Scope Z_scope. Open Scope Q_scope. @@ -60,7 +57,11 @@ Lemma vcgen_25 : forall (( 1# 1) == (-2 # 1) * i + it). Proof. intros. - psatzl Q. + lra. +Qed. + +Goal forall x : Q, x * x >= 0. + intro; nra. Qed. Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v index 2eed7e951d..89c08c7704 100644 --- a/test-suite/micromega/rexample.v +++ b/test-suite/micromega/rexample.v @@ -6,7 +6,7 @@ (* *) (************************************************************************) -Require Import Psatz. +Require Import Lra. Require Import Reals. Open Scope R_scope. @@ -15,7 +15,7 @@ Lemma yplus_minus : forall x y, 0 = x + y -> 0 = x -y -> 0 = x /\ 0 = y. Proof. intros. - psatzl R. + lra. Qed. (* Other (simple) examples *) @@ -23,13 +23,13 @@ Qed. Lemma binomial : forall x y, ((x+y)^2 = x^2 + 2 *x*y + y^2). Proof. intros. - psatzl R. + lra. Qed. Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m. Proof. - intros ; psatzl R. + intros ; lra. Qed. @@ -57,7 +57,7 @@ Lemma vcgen_25 : forall (( 1 ) = (-2 ) * i + it). Proof. intros. - psatzl R. + lra. Qed. Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. @@ -72,5 +72,5 @@ Proof. Qed. Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z). -intros; split_Rabs; psatzl R. +intros; split_Rabs; lra. Qed. \ No newline at end of file -- cgit v1.2.3 From 4582ed1c8f0620941a3c296941b1dc808c95d7fe Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 30 Aug 2016 18:47:45 +0200 Subject: Fix bug #4893: not_evar: unexpected failure in 8.5pl1. --- ltac/extratactics.ml4 | 4 +++- tactics/class_tactics.ml | 8 +++++--- test-suite/bugs/closed/4893.v | 4 ++++ 3 files changed, 12 insertions(+), 4 deletions(-) create mode 100644 test-suite/bugs/closed/4893.v diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index be47293fcd..e50b0520bc 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -816,9 +816,11 @@ END TACTIC EXTEND is_evar | [ "is_evar" constr(x) ] -> - [ match kind_of_term x with + [ Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma -> + match Evarutil.kind_of_term_upto sigma x with | Evar _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar") + end ] END diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 6e01a676a2..8d6c085e63 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1500,9 +1500,11 @@ let head_of_constr h c = let c = head_of_constr c in letin_tac None (Name h) c None Locusops.allHyps -let not_evar c = match kind_of_term c with -| Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar") -| _ -> Proofview.tclUNIT () +let not_evar c = + Proofview.tclEVARMAP >>= fun sigma -> + match Evarutil.kind_of_term_upto sigma c with + | Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar") + | _ -> Proofview.tclUNIT () let is_ground c gl = if Evarutil.is_ground_term (project gl) c then tclIDTAC gl diff --git a/test-suite/bugs/closed/4893.v b/test-suite/bugs/closed/4893.v new file mode 100644 index 0000000000..9a35bcf954 --- /dev/null +++ b/test-suite/bugs/closed/4893.v @@ -0,0 +1,4 @@ +Goal True. +evar (P: Prop). +assert (H : P); [|subst P]; [exact I|]. +let T := type of H in not_evar T. -- cgit v1.2.3 From 68ee3958437b98291d69709b9c2a730abf7f7f96 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 30 Aug 2016 19:01:17 +0200 Subject: Fixing output test-suite after warning for inner Requires. --- test-suite/output/PatternsInBinders.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index b5c91e347b..fff86d6fae 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -1,3 +1,5 @@ +Require Coq.Unicode.Utf8. + (** The purpose of this file is to test printing of the destructive patterns used in binders ([fun] and [forall]). *) @@ -37,7 +39,7 @@ End WithParameters. (** Some test involving unicode notations. *) Module WithUnicode. - Require Import Coq.Unicode.Utf8. + Import Coq.Unicode.Utf8. Check λ '((x,y) : A*B), (y,x). Check ∀ '(x,y), swap (x,y) = (y,x). -- cgit v1.2.3 From 985e83e60b6665d17b81830aea4fce3384fe2b5a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 30 Aug 2016 20:32:13 +0200 Subject: Fix bug #5051: Large outputs are garbled. Instead of relying on the current position of the cursor, we rather use a dedicated mark in the message view. --- ide/ideutils.ml | 22 +++++++++++----------- ide/ideutils.mli | 2 +- ide/wg_MessageView.ml | 9 ++++++--- 3 files changed, 18 insertions(+), 15 deletions(-) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index ae668ae8ab..06a1327320 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -46,37 +46,37 @@ let xml_to_string xml = let () = iter (Richpp.repr xml) in Buffer.contents buf -let insert_with_tags (buf : #GText.buffer_skel) mark tags text = +let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text = (** FIXME: LablGTK2 does not export the C insert_with_tags function, so that it has to reimplement its own helper function. Unluckily, it relies on a slow algorithm, so that we have to have our own quicker version here. Alas, it is still much slower than the native version... *) - if CList.is_empty tags then buf#insert text + if CList.is_empty tags then buf#insert ~iter:(buf#get_iter_at_mark mark) text else - let it = buf#get_iter_at_mark `INSERT in - let () = buf#move_mark (`MARK mark) ~where:it in - let () = buf#insert text in - let start = buf#get_iter_at_mark `INSERT in - let stop = buf#get_iter_at_mark (`MARK mark) in + let it = buf#get_iter_at_mark mark in + let () = buf#move_mark rmark ~where:it in + let () = buf#insert ~iter:(buf#get_iter_at_mark mark) text in + let start = buf#get_iter_at_mark mark in + let stop = buf#get_iter_at_mark rmark in let iter tag = buf#apply_tag tag start stop in List.iter iter tags -let insert_xml ?(tags = []) (buf : #GText.buffer_skel) msg = +let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg = let open Xml_datatype in let tag name = match GtkText.TagTable.lookup buf#tag_table name with | None -> raise Not_found | Some tag -> new GText.tag tag in - let mark = buf#create_mark buf#start_iter in + let rmark = `MARK (buf#create_mark buf#start_iter) in let rec insert tags = function - | PCData s -> insert_with_tags buf mark tags s + | PCData s -> insert_with_tags buf mark rmark tags s | Element (t, _, children) -> let tags = try tag t :: tags with Not_found -> tags in List.iter (fun xml -> insert tags xml) children in let () = try insert tags (Richpp.repr msg) with _ -> () in - buf#delete_mark (`MARK mark) + buf#delete_mark rmark let set_location = ref (function s -> failwith "not ready") diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 491e8e823d..e32a4d9e38 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -54,7 +54,7 @@ val flash_info : ?delay:int -> string -> unit val xml_to_string : Richpp.richpp -> string -val insert_xml : ?tags:GText.tag list -> +val insert_xml : ?mark:GText.mark -> ?tags:GText.tag list -> #GText.buffer_skel -> Richpp.richpp -> unit val set_location : (string -> unit) ref diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 758f383d6d..0330b8eff1 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -43,6 +43,7 @@ let message_view () : message_view = ~tag_table:Tags.Message.table () in let text_buffer = new GText.buffer buffer#as_buffer in + let mark = buffer#create_mark ~left_gravity:false buffer#start_iter in let box = GPack.vbox () in let scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(box#pack ~expand:true) () in @@ -69,7 +70,8 @@ let message_view () : message_view = new message_view_signals_impl box#as_widget push method clear = - buffer#set_text "" + buffer#set_text ""; + buffer#move_mark (`MARK mark) ~where:buffer#start_iter method push level msg = let tags = match level with @@ -83,8 +85,9 @@ let message_view () : message_view = | Xml_datatype.Element (_, _, children) -> List.exists non_empty children in if non_empty (Richpp.repr msg) then begin - Ideutils.insert_xml buffer ~tags msg; - buffer#insert (*~tags*) "\n"; + let mark = `MARK mark in + Ideutils.insert_xml ~mark buffer ~tags msg; + buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n"; push#call (level, msg) end -- 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 7d4b8108bc8fa6951e605cb9b42580ff6f8e583f Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Wed, 31 Aug 2016 19:12:15 +0200 Subject: Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'. If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative. --- plugins/micromega/Lia.v | 32 +++++++++--------- plugins/micromega/Lqa.v | 27 ++++++++------- plugins/micromega/Lra.v | 27 ++++++++------- plugins/micromega/Psatz.v | 73 +++++++++-------------------------------- test-suite/micromega/zomicron.v | 11 ++++++- 5 files changed, 67 insertions(+), 103 deletions(-) diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v index 52bf5ed3df..6974f8d998 100644 --- a/plugins/micromega/Lia.v +++ b/plugins/micromega/Lia.v @@ -8,7 +8,7 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) -(* Frédéric Besson (Irisa/Inria) 2013 *) +(* Frédéric Besson (Irisa/Inria) 2013-2016 *) (* *) (************************************************************************) @@ -19,24 +19,24 @@ Require Import VarMap. Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". + Ltac preprocess := zify ; unfold Z.succ in * ; unfold Z.pred in *. -Ltac lia := - preprocess; - xlia ; - abstract ( - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)). - -Ltac nia := - preprocess; - xnlia ; - abstract ( - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)). +Ltac zchange := + intros __wit __varmap __ff ; + change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; + apply (ZTautoChecker_sound __ff __wit). + +Ltac zchecker_no_abstract := zchange ; vm_compute ; reflexivity. + +Ltac zchecker_abstract := abstract (zchange ; vm_cast_no_check (eq_refl true)). + +Ltac zchecker := zchecker_abstract || zchecker_no_abstract . + +Ltac lia := preprocess; xlia ; zchecker. + +Ltac nia := preprocess; xnlia ; zchecker. (* Local Variables: *) diff --git a/plugins/micromega/Lqa.v b/plugins/micromega/Lqa.v index 0055600a08..e3414b8497 100644 --- a/plugins/micromega/Lqa.v +++ b/plugins/micromega/Lqa.v @@ -19,18 +19,21 @@ Require Import VarMap. Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". +Ltac rchange := + intros __wit __varmap __ff ; + change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; + apply (QTautoChecker_sound __ff __wit). + +Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity. +Ltac rchecker_abstract := abstract (rchange ; vm_cast_no_check (eq_refl true)). + +Ltac rchecker := (rchecker_abstract || rchecker_no_abstract). + (** Here, lra stands for linear rational arithmetic *) -Ltac lra := lra_Q ; - (abstract(intros __wit __varmap __ff ; - change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; - apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))). +Ltac lra := lra_Q ; rchecker. (** Here, nra stands for non-linear rational arithmetic *) -Ltac nra := - xnqa ; - (abstract(intros __wit __varmap __ff ; - change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; - apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))). +Ltac nra := xnqa ; rchecker. Ltac xpsatz dom d := let tac := lazymatch dom with @@ -38,9 +41,7 @@ Ltac xpsatz dom d := (sos_Q || psatz_Q d) ; (* If csdp is not installed, the previous step might not produce any progress: the rest of the tactical will then fail. Hence the 'try'. *) - try (abstract(intros __wit __varmap __ff ; - change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; - apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) + try rchecker | _ => fail "Unsupported domain" end in tac. @@ -48,8 +49,6 @@ Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n. Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1). - - (* Local Variables: *) (* coding: utf-8 *) (* End: *) diff --git a/plugins/micromega/Lra.v b/plugins/micromega/Lra.v index 7ffe1e4ed0..4d9cf22dd5 100644 --- a/plugins/micromega/Lra.v +++ b/plugins/micromega/Lra.v @@ -20,20 +20,21 @@ Require Import VarMap. Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". +Ltac rchange := + intros __wit __varmap __ff ; + change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; + apply (RTautoChecker_sound __ff __wit). + +Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity. +Ltac rchecker_abstract := abstract (rchange ; vm_cast_no_check (eq_refl true)). + +Ltac rchecker := rchecker_abstract || rchecker_no_abstract. + (** Here, lra stands for linear real arithmetic *) -Ltac lra := - unfold Rdiv in * ; - lra_R ; - (abstract((intros __wit __varmap __ff ; - change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; - apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))). +Ltac lra := unfold Rdiv in * ; lra_R ; rchecker. (** Here, nra stands for non-linear real arithmetic *) -Ltac nra := - xnra ; - (abstract((intros __wit __varmap __ff ; - change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; - apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))). +Ltac nra := unfold Rdiv in * ; xnra ; rchecker. Ltac xpsatz dom d := let tac := lazymatch dom with @@ -41,9 +42,7 @@ Ltac xpsatz dom d := (sos_R || psatz_R d) ; (* If csdp is not installed, the previous step might not produce any progress: the rest of the tactical will then fail. Hence the 'try'. *) - try (abstract(intros __wit __varmap __ff ; - change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; - apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) + try rchecker | _ => fail "Unsupported domain" end in tac. diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index b1f242f58a..c81c025a55 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -21,50 +21,30 @@ Require Import Rdefinitions. Require Import RingMicromega. Require Import VarMap. Require Coq.micromega.Tauto. -Declare ML Module "micromega_plugin". +Require Lia. +Require Lra. +Require Lqa. -Ltac preprocess := - zify ; unfold Z.succ in * ; unfold Z.pred in *. +Declare ML Module "micromega_plugin". -Ltac lia := - preprocess; - xlia ; - abstract ( - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)). +Ltac lia := Lia.lia. -Ltac nia := - preprocess; - xnlia ; - abstract ( - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)). +Ltac nia := Lia.nia. Ltac xpsatz dom d := let tac := lazymatch dom with | Z => - (sos_Z || psatz_Z d) ; - abstract( - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)) + (sos_Z || psatz_Z d) ; Lia.zchecker | R => (sos_R || psatz_R d) ; (* If csdp is not installed, the previous step might not produce any progress: the rest of the tactical will then fail. Hence the 'try'. *) - try (abstract(intros __wit __varmap __ff ; - change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; - apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) - | Q => - (sos_Q || psatz_Q d) ; + try Lra.rchecker + | Q => (sos_Q || psatz_Q d) ; (* If csdp is not installed, the previous step might not produce any progress: the rest of the tactical will then fail. Hence the 'try'. *) - try (abstract(intros __wit __varmap __ff ; - change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; - apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) + try Lqa.rchecker | _ => fail "Unsupported domain" end in tac. @@ -73,41 +53,18 @@ Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1). Ltac psatzl dom := let tac := lazymatch dom with - | Z => lia - | Q => - lra_Q ; - (abstract(intros __wit __varmap __ff ; - change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; - apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) - | R => - unfold Rdiv in * ; - lra_R ; - (abstract((intros __wit __varmap __ff ; - change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; - apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))) -| _ => fail "Unsupported domain" + | Z => Lia.lia + | Q => Lqa.lra + | R => Lra.lra + | _ => fail "Unsupported domain" end in tac. Ltac lra := first [ psatzl R | psatzl Q ]. -Ltac nra_R := - unfold Rdiv in * ; - xnra ; - abstract - (intros __wit __varmap __ff ; - change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; - apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity). - -Ltac nra_Q := - xnqa ; - (abstract(intros __wit __varmap __ff ; - change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; - apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))). - Ltac nra := - first [ nra_R | nra_Q ]. + first [ Lra.nra | Lqa.nra ]. (* Local Variables: *) diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v index 0ec1dbfbcd..1f148becc9 100644 --- a/test-suite/micromega/zomicron.v +++ b/test-suite/micromega/zomicron.v @@ -33,4 +33,13 @@ Lemma compact_proof : forall z, Proof. intros. lia. -Qed. \ No newline at end of file +Qed. + +Lemma dummy_ex : exists (x:Z), x = x. +Proof. + eexists. + lia. + Unshelve. + exact Z0. +Qed. + \ No newline at end of file -- 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 18046e2525300b990db4c8817f1cc02dcab97445 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 1 Sep 2016 09:59:20 +0200 Subject: Moving log of "TacReduce"/"reduce" to Tactics.reduce so that internal calls are logged too. Using appropriate printer for reparsability of the output. --- ltac/tacinterp.ml | 3 --- tactics/tactics.ml | 7 +++++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 397cd988da..83d67c8e32 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1822,13 +1822,10 @@ and interp_atomic ist tac : unit Proofview.tactic = (* Conversion *) | TacReduce (r,cl) -> - (* spiwack: until the tactic is in the monad *) - Proofview.Trace.name_tactic (fun () -> Pp.str"") begin Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in Sigma.Unsafe.of_pair (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl), sigma) end } - end | TacChange (None,c,cl) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"") begin diff --git a/tactics/tactics.ml b/tactics/tactics.ml index acc0fa1ca7..c9cec828c1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -869,14 +869,17 @@ let reduction_clause redexp cl = (None, bind_red_expr_occurrences occs nbcl redexp)) cl let reduce redexp cl = + let trace () = Pp.(hov 2 (Pptactic.pr_atomic_tactic (Global.env()) (TacReduce (redexp,cl)))) in + Proofview.Trace.name_tactic trace begin Proofview.Goal.enter { enter = begin fun gl -> - let cl = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in - let redexps = reduction_clause redexp cl in + let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in + let redexps = reduction_clause redexp cl' in let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in Tacticals.New.tclMAP (fun (where,redexp) -> e_reduct_option ~check (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps end } + end (* Unfolding occurrences of a constant *) -- 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 04f3aea9afa9fc4b7fa5a50be21b992ba9018dbc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 30 Aug 2016 13:39:06 +0200 Subject: Short documentation, filling TODO's in evd.mli. --- engine/evd.mli | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/engine/evd.mli b/engine/evd.mli index 9424145113..b47b389d1b 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -98,11 +98,12 @@ type evar_info = { (** Optional content of the evar. *) evar_filter : Filter.t; (** Boolean mask over {!evar_hyps}. Should have the same length. - TODO: document me more. *) + When filtered out, the corresponding variable is not allowed to occur + in the solution *) evar_source : Evar_kinds.t located; (** Information about the evar. *) evar_candidates : constr list option; - (** TODO: document this *) + (** List of possible solutions when known that it is a finite list *) evar_extra : Store.t (** Extra store, used for clever hacks. *) } -- cgit v1.2.3 From 5776f7d2b4753b89efa095a0f6774dac702fdfbd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 1 Sep 2016 11:16:09 +0200 Subject: Notation_ops.subst_glob_vars: substituting also in evar kind for consistency of the use of names. --- interp/notation_ops.ml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index de56dbe0ab..fcb4a345e2 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -124,6 +124,14 @@ let rec cases_pattern_fold_map loc g e = function let e',patl' = List.fold_map (cases_pattern_fold_map loc g) e patl in e', PatCstr (loc,cstr,patl',na') +let subst_binder_type_vars l = function + | Evar_kinds.BinderType (Name id) as e -> + let id = + try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id + with Not_found -> id in + Evar_kinds.BinderType (Name id) + | e -> e + let rec subst_glob_vars l = function | GVar (_,id) as r -> (try Id.List.assoc id l with Not_found -> r) | GProd (loc,Name id,bk,t,c) -> @@ -136,6 +144,7 @@ let rec subst_glob_vars l = function try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id with Not_found -> id in GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c) + | GHole (loc,x,naming,arg) -> GHole (loc,subst_binder_type_vars l x,naming,arg) | r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *) let ldots_var = Id.of_string ".." -- cgit v1.2.3 From 5ea872c80cc8b9d2845629cc75369f061e3bad05 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 1 Sep 2016 14:22:13 +0200 Subject: More efficient data structure to check if a native file is loaded. Spotted by PMP. --- kernel/nativecode.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index e2f43b93ee..87302dcf5a 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1930,13 +1930,15 @@ let compile_constant env sigma prefix ~interactive con cb = arg|]))):: [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix -let loaded_native_files = ref ([] : string list) +module StringOrd = struct type t = string let compare = String.compare end +module StringSet = Set.Make(StringOrd) -let is_loaded_native_file s = String.List.mem s !loaded_native_files +let loaded_native_files = ref StringSet.empty + +let is_loaded_native_file s = StringSet.mem s !loaded_native_files let register_native_file s = - if not (is_loaded_native_file s) then - loaded_native_files := s :: !loaded_native_files + loaded_native_files := StringSet.add s !loaded_native_files let is_code_loaded ~interactive name = match !name with -- cgit v1.2.3 From 1ae74bfd16f00bea0de14299cace8b638f768a70 Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Thu, 1 Sep 2016 16:21:11 +0200 Subject: Fixed Bug #5003 : more careful generalisation of dependent terms. --- plugins/micromega/coq_micromega.ml | 35 ++++++++++++++++++++++++++++++++--- 1 file changed, 32 insertions(+), 3 deletions(-) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index edcb00b90b..42ea8c4592 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1437,7 +1437,36 @@ let rcst_domain_spec = lazy { open Proofview.Notations - +(** Naive topological sort of constr according to the subterm-ordering *) + +(* An element is minimal x is minimal w.r.t y if + x <= y or (x and y are incomparable) *) + +let is_min le x y = + if le x y then true + else if le y x then false else true + +let is_minimal le l c = List.for_all (is_min le c) l + +let find_rem p l = + let rec xfind_rem acc l = + match l with + | [] -> (None, acc) + | x :: l -> if p x then (Some x, acc @ l) + else xfind_rem (x::acc) l in + xfind_rem [] l + +let find_minimal le l = find_rem (is_minimal le l) l + +let rec mk_topo_order le l = + match find_minimal le l with + | (None , _) -> [] + | (Some v,l') -> v :: (mk_topo_order le l') + + +let topo_sort_constr l = mk_topo_order Termops.dependent l + + (** * Instanciate the current Coq goal with a Micromega formula, a varmap, and a * witness. @@ -1464,7 +1493,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* ] (Tacmach.pf_concl gl)) ; - Tactics.generalize env ; + Tactics.generalize (topo_sort_constr env) ; Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] end } @@ -1774,7 +1803,7 @@ let micromega_order_changer cert env ff = ("__wit", cert, cert_typ) ] (Tacmach.pf_concl gl))); - Tactics.generalize env ; + Tactics.generalize (topo_sort_constr env) ; Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] end } -- 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