From b1656fe62adb0bbbee4081b07eb42941b1c5696e Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 15:41:23 -0500 Subject: Correct spelling errors --- debian/coq.lintian-overrides | 2 + debian/patches/0007-spelling.patch | 320 +++++++++++++++++++++++++++++++++++++ debian/patches/series | 1 + 3 files changed, 323 insertions(+) create mode 100644 debian/coq.lintian-overrides create mode 100644 debian/patches/0007-spelling.patch diff --git a/debian/coq.lintian-overrides b/debian/coq.lintian-overrides new file mode 100644 index 00000000..1c84a5d0 --- /dev/null +++ b/debian/coq.lintian-overrides @@ -0,0 +1,2 @@ +# False positive spelling error. +coq binary: spelling-error-in-binary usr/bin/coqwc tage stage diff --git a/debian/patches/0007-spelling.patch b/debian/patches/0007-spelling.patch new file mode 100644 index 00000000..149d11b4 --- /dev/null +++ b/debian/patches/0007-spelling.patch @@ -0,0 +1,320 @@ +From: Benjamin Barenblat +Subject: Correct some spelling errors +Origin: backport, https://github.com/coq/coq/commit/06cd051d140a183229cd43f0bbae152d6ad8d6ca +Reviewed-by: Benjamin Barenblat + +Lintian found some spelling errors in the Debian packaging for coq. Fix +them most places they appear in the current source. (Don't change +documentation anchor names, as that would invalidate external +deeplinks.) + +This also fixes a bug in coqdoc: prior to this commit, coqdoc would +highlight `instanciate` but not `instantiate`. +--- a/ide/nanoPG.ml ++++ b/ide/nanoPG.ml +@@ -189,7 +189,7 @@ + run "Edit" "Cut"; + { s with kill = Some(txt,false); sel = false } + else s)); +- mkE _k "k" "Kill untill the end of line" (Edit(fun s b i _ -> ++ mkE _k "k" "Kill until the end of line" (Edit(fun s b i _ -> + let already_killed = match s.kill with Some (k,true) -> k | _ -> "" in + let k = + if i#ends_line then begin +--- a/kernel/clambda.ml ++++ b/kernel/clambda.ml +@@ -767,7 +767,7 @@ + and such, which can't be done at this time. + for instance, for int31: if one of the digit is + not closed, it's not impossible that the number +- gets fully instanciated at run-time, thus to ensure ++ gets fully instantiated at run-time, thus to ensure + uniqueness of the representation in the vm + it is necessary to try and build a caml integer + during the execution *) +--- a/lib/future.ml ++++ b/lib/future.ml +@@ -49,7 +49,7 @@ + module UUIDMap = Map.Make(UUID) + module UUIDSet = Set.Make(UUID) + +-type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] ++type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] + + (* Val is not necessarily a final state, so the + computation restarts from the state stocked into Val *) +@@ -103,7 +103,7 @@ + let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn + + let create_delegate ?(blocking=true) ~name fix_exn = +- let assignement signal ck = fun v -> ++ let assignment signal ck = fun v -> + let _, _, fix_exn, c = get ck in + assert (match !c with Delegated _ -> true | _ -> false); + begin match v with +@@ -118,7 +118,7 @@ + (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock), + (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in + let ck = create ~name fix_exn (Delegated wait) in +- ck, assignement signal ck ++ ck, assignment signal ck + + (* TODO: get rid of try/catch to be stackless *) + let rec compute ck : 'a value = +--- a/lib/future.mli ++++ b/lib/future.mli +@@ -70,10 +70,10 @@ + (* Run remotely, returns the function to assign. + If not blocking (the default) it raises NotReady if forced before the + delegate assigns it. *) +-type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] ++type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] + val create_delegate : + ?blocking:bool -> name:string -> +- fix_exn -> 'a computation * ('a assignement -> unit) ++ fix_exn -> 'a computation * ('a assignment -> unit) + + (* Given a computation that is_exn, replace it by another one *) + val replace : 'a computation -> 'a computation -> unit +--- a/plugins/funind/functional_principles_proofs.ml ++++ b/plugins/funind/functional_principles_proofs.ml +@@ -638,11 +638,11 @@ + (* observe (str "using snd tac since : " ++ CErrors.print e); *) + tac2 g + +-let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = ++let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = + let args = Array.of_list (List.map mkVar args_id) in +- let instanciate_one_hyp hid = ++ let instantiate_one_hyp hid = + my_orelse +- ( (* we instanciate the hyp if possible *) ++ ( (* we instantiate the hyp if possible *) + fun g -> + let prov_hid = pf_get_new_id hid g in + let c = mkApp(mkVar hid,args) in +@@ -678,7 +678,7 @@ + tclTHENLIST + [ + tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps; +- tclMAP instanciate_one_hyp hyps; ++ tclMAP instantiate_one_hyp hyps; + (fun g -> + let all_g_hyps_id = + List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty +@@ -722,11 +722,11 @@ + tclTHENLIST [Proofview.V82.of_tactic (Simple.case t); + (fun g' -> + let g'_nb_prod = nb_prod (project g') (pf_concl g') in +- let nb_instanciate_partial = g'_nb_prod - g_nb_prod in ++ let nb_instantiate_partial = g'_nb_prod - g_nb_prod in + observe_tac "treat_new_case" + (treat_new_case + ptes_infos +- nb_instanciate_partial ++ nb_instantiate_partial + (build_proof do_finalize) + t + dyn_infos) +@@ -760,7 +760,7 @@ + nb_rec_hyps = List.length new_hyps + } + in +-(* observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' ++(* observe_tac "Lambda" *) (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' + (* build_proof do_finalize new_infos g' *) + ) g + | _ -> +@@ -1118,7 +1118,7 @@ + in + (full_params, (* real params *) + princ_params, (* the params of the principle which are not params of the function *) +- substl (* function instanciated with real params *) ++ substl (* function instantiated with real params *) + (List.map var_of_decl full_params) + f_body + ) +@@ -1128,7 +1128,7 @@ + let f_body = compose_lam f_ctxt_other f_body in + (princ_info.params, (* real params *) + [],(* all params are full params *) +- substl (* function instanciated with real params *) ++ substl (* function instantiated with real params *) + (List.map var_of_decl princ_info.params) + f_body + ) +@@ -1319,7 +1319,7 @@ + (* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *) + + (* ); *) +- (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac ++ (* observe_tac "instancing" *) (instantiate_hyps_with_args prove_tac + (List.rev_map id_of_decl princ_info.branches) + (List.rev args_id)) + ] +@@ -1369,7 +1369,7 @@ + do_prove + dyn_infos + in +- instanciate_hyps_with_args prove_tac ++ instantiate_hyps_with_args prove_tac + (List.rev_map id_of_decl princ_info.branches) + (List.rev args_id) + ] +@@ -1726,8 +1726,8 @@ + ptes_info + (body_info rec_hyps) + in +- (* observe_tac "instanciate_hyps_with_args" *) +- (instanciate_hyps_with_args ++ (* observe_tac "instantiate_hyps_with_args" *) ++ (instantiate_hyps_with_args + make_proof + (List.map (get_name %> Nameops.Name.get_id) princ_info.branches) + (List.rev args_ids) +--- a/plugins/funind/recdef.ml ++++ b/plugins/funind/recdef.ml +@@ -1318,7 +1318,7 @@ + | None -> + try add_suffix current_proof_name "_subproof" + with e when CErrors.noncritical e -> +- anomaly (Pp.str "open_new_goal with an unamed theorem.") ++ anomaly (Pp.str "open_new_goal with an unnamed theorem.") + in + let na = next_global_ident_away name Id.Set.empty in + if Termops.occur_existential sigma gls_type then +--- a/plugins/omega/PreOmega.v ++++ b/plugins/omega/PreOmega.v +@@ -181,7 +181,7 @@ + let t := eval compute in (Z.of_nat (S a)) in + change (Z.of_nat (S a)) with t in H + | _ => rewrite (Nat2Z.inj_succ a) in H +- | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), ++ | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), + hide [Z.of_nat (S a)] in this one hypothesis *) + change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H + end +@@ -192,7 +192,7 @@ + let t := eval compute in (Z.of_nat (S a)) in + change (Z.of_nat (S a)) with t + | _ => rewrite (Nat2Z.inj_succ a) +- | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), ++ | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), + hide [Z.of_nat (S a)] in the goal *) + change (Z.of_nat (S a)) with (Z_of_nat' (S a)) + end +--- a/plugins/omega/omega.ml ++++ b/plugins/omega/omega.ml +@@ -178,7 +178,7 @@ + | DIVIDE_AND_APPROX (e1,e2,k,d) -> + Printf.printf + "Inequation E%d is divided by %s and the constant coefficient is \ +- rounded by substracting %s.\n" e1.id (sbi k) (sbi d) ++ rounded by subtracting %s.\n" e1.id (sbi k) (sbi d) + | NOT_EXACT_DIVIDE (e,k) -> + Printf.printf + "Constant in equation E%d is not divisible by the pgcd \ +--- a/stm/stm.ml ++++ b/stm/stm.ml +@@ -1343,7 +1343,7 @@ + t_stop : Stateid.t; + t_drop : bool; + t_states : competence; +- t_assign : Proof_global.closed_proof_output Future.assignement -> unit; ++ t_assign : Proof_global.closed_proof_output Future.assignment -> unit; + t_loc : Loc.t option; + t_uuid : Future.UUID.t; + t_name : string } +@@ -1381,7 +1381,7 @@ + t_stop : Stateid.t; + t_drop : bool; + t_states : competence; +- t_assign : Proof_global.closed_proof_output Future.assignement -> unit; ++ t_assign : Proof_global.closed_proof_output Future.assignment -> unit; + t_loc : Loc.t option; + t_uuid : Future.UUID.t; + t_name : string } +@@ -1819,7 +1819,7 @@ + type task = { + t_state : Stateid.t; + t_state_fb : Stateid.t; +- t_assign : output Future.assignement -> unit; ++ t_assign : output Future.assignment -> unit; + t_ast : int * aast; + t_goal : Goal.goal; + t_kill : unit -> unit; +@@ -1836,7 +1836,7 @@ + type task = { + t_state : Stateid.t; + t_state_fb : Stateid.t; +- t_assign : output Future.assignement -> unit; ++ t_assign : output Future.assignment -> unit; + t_ast : int * aast; + t_goal : Goal.goal; + t_kill : unit -> unit; +--- a/test-suite/success/univers.v ++++ b/test-suite/success/univers.v +@@ -60,7 +60,7 @@ + + Record U : Type := { A:=Type; a:A }. + +-(** Check assignement of sorts to inductives and records. *) ++(** Check assignment of sorts to inductives and records. *) + + Variable sh : list nat. + +--- a/tools/coq_makefile.ml ++++ b/tools/coq_makefile.ml +@@ -59,7 +59,7 @@ + \n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\ + \n as a dependencies of an already defined target \"foo\".\ + \n[-I dir]: look for Objective Caml dependencies in \"dir\"\ +-\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\ ++\n[-R physicalpath logicalpath]: look for Coq dependencies recursively\ + \n starting from \"physicalpath\". The logical path associated to the\ + \n physical path is \"logicalpath\".\ + \n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\ +--- a/tools/coqdoc/output.ml ++++ b/tools/coqdoc/output.ml +@@ -76,7 +76,7 @@ + [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; + "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; + "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct"; +- "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto"; ++ "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instantiate"; "info_auto"; "info_eauto"; + "quote"; "eexact"; "autorewrite"; + "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; + "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; +--- a/tools/coqworkmgr.ml ++++ b/tools/coqworkmgr.ml +@@ -169,7 +169,7 @@ + "-j",Arg.Set_int max_tokens, "max number of concurrent jobs"; + "-d",Arg.Set debug, "do not detach (debug)"] in + let usage = +- "Prints on stdout an env variable assignement to be picked up by coq\n"^ ++ "Prints on stdout an env variable assignment to be picked up by coq\n"^ + "instances in order to limit the maximum number of concurrent workers.\n"^ + "The default value is 2.\n"^ + "Usage:" in +--- a/vernac/comProgramFixpoint.ml ++++ b/vernac/comProgramFixpoint.ml +@@ -254,7 +254,7 @@ + interp_recursive ~cofix ~program_mode:true fixl ntns + in + (* Program-specific code *) +- (* Get the interesting evars, those that were not instanciated *) ++ (* Get the interesting evars, those that were not instantiated *) + let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in + (* Solve remaining evars *) + let evd = nf_evar_map_undefined evd in +--- a/vernac/obligations.ml ++++ b/vernac/obligations.ml +@@ -338,7 +338,7 @@ + let _ = + declare_bool_option + { optdepr = false; +- optname = "Hidding of Program obligations"; ++ optname = "Hiding of Program obligations"; + optkey = ["Hide";"Obligations"]; + optread = get_hide_obligations; + optwrite = set_hide_obligations; } diff --git a/debian/patches/series b/debian/patches/series index 8e94de36..b098f303 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -4,3 +4,4 @@ 0004-5127-fails-on-mips.patch 0005-remove-ssrmatching.patch 0006-remove-tests-that-need-coqlib.patch +0007-spelling.patch -- cgit v1.2.3