From cf916fd97fbac51af6fa68ec2704da2a28ef9ede Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:12:28 -0500 Subject: Prepare to import ssrmatching in 8.9.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Upstream has corrected most of the licensing issues with ssrmatching in 8.9.0. That version introduced one new file with a CeCILL-B license, but it’s an .mli file, so OCaml should be able to infer its contents. Don’t import the offending .mli, but do import the files with corrected license headers. Remove the patch introduced in 5d3dc22cc205021e517a81943952655c51777083 (which backported the correctly licensed files). --- debian/gbp.conf | 6 +- .../0005-remove-tests-that-need-coqlib.patch | 633 +++++++++++++++++++++ debian/patches/0005-ssrmatching-license.patch | 298 ---------- .../0006-remove-tests-that-need-coqlib.patch | 633 --------------------- debian/patches/0006-spelling.patch | 320 +++++++++++ debian/patches/0007-avoid-usr-bin-env.patch | 32 ++ debian/patches/0007-spelling.patch | 320 ----------- debian/patches/0008-avoid-usr-bin-env.patch | 32 -- debian/patches/0008-python-scripts-libraries.patch | 20 + debian/patches/0009-python-scripts-libraries.patch | 20 - debian/patches/0009-skip-dot-pc.patch | 13 + debian/patches/0010-skip-dot-pc.patch | 13 - debian/patches/series | 11 +- 13 files changed, 1024 insertions(+), 1327 deletions(-) create mode 100644 debian/patches/0005-remove-tests-that-need-coqlib.patch delete mode 100644 debian/patches/0005-ssrmatching-license.patch delete mode 100644 debian/patches/0006-remove-tests-that-need-coqlib.patch create mode 100644 debian/patches/0006-spelling.patch create mode 100644 debian/patches/0007-avoid-usr-bin-env.patch delete mode 100644 debian/patches/0007-spelling.patch delete mode 100644 debian/patches/0008-avoid-usr-bin-env.patch create mode 100644 debian/patches/0008-python-scripts-libraries.patch delete mode 100644 debian/patches/0009-python-scripts-libraries.patch create mode 100644 debian/patches/0009-skip-dot-pc.patch delete mode 100644 debian/patches/0010-skip-dot-pc.patch diff --git a/debian/gbp.conf b/debian/gbp.conf index a4ee2a5f..92f87323 100644 --- a/debian/gbp.conf +++ b/debian/gbp.conf @@ -51,11 +51,7 @@ filter = [ # Code with CeCILL-B license headers. bbaren believes CeCILL-B to be # nonfree; see # https://lists.debian.org/msgid-search/875zvih02a.jfx@benwick.benjamin.barenblat.name. - # - # These files will be patched in with properly licensed replacements once - # https://github.com/coq/coq/pull/9282 is merged. - "plugins/ssrmatching/ssrmatching.mli", - "plugins/ssrmatching/ssrmatching.v", + "plugins/ssrmatching/g_ssrmatching.mli", # This tries to build upstream's CI on Salsa, which doesn't work. ".travis.yml" ] diff --git a/debian/patches/0005-remove-tests-that-need-coqlib.patch b/debian/patches/0005-remove-tests-that-need-coqlib.patch new file mode 100644 index 00000000..48cd1b96 --- /dev/null +++ b/debian/patches/0005-remove-tests-that-need-coqlib.patch @@ -0,0 +1,633 @@ +From: Benjamin Barenblat +Subject: Disable tests which require -coqlib to be set +Bug: https://github.com/coq/coq/issues/5975 +Forwarded: not-needed + +A number of tests (mostly for coq_makefile) assume that Coq is +installed when the test runs. This isn't true in an sbuild environment, +though, so disable those tests. +--- a/test-suite/misc/printers.sh ++++ /dev/null +@@ -1,3 +0,0 @@ +-printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound" +-if [ $? = 0 ]; then exit 1; else exit 0; fi +- +--- a/test-suite/coq-makefile/arg/run.sh ++++ /dev/null +@@ -1,7 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +--- a/test-suite/coq-makefile/compat-subdirs/run.sh ++++ /dev/null +@@ -1,8 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-exec test -f "subdir/done" +--- a/test-suite/coq-makefile/coqdoc1/run.sh ++++ /dev/null +@@ -1,51 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-make install-doc DSTROOT="$PWD/tmp" +-#make debug +-(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort -u > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort -u > desired <> src/test_aux.ml +-export OCAMLPATH=$OCAMLPATH:$PWD/findlib +-if which cygpath 2>/dev/null; then +- # the only way I found to pass OCAMLPATH on win is to have it contain +- # only one entry +- export OCAMLPATH=`cygpath -w $PWD/findlib` +-fi +-make -C findlib/foo clean +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-cat Makefile.local +-make -C findlib/foo +-make +-make byte +--- a/test-suite/coq-makefile/latex1/run.sh ++++ /dev/null +@@ -1,13 +0,0 @@ +-#!/usr/bin/env bash +- +-if which pdflatex; then +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-exec make all.pdf +- +-fi +-exit 0 # test skipped +--- a/test-suite/coq-makefile/merlin1/run.sh ++++ /dev/null +@@ -1,13 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make .merlin +-cat > desired < actual +-exec diff -u desired actual +--- a/test-suite/coq-makefile/mlpack1/run.sh ++++ /dev/null +@@ -1,23 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-#make debug +-(cd `find tmp -name user-contrib` && find .) | sort > actual +-sort > desired < actual +-sort > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort > desired < actual +-sort > desired < actual +-sort > desired < actual +-sort > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort -u > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort -u > desired < ${file}${ext}.processed +- done +-done +-for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do +- echo "cat $file" +- cat "$file" +- echo +- diff -u $file.desired.processed $file.processed || exit $? +-done +- +-cd ../per-file-before +-coq_makefile -f _CoqProject -o Makefile +-make cleanall +-make all TIMING=before -j2 || exit $? +- +-cd ../per-file-after +-coq_makefile -f _CoqProject -o Makefile +-make cleanall +-make all TIMING=after -j2 || exit $? +- +-find ../per-file-before/ -name "*.before-timing" -exec 'cp' '{}' './' ';' +-make all.timing.diff -j2 || exit $? +-echo "cat A.v.before-timing" +-cat A.v.before-timing +-echo +-echo "cat A.v.after-timing" +-cat A.v.after-timing +-echo +-echo "cat A.v.timing.diff" +-cat A.v.timing.diff +-echo +- +-for ext in "" .desired; do +- for file in A.v.timing.diff; do +- cat ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" | sort > ${file}${ext}.processed +- done +-done +-for file in A.v.timing.diff; do +- diff -u $file.desired.processed $file.processed || exit $? +-done +- +-exit 0 diff --git a/debian/patches/0005-ssrmatching-license.patch b/debian/patches/0005-ssrmatching-license.patch deleted file mode 100644 index f207cc8b..00000000 --- a/debian/patches/0005-ssrmatching-license.patch +++ /dev/null @@ -1,298 +0,0 @@ -From: Benjamin Barenblat -Subject: Replace deleted non-free ssrmatching files with free ones -Forwarded: not-needed -Last-Update: 2019-01-17 - -Coq 8.8.2 shipped with two files in ssrmatching that were licensed under -CeCILL-B, which I believe is a nonfree license. I've removed them from -the Debian source package (see gbp.conf). This patch replaces them with -equivalent files (from a later version) that are licensed freely. - -These files are present starting at upstream commit -f613d9f9f0c8aec814272f6c2dcdce7e70da47b6. I've modified them by where required -to get them to compile against 8.8.2. ---- /dev/null -+++ b/plugins/ssrmatching/ssrmatching.mli -@@ -0,0 +1,242 @@ -+(************************************************************************) -+(* * The Coq Proof Assistant / The Coq Development Team *) -+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -+(* Pp.t -+ -+(** The type of rewrite patterns, the patterns of the [rewrite] tactic. -+ These patterns also include patterns that identify all the subterms -+ of a context (i.e. "in" prefix) *) -+type rpattern -+val pr_rpattern : rpattern -> Pp.t -+ -+(** Pattern interpretation and matching *) -+ -+exception NoMatch -+exception NoProgress -+ -+(** AST for [rpattern] (and consequently [cpattern]) *) -+type ('ident, 'term) ssrpattern = -+ | T of 'term -+ | In_T of 'term -+ | X_In_T of 'ident * 'term -+ | In_X_In_T of 'ident * 'term -+ | E_In_X_In_T of 'term * 'ident * 'term -+ | E_As_X_In_T of 'term * 'ident * 'term -+ -+type pattern = evar_map * (constr, constr) ssrpattern -+val pp_pattern : pattern -> Pp.t -+ -+(** Extracts the redex and applies to it the substitution part of the pattern. -+ @raise Anomaly if called on [In_T] or [In_X_In_T] *) -+val redex_of_pattern : -+ ?resolve_typeclasses:bool -> env -> pattern -> -+ constr Evd.in_evar_universe_context -+ -+(** [interp_rpattern ise gl rpat] "internalizes" and "interprets" [rpat] -+ in the current [Ltac] interpretation signature [ise] and tactic input [gl]*) -+val interp_rpattern : -+ goal sigma -> -+ rpattern -> -+ pattern -+ -+(** [interp_cpattern ise gl cpat ty] "internalizes" and "interprets" [cpat] -+ in the current [Ltac] interpretation signature [ise] and tactic input [gl]. -+ [ty] is an optional type for the redex of [cpat] *) -+val interp_cpattern : -+ goal sigma -> -+ cpattern -> (Tacexpr.glob_constr_and_expr * Geninterp.interp_sign) option -> -+ pattern -+ -+(** The set of occurrences to be matched. The boolean is set to true -+ * to signal the complement of this set (i.e. \{-1 3\}) *) -+type occ = (bool * int list) option -+ -+(** [subst e p t i]. [i] is the number of binders -+ traversed so far, [p] the term from the pattern, [t] the matched one *) -+type subst = env -> constr -> constr -> int -> constr -+ -+(** [eval_pattern b env sigma t pat occ subst] maps [t] calling [subst] on every -+ [occ] occurrence of [pat]. The [int] argument is the number of -+ binders traversed. If [pat] is [None] then then subst is called on [t]. -+ [t] must live in [env] and [sigma], [pat] must have been interpreted in -+ (an extension of) [sigma]. -+ @raise NoMatch if [pat] has no occurrence and [b] is [true] (default [false]) -+ @return [t] where all [occ] occurrences of [pat] have been mapped using -+ [subst] *) -+val eval_pattern : -+ ?raise_NoMatch:bool -> -+ env -> evar_map -> constr -> -+ pattern option -> occ -> subst -> -+ constr -+ -+(** [fill_occ_pattern b env sigma t pat occ h] is a simplified version of -+ [eval_pattern]. -+ It replaces all [occ] occurrences of [pat] in [t] with Rel [h]. -+ [t] must live in [env] and [sigma], [pat] must have been interpreted in -+ (an extension of) [sigma]. -+ @raise NoMatch if [pat] has no occurrence and [b] is [true] (default [false]) -+ @return the instance of the redex of [pat] that was matched and [t] -+ transformed as described above. *) -+val fill_occ_pattern : -+ ?raise_NoMatch:bool -> -+ env -> evar_map -> constr -> -+ pattern -> occ -> int -> -+ constr Evd.in_evar_universe_context * constr -+ -+(** *************************** Low level APIs ****************************** *) -+ -+(* The primitive matching facility. It matches of a term with holes, like -+ the T pattern above, and calls a continuation on its occurrences. *) -+ -+type ssrdir = L2R | R2L -+val pr_dir_side : ssrdir -> Pp.t -+ -+(** a pattern for a term with wildcards *) -+type tpattern -+ -+(** [mk_tpattern env sigma0 sigma_p ok p_origin dir t] compiles a term [t] -+ living in [env] [sigma] (an extension of [sigma0]) intro a [tpattern]. -+ The [tpattern] can hold a (proof) term [p] and a diction [dir]. The [ok] -+ callback is used to filter occurrences. -+ @return the compiled [tpattern] and its [evar_map] -+ @raise UserEerror is the pattern is a wildcard *) -+val mk_tpattern : -+ ?p_origin:ssrdir * constr -> -+ env -> evar_map -> -+ evar_map * constr -> -+ (constr -> evar_map -> bool) -> -+ ssrdir -> constr -> -+ evar_map * tpattern -+ -+(** [findP env t i k] is a stateful function that finds the next occurrence -+ of a tpattern and calls the callback [k] to map the subterm matched. -+ The [int] argument passed to [k] is the number of binders traversed so far -+ plus the initial value [i]. -+ @return [t] where the subterms identified by the selected occurrences of -+ the patter have been mapped using [k] -+ @raise NoMatch if the raise_NoMatch flag given to [mk_tpattern_matcher] is -+ [true] and if the pattern did not match -+ @raise UserEerror if the raise_NoMatch flag given to [mk_tpattern_matcher] is -+ [false] and if the pattern did not match *) -+type find_P = -+ env -> constr -> int -> k:subst -> constr -+ -+(** [conclude ()] asserts that all mentioned ocurrences have been visited. -+ @return the instance of the pattern, the evarmap after the pattern -+ instantiation, the proof term and the ssrdit stored in the tpattern -+ @raise UserEerror if too many occurrences were specified *) -+type conclude = -+ unit -> constr * ssrdir * (evar_map * UState.t * constr) -+ -+(** [mk_tpattern_matcher b o sigma0 occ sigma_tplist] creates a pair -+ a function [find_P] and [conclude] with the behaviour explained above. -+ The flag [b] (default [false]) changes the error reporting behaviour -+ of [find_P] if none of the [tpattern] matches. The argument [o] can -+ be passed to tune the [UserError] eventually raised (useful if the -+ pattern is coming from the LHS/RHS of an equation) *) -+val mk_tpattern_matcher : -+ ?all_instances:bool -> -+ ?raise_NoMatch:bool -> -+ ?upats_origin:ssrdir * constr -> -+ evar_map -> occ -> evar_map * tpattern list -> -+ find_P * conclude -+ -+(** Example of [mk_tpattern_matcher] to implement -+ [rewrite \{occ\}\[in t\]rules]. -+ It first matches "in t" (called [pat]), then in all matched subterms -+ it matches the LHS of the rules using [find_R]. -+ [concl0] is the initial goal, [concl] will be the goal where some terms -+ are replaced by a De Bruijn index. The [rw_progress] extra check -+ selects only occurrences that are not rewritten to themselves (e.g. -+ an occurrence "x + x" rewritten with the commutativity law of addition -+ is skipped) {[ -+ let find_R, conclude = match pat with -+ | Some (_, In_T _) -> -+ let aux (sigma, pats) (d, r, lhs, rhs) = -+ let sigma, pat = -+ mk_tpattern env0 sigma0 (sigma, r) (rw_progress rhs) d lhs in -+ sigma, pats @ [pat] in -+ let rpats = List.fold_left aux (r_sigma, []) rules in -+ let find_R, end_R = mk_tpattern_matcher sigma0 occ rpats in -+ find_R ~k:(fun _ _ h -> mkRel h), -+ fun cl -> let rdx, d, r = end_R () in (d,r),rdx -+ | _ -> ... in -+ let concl = eval_pattern env0 sigma0 concl0 pat occ find_R in -+ let (d, r), rdx = conclude concl in ]} *) -+ -+(* convenience shortcut: [pf_fill_occ_term gl occ (sigma,t)] returns -+ * the conclusion of [gl] where [occ] occurrences of [t] have been replaced -+ * by [Rel 1] and the instance of [t] *) -+val pf_fill_occ_term : goal sigma -> occ -> evar_map * EConstr.t -> EConstr.t * EConstr.t -+ -+(* It may be handy to inject a simple term into the first form of cpattern *) -+val cpattern_of_term : char * Tacexpr.glob_constr_and_expr -> Geninterp.interp_sign -> cpattern -+ -+(** Helpers to make stateful closures. Example: a [find_P] function may be -+ called many times, but the pattern instantiation phase is performed only the -+ first time. The corresponding [conclude] has to return the instantiated -+ pattern redex. Since it is up to [find_P] to raise [NoMatch] if the pattern -+ has no instance, [conclude] considers it an anomaly if the pattern did -+ not match *) -+ -+(** [do_once r f] calls [f] and updates the ref only once *) -+val do_once : 'a option ref -> (unit -> 'a) -> unit -+ -+(** [assert_done r] return the content of r. @raise Anomaly is r is [None] *) -+val assert_done : 'a option ref -> 'a -+ -+(** Very low level APIs. -+ these are calls to evarconv's [the_conv_x] followed by -+ [solve_unif_constraints_with_heuristics]. -+ In case of failure they raise [NoMatch] *) -+ -+val unify_HO : env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map -+val pf_unify_HO : goal sigma -> EConstr.constr -> EConstr.constr -> goal sigma -+ -+(** Some more low level functions needed to implement the full SSR language -+ on top of the former APIs *) -+val tag_of_cpattern : cpattern -> char -+val loc_of_cpattern : cpattern -> Loc.t option -+val id_of_pattern : pattern -> Names.Id.t option -+val is_wildcard : cpattern -> bool -+val cpattern_of_id : Names.Id.t -> cpattern -+val pr_constr_pat : constr -> Pp.t -+val pf_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma -+val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma -+ -+(* One can also "Set SsrMatchingDebug" from a .v *) -+val debug : bool -> unit -+ -+val ssrinstancesof : cpattern -> Tacmach.tactic -+ -+val profile : bool -> unit -+val wit_cpattern : cpattern Genarg.uniform_genarg_type -+val lcpattern : cpattern Pcoq.Gram.entry -+val wit_lcpattern : cpattern Genarg.uniform_genarg_type -+val cpattern : cpattern Pcoq.Gram.entry -+val wit_rpattern : rpattern Genarg.uniform_genarg_type -+val rpattern : rpattern Pcoq.Gram.entry -+ -+(* eof *) ---- /dev/null -+++ b/plugins/ssrmatching/ssrmatching.v -@@ -0,0 +1,37 @@ -+(************************************************************************) -+(* * The Coq Proof Assistant / The Coq Development Team *) -+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -+(* t) : ssrpatternscope. -+ -+(* Some shortcuts for recurrent "X in t" parts. *) -+Notation RHS := (X in _ = X)%pattern. -+Notation LHS := (X in X = _)%pattern. -+ -+End SsrMatchingSyntax. -+ -+Export SsrMatchingSyntax. -+ -+Tactic Notation "ssrpattern" ssrpatternarg(p) := ssrpattern p . diff --git a/debian/patches/0006-remove-tests-that-need-coqlib.patch b/debian/patches/0006-remove-tests-that-need-coqlib.patch deleted file mode 100644 index 48cd1b96..00000000 --- a/debian/patches/0006-remove-tests-that-need-coqlib.patch +++ /dev/null @@ -1,633 +0,0 @@ -From: Benjamin Barenblat -Subject: Disable tests which require -coqlib to be set -Bug: https://github.com/coq/coq/issues/5975 -Forwarded: not-needed - -A number of tests (mostly for coq_makefile) assume that Coq is -installed when the test runs. This isn't true in an sbuild environment, -though, so disable those tests. ---- a/test-suite/misc/printers.sh -+++ /dev/null -@@ -1,3 +0,0 @@ --printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound" --if [ $? = 0 ]; then exit 1; else exit 0; fi -- ---- a/test-suite/coq-makefile/arg/run.sh -+++ /dev/null -@@ -1,7 +0,0 @@ --#!/usr/bin/env bash -- --. ../template/init.sh -- --coq_makefile -f _CoqProject -o Makefile --cat Makefile.conf --make ---- a/test-suite/coq-makefile/compat-subdirs/run.sh -+++ /dev/null -@@ -1,8 +0,0 @@ --#!/usr/bin/env bash -- --. ../template/init.sh -- --coq_makefile -f _CoqProject -o Makefile --cat Makefile.conf --make --exec test -f "subdir/done" ---- a/test-suite/coq-makefile/coqdoc1/run.sh -+++ /dev/null -@@ -1,51 +0,0 @@ --#!/usr/bin/env bash -- --. ../template/init.sh -- --coq_makefile -f _CoqProject -o Makefile --cat Makefile.conf --make --make html mlihtml --make install DSTROOT="$PWD/tmp" --make install-doc DSTROOT="$PWD/tmp" --#make debug --(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual --sort -u > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual --sort -u > desired <> src/test_aux.ml --export OCAMLPATH=$OCAMLPATH:$PWD/findlib --if which cygpath 2>/dev/null; then -- # the only way I found to pass OCAMLPATH on win is to have it contain -- # only one entry -- export OCAMLPATH=`cygpath -w $PWD/findlib` --fi --make -C findlib/foo clean --coq_makefile -f _CoqProject -o Makefile --cat Makefile.conf --cat Makefile.local --make -C findlib/foo --make --make byte ---- a/test-suite/coq-makefile/latex1/run.sh -+++ /dev/null -@@ -1,13 +0,0 @@ --#!/usr/bin/env bash -- --if which pdflatex; then -- --. ../template/init.sh -- --coq_makefile -f _CoqProject -o Makefile --cat Makefile.conf --make --exec make all.pdf -- --fi --exit 0 # test skipped ---- a/test-suite/coq-makefile/merlin1/run.sh -+++ /dev/null -@@ -1,13 +0,0 @@ --#!/usr/bin/env bash -- --. ../template/init.sh -- --coq_makefile -f _CoqProject -o Makefile --cat Makefile.conf --make .merlin --cat > desired < actual --exec diff -u desired actual ---- a/test-suite/coq-makefile/mlpack1/run.sh -+++ /dev/null -@@ -1,23 +0,0 @@ --#!/usr/bin/env bash -- --. ../template/init.sh -- --coq_makefile -f _CoqProject -o Makefile --cat Makefile.conf --make --make html mlihtml --make install DSTROOT="$PWD/tmp" --#make debug --(cd `find tmp -name user-contrib` && find .) | sort > actual --sort > desired < actual --sort > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual --sort > desired < actual --sort > desired < actual --sort > desired < actual --sort > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual --sort -u > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual --sort -u > desired < ${file}${ext}.processed -- done --done --for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do -- echo "cat $file" -- cat "$file" -- echo -- diff -u $file.desired.processed $file.processed || exit $? --done -- --cd ../per-file-before --coq_makefile -f _CoqProject -o Makefile --make cleanall --make all TIMING=before -j2 || exit $? -- --cd ../per-file-after --coq_makefile -f _CoqProject -o Makefile --make cleanall --make all TIMING=after -j2 || exit $? -- --find ../per-file-before/ -name "*.before-timing" -exec 'cp' '{}' './' ';' --make all.timing.diff -j2 || exit $? --echo "cat A.v.before-timing" --cat A.v.before-timing --echo --echo "cat A.v.after-timing" --cat A.v.after-timing --echo --echo "cat A.v.timing.diff" --cat A.v.timing.diff --echo -- --for ext in "" .desired; do -- for file in A.v.timing.diff; do -- cat ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" | sort > ${file}${ext}.processed -- done --done --for file in A.v.timing.diff; do -- diff -u $file.desired.processed $file.processed || exit $? --done -- --exit 0 diff --git a/debian/patches/0006-spelling.patch b/debian/patches/0006-spelling.patch new file mode 100644 index 00000000..149d11b4 --- /dev/null +++ b/debian/patches/0006-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/0007-avoid-usr-bin-env.patch b/debian/patches/0007-avoid-usr-bin-env.patch new file mode 100644 index 00000000..132ed7aa --- /dev/null +++ b/debian/patches/0007-avoid-usr-bin-env.patch @@ -0,0 +1,32 @@ +From: Benjamin Barenblat +Subject: Avoid invoking /usr/bin/env +Forwarded: not-needed + +Per Debian Python policy [1], use `/usr/bin/python3` rather than +`/usr/bin/env python` to refer to the system Python (3) interpreter. + +[1] https://www.debian.org/doc/packaging-manuals/python-policy/python.html#interpreter_loc +--- a/tools/make-both-single-timing-files.py ++++ b/tools/make-both-single-timing-files.py +@@ -1,4 +1,4 @@ +-#!/usr/bin/env python ++#!/usr/bin/python3 + import sys + from TimeFileMaker import * + +--- a/tools/make-both-time-files.py ++++ b/tools/make-both-time-files.py +@@ -1,4 +1,4 @@ +-#!/usr/bin/env python ++#!/usr/bin/python3 + import sys + from TimeFileMaker import * + +--- a/tools/make-one-time-file.py ++++ b/tools/make-one-time-file.py +@@ -1,4 +1,4 @@ +-#!/usr/bin/env python ++#!/usr/bin/python3 + import sys + from TimeFileMaker import * + diff --git a/debian/patches/0007-spelling.patch b/debian/patches/0007-spelling.patch deleted file mode 100644 index 149d11b4..00000000 --- a/debian/patches/0007-spelling.patch +++ /dev/null @@ -1,320 +0,0 @@ -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/0008-avoid-usr-bin-env.patch b/debian/patches/0008-avoid-usr-bin-env.patch deleted file mode 100644 index 132ed7aa..00000000 --- a/debian/patches/0008-avoid-usr-bin-env.patch +++ /dev/null @@ -1,32 +0,0 @@ -From: Benjamin Barenblat -Subject: Avoid invoking /usr/bin/env -Forwarded: not-needed - -Per Debian Python policy [1], use `/usr/bin/python3` rather than -`/usr/bin/env python` to refer to the system Python (3) interpreter. - -[1] https://www.debian.org/doc/packaging-manuals/python-policy/python.html#interpreter_loc ---- a/tools/make-both-single-timing-files.py -+++ b/tools/make-both-single-timing-files.py -@@ -1,4 +1,4 @@ --#!/usr/bin/env python -+#!/usr/bin/python3 - import sys - from TimeFileMaker import * - ---- a/tools/make-both-time-files.py -+++ b/tools/make-both-time-files.py -@@ -1,4 +1,4 @@ --#!/usr/bin/env python -+#!/usr/bin/python3 - import sys - from TimeFileMaker import * - ---- a/tools/make-one-time-file.py -+++ b/tools/make-one-time-file.py -@@ -1,4 +1,4 @@ --#!/usr/bin/env python -+#!/usr/bin/python3 - import sys - from TimeFileMaker import * - diff --git a/debian/patches/0008-python-scripts-libraries.patch b/debian/patches/0008-python-scripts-libraries.patch new file mode 100644 index 00000000..66a4a9e9 --- /dev/null +++ b/debian/patches/0008-python-scripts-libraries.patch @@ -0,0 +1,20 @@ +From: Benjamin Barenblat +Subject: Differentiate between Python scripts and libraries +Forwarded: not-needed + +Eliminate the .py extension from executable Python scripts. +--- a/tools/CoqMakefile.in ++++ b/tools/CoqMakefile.in +@@ -91,9 +91,9 @@ + COQMKFILE ?= "$(COQBIN)coq_makefile" + + # Timing scripts +-COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" +-COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" +-COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" ++COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file" ++COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files" ++COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files" + BEFORE ?= + AFTER ?= + diff --git a/debian/patches/0009-python-scripts-libraries.patch b/debian/patches/0009-python-scripts-libraries.patch deleted file mode 100644 index 66a4a9e9..00000000 --- a/debian/patches/0009-python-scripts-libraries.patch +++ /dev/null @@ -1,20 +0,0 @@ -From: Benjamin Barenblat -Subject: Differentiate between Python scripts and libraries -Forwarded: not-needed - -Eliminate the .py extension from executable Python scripts. ---- a/tools/CoqMakefile.in -+++ b/tools/CoqMakefile.in -@@ -91,9 +91,9 @@ - COQMKFILE ?= "$(COQBIN)coq_makefile" - - # Timing scripts --COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" --COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" --COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" -+COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file" -+COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files" -+COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files" - BEFORE ?= - AFTER ?= - diff --git a/debian/patches/0009-skip-dot-pc.patch b/debian/patches/0009-skip-dot-pc.patch new file mode 100644 index 00000000..ce85adf8 --- /dev/null +++ b/debian/patches/0009-skip-dot-pc.patch @@ -0,0 +1,13 @@ +From: Benjamin Barenblat +Subject: Ignore .pc directory when building +Forwarded: no +--- a/Makefile ++++ b/Makefile +@@ -53,6 +53,7 @@ + -name '.git' -o \ + -name '.bzr' -o \ + -name 'debian' -o \ ++ -name '.pc' -o \ + -name "$${GIT_DIR}" -o \ + -name '_build' -o \ + -name '_build_ci' -o \ diff --git a/debian/patches/0010-skip-dot-pc.patch b/debian/patches/0010-skip-dot-pc.patch deleted file mode 100644 index ce85adf8..00000000 --- a/debian/patches/0010-skip-dot-pc.patch +++ /dev/null @@ -1,13 +0,0 @@ -From: Benjamin Barenblat -Subject: Ignore .pc directory when building -Forwarded: no ---- a/Makefile -+++ b/Makefile -@@ -53,6 +53,7 @@ - -name '.git' -o \ - -name '.bzr' -o \ - -name 'debian' -o \ -+ -name '.pc' -o \ - -name "$${GIT_DIR}" -o \ - -name '_build' -o \ - -name '_build_ci' -o \ diff --git a/debian/patches/series b/debian/patches/series index 7253c063..d2f569c1 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -2,9 +2,8 @@ 0002-Remove-test-4429.patch 0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch 0004-5127-fails-on-mips.patch -0005-ssrmatching-license.patch -0006-remove-tests-that-need-coqlib.patch -0007-spelling.patch -0008-avoid-usr-bin-env.patch -0009-python-scripts-libraries.patch -0010-skip-dot-pc.patch +0005-remove-tests-that-need-coqlib.patch +0006-spelling.patch +0007-avoid-usr-bin-env.patch +0008-python-scripts-libraries.patch +0009-skip-dot-pc.patch -- cgit v1.2.3