diff options
| -rw-r--r-- | debian/gbp.conf | 6 | ||||
| -rw-r--r-- | debian/patches/0005-remove-tests-that-need-coqlib.patch (renamed from debian/patches/0006-remove-tests-that-need-coqlib.patch) | 0 | ||||
| -rw-r--r-- | debian/patches/0005-ssrmatching-license.patch | 298 | ||||
| -rw-r--r-- | debian/patches/0006-spelling.patch (renamed from debian/patches/0007-spelling.patch) | 0 | ||||
| -rw-r--r-- | debian/patches/0007-avoid-usr-bin-env.patch (renamed from debian/patches/0008-avoid-usr-bin-env.patch) | 0 | ||||
| -rw-r--r-- | debian/patches/0008-python-scripts-libraries.patch (renamed from debian/patches/0009-python-scripts-libraries.patch) | 0 | ||||
| -rw-r--r-- | debian/patches/0009-skip-dot-pc.patch (renamed from debian/patches/0010-skip-dot-pc.patch) | 0 | ||||
| -rw-r--r-- | debian/patches/series | 11 |
8 files changed, 6 insertions, 309 deletions
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/0006-remove-tests-that-need-coqlib.patch b/debian/patches/0005-remove-tests-that-need-coqlib.patch index 48cd1b96..48cd1b96 100644 --- a/debian/patches/0006-remove-tests-that-need-coqlib.patch +++ b/debian/patches/0005-remove-tests-that-need-coqlib.patch 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 <bbaren@debian.org> -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 *) -+(* <O___,, * (see CREDITS file for the list of authors) *) -+(* \VV/ **************************************************************) -+(* // * This file is distributed under the terms of the *) -+(* * GNU Lesser General Public License Version 2.1 *) -+(* * (see LICENSE file for the text of the license) *) -+(************************************************************************) -+ -+(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) -+ -+open Goal -+open Environ -+open Evd -+open Constr -+open Genintern -+ -+(** ******** Small Scale Reflection pattern matching facilities ************* *) -+ -+(** Pattern parsing *) -+ -+(** The type of context patterns, the patterns of the [set] tactic and -+ [:] tactical. These are patterns that identify a precise subterm. *) -+type cpattern -+val pr_cpattern : cpattern -> 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 *) -+(* <O___,, * (see CREDITS file for the list of authors) *) -+(* \VV/ **************************************************************) -+(* // * This file is distributed under the terms of the *) -+(* * GNU Lesser General Public License Version 2.1 *) -+(* * (see LICENSE file for the text of the license) *) -+(************************************************************************) -+ -+(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) -+ -+Declare ML Module "ssrmatching_plugin". -+ -+Module SsrMatchingSyntax. -+ -+(* Reserve the notation for rewrite patterns so that the user is not allowed *) -+(* to declare it at a different level. *) -+Reserved Notation "( a 'in' b )" (at level 0). -+Reserved Notation "( a 'as' b )" (at level 0). -+Reserved Notation "( a 'in' b 'in' c )" (at level 0). -+Reserved Notation "( a 'as' b 'in' c )" (at level 0). -+ -+Delimit Scope ssrpatternscope with pattern. -+ -+(* Notation to define shortcuts for the "X in t" part of a pattern. *) -+Notation "( X 'in' t )" := (_ : fun X => 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/0007-spelling.patch b/debian/patches/0006-spelling.patch index 149d11b4..149d11b4 100644 --- a/debian/patches/0007-spelling.patch +++ b/debian/patches/0006-spelling.patch diff --git a/debian/patches/0008-avoid-usr-bin-env.patch b/debian/patches/0007-avoid-usr-bin-env.patch index 132ed7aa..132ed7aa 100644 --- a/debian/patches/0008-avoid-usr-bin-env.patch +++ b/debian/patches/0007-avoid-usr-bin-env.patch diff --git a/debian/patches/0009-python-scripts-libraries.patch b/debian/patches/0008-python-scripts-libraries.patch index 66a4a9e9..66a4a9e9 100644 --- a/debian/patches/0009-python-scripts-libraries.patch +++ b/debian/patches/0008-python-scripts-libraries.patch diff --git a/debian/patches/0010-skip-dot-pc.patch b/debian/patches/0009-skip-dot-pc.patch index ce85adf8..ce85adf8 100644 --- a/debian/patches/0010-skip-dot-pc.patch +++ b/debian/patches/0009-skip-dot-pc.patch 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 |