diff options
| -rw-r--r-- | .gitlab-ci.yml | 14 | ||||
| -rw-r--r-- | Makefile.ci | 3 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 7 | ||||
| -rwxr-xr-x | dev/ci/ci-equations.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-metacoq.sh | 8 | ||||
| -rw-r--r-- | doc/changelog/04-tactics/11362-micromega-fix-11191.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 2 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 2 | ||||
| -rw-r--r-- | doc/stdlib/hidden-files | 1 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 2 | ||||
| -rw-r--r-- | kernel/kernel.mllib | 2 | ||||
| -rw-r--r-- | kernel/reduction.ml | 2 | ||||
| -rw-r--r-- | kernel/relevanceops.ml (renamed from kernel/retypeops.ml) | 0 | ||||
| -rw-r--r-- | kernel/relevanceops.mli (renamed from kernel/retypeops.mli) | 0 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 2 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 15 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 10 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 12 | ||||
| -rw-r--r-- | theories/micromega/ZifyPow.v | 1 |
19 files changed, 71 insertions, 19 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 5b343a23c5..cf1dc47fab 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -731,10 +731,24 @@ plugin:ci-elpi: plugin:ci-equations: extends: .ci-template + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build_ci plugin:ci-fiat_parsers: extends: .ci-template +plugin:ci-metacoq: + extends: .ci-template + stage: stage-3 + needs: + - build:base + - plugin:ci-equations + dependencies: + - build:base + - plugin:ci-equations + plugin:ci-mtac2: extends: .ci-template diff --git a/Makefile.ci b/Makefile.ci index dfb3f69a8c..f58dd9f37a 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -33,6 +33,7 @@ CI_TARGETS= \ ci-iris-lambda-rust \ ci-math-classes \ ci-math-comp \ + ci-metacoq \ ci-mtac2 \ ci-paramcoq \ ci-perennial \ @@ -72,6 +73,8 @@ ci-fiat-crypto: ci-coqprime ci-rewriter ci-simple-io: ci-ext-lib ci-quickchick: ci-ext-lib ci-simple-io +ci-metacoq: ci-equations + # Generic rule, we use make to ease CI integration $(CI_TARGETS): ci-%: +./dev/ci/ci-wrapper.sh $* diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index bd7ee46358..70e3fe5c69 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -330,3 +330,10 @@ : "${perennial_CI_REF:=master}" : "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}" : "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}" + +######################################################################## +# metacoq +######################################################################## +: "${metacoq_CI_REF:=master}" +: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}" +: "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}" diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh index 871d033f5b..30047e624b 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download equations -( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci) +( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci && make install ) diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh new file mode 100755 index 0000000000..1302065961 --- /dev/null +++ b/dev/ci/ci-metacoq.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download metacoq + +( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make ci-local && make install ) diff --git a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst index 79879c78d5..20d48929f2 100644 --- a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst +++ b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst @@ -1,5 +1,8 @@ - **Fixed:** - Regression of :tacn:`lia` due to more powerful :tacn:`zify` + :tacn:`zify` now handles :g:`Z.pow_pos` by default. + In Coq 8.11, this was the case only when loading module + :g:`ZifyPow` because this triggered a regression of :tacn:`lia`. + The regression is now fixed, and the module kept only for compatibility (`#11362 <https://github.com/coq/coq/pull/11362>`_, fixes `#11191 <https://github.com/coq/coq/issues/11191>`_, by Frédéric Besson). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index a0cf9730a9..f76b60097a 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -4,7 +4,7 @@ Recent changes -------------- -.. ifconfig:: not coq_config.is_a_released_version +.. ifconfig:: not is_a_released_version .. include:: ../unreleased.rst diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index c2c1c68f5c..2ed9ec21b3 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -100,7 +100,7 @@ def copy_formatspecific_files(app): def setup(app): app.connect('builder-inited', copy_formatspecific_files) - app.add_config_value('coq_config', coq_config, 'env') + app.add_config_value('is_a_released_version', coq_config.is_a_released_version, 'env') # The master toctree document. # We create this file in `copy_master_doc` above. diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 60d6039b0f..67d0b37e81 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -50,6 +50,7 @@ theories/micromega/ZifyInst.v theories/micromega/ZifyBool.v theories/micromega/ZifyComparison.v theories/micromega/ZifyClasses.v +theories/micromega/ZifyPow.v theories/micromega/Zify.v theories/nsatz/Nsatz.v theories/omega/Omega.v diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 84f32e187b..0b94b0d675 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -519,7 +519,7 @@ class ProductionObject(CoqObject): row = nodes.inline(classes=['prodn-row']) entry = nodes.inline(classes=['prodn-cell-nonterminal']) if lhs != "": - target_name = 'grammar-token-' + lhs + target_name = 'grammar-token-' + nodes.make_id(lhs) target = nodes.target('', '', ids=[target_name], names=[target_name]) # putting prodn-target on the target node won't appear in the tex file inline = nodes.inline(classes=['prodn-target']) diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index f1e994b337..cc9da3a2ce 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -27,7 +27,7 @@ Conv_oracle Environ Primred CClosure -Retypeops +Relevanceops Reduction Clambda Nativelambda diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 5fbe501169..469d5ccaa2 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -331,7 +331,7 @@ let skip_pattern infos n c1 c2 = let is_irrelevant infos lft c = let env = info_env infos.cnv_inf in - try Retypeops.relevance_of_fterm env infos.relevances lft c == Sorts.Irrelevant with _ -> false + try Relevanceops.relevance_of_fterm env infos.relevances lft c == Sorts.Irrelevant with _ -> false (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = diff --git a/kernel/retypeops.ml b/kernel/relevanceops.ml index 3f3e722245..3f3e722245 100644 --- a/kernel/retypeops.ml +++ b/kernel/relevanceops.ml diff --git a/kernel/retypeops.mli b/kernel/relevanceops.mli index 86734e747e..86734e747e 100644 --- a/kernel/retypeops.mli +++ b/kernel/relevanceops.mli diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 0c89d51033..c8c2301171 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -143,7 +143,7 @@ let infer_declaration env (dcl : constant_entry) = Cooking.cook_body = def; cook_type = typ; cook_universes = univs; - cook_relevance = Retypeops.relevance_of_term env j.uj_val; + cook_relevance = Relevanceops.relevance_of_term env j.uj_val; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index c92c9a75a0..b5d81f762a 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -530,22 +530,25 @@ let change_sort_arity sort = corresponding eta-expanded term *) let weaken_sort_scheme env evd set sort npars term ty = let evdref = ref evd in - let rec drec np elim = + let rec drec ctx np elim = match kind elim with | Prod (n,t,c) -> + let ctx = LocalAssum (n, t) :: ctx in if Int.equal np 0 then let osort, t' = change_sort_arity sort t in evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort) env !evdref sort osort; mkProd (n, t', c), - mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1))) + mkLambda (n, t', mkApp(term, Context.Rel.to_extended_vect mkRel 0 ctx)) else - let c',term' = drec (np-1) c in + let c',term' = drec ctx (np-1) c in mkProd (n, t, c'), mkLambda (n, t, term') - | LetIn (n,b,t,c) -> let c',term' = drec np c in - mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') + | LetIn (n,b,t,c) -> + let ctx = LocalDef (n, b, t) :: ctx in + let c',term' = drec ctx np c in + mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type.") in - let ty, term = drec npars ty in + let ty, term = drec [] npars ty in !evdref, ty, term (**********************************************************************) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index d4fa2461b4..821c57d033 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -273,8 +273,8 @@ let relevance_of_term env sigma c = | Rel n -> let len = Range.length rels in if n <= len then Range.get rels (n - 1) - else Retypeops.relevance_of_rel env (n - len) - | Var x -> Retypeops.relevance_of_var env x + else Relevanceops.relevance_of_rel env (n - len) + | Var x -> Relevanceops.relevance_of_var env x | Sort _ -> Sorts.Relevant | Cast (c, _, _) -> aux rels c | Prod ({binder_relevance=r}, _, codom) -> @@ -284,13 +284,13 @@ let relevance_of_term env sigma c = | LetIn ({binder_relevance=r}, _, _, bdy) -> aux (Range.cons r rels) bdy | App (c, _) -> aux rels c - | Const (c,_) -> Retypeops.relevance_of_constant env c + | Const (c,_) -> Relevanceops.relevance_of_constant env c | Ind _ -> Sorts.Relevant - | Construct (c,_) -> Retypeops.relevance_of_constructor env c + | Construct (c,_) -> Relevanceops.relevance_of_constructor env c | Case (ci, _, _, _) -> ci.ci_relevance | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance - | Proj (p, _) -> Retypeops.relevance_of_projection env p + | Proj (p, _) -> Relevanceops.relevance_of_projection env p | Int _ | Float _ -> Sorts.Relevant | Meta _ | Evar _ -> Sorts.Relevant diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 19d4ed91e6..d8f7b7eed8 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -37,6 +37,7 @@ val pf_unsafe_type_of : Goal.goal sigma -> constr -> types [@@ocaml.deprecated "Use [type_of] or retyping according to your needs."] val pf_type_of : Goal.goal sigma -> constr -> evar_map * types val pf_hnf_type_of : Goal.goal sigma -> constr -> types +[@@ocaml.deprecated "This is a no-op now"] val pf_get_hyp : Goal.goal sigma -> Id.t -> named_declaration val pf_get_hyp_typ : Goal.goal sigma -> Id.t -> types @@ -49,22 +50,33 @@ val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) -> val pf_reduce : (env -> evar_map -> constr -> constr) -> Goal.goal sigma -> constr -> constr +[@@ocaml.deprecated "Use the version in Tacmach.New"] + val pf_e_reduce : (env -> evar_map -> constr -> evar_map * constr) -> Goal.goal sigma -> constr -> evar_map * constr +[@@ocaml.deprecated "Use the version in Tacmach.New"] val pf_whd_all : Goal.goal sigma -> constr -> constr +[@@ocaml.deprecated "Use the version in Tacmach.New"] val pf_hnf_constr : Goal.goal sigma -> constr -> constr +[@@ocaml.deprecated "Use the version in Tacmach.New"] val pf_nf : Goal.goal sigma -> constr -> constr +[@@ocaml.deprecated "Use the version in Tacmach.New"] val pf_nf_betaiota : Goal.goal sigma -> constr -> constr val pf_reduce_to_quantified_ind : Goal.goal sigma -> types -> (inductive * EInstance.t) * types val pf_reduce_to_atomic_ind : Goal.goal sigma -> types -> (inductive * EInstance.t) * types +[@@ocaml.deprecated "Use Tacred.pf_reduce_to_atomic_ind"] val pf_compute : Goal.goal sigma -> constr -> constr +[@@ocaml.deprecated "Use the version in Tacmach.New"] val pf_unfoldn : (occurrences * evaluable_global_reference) list -> Goal.goal sigma -> constr -> constr +[@@ocaml.deprecated "Use Tacred.unfoldn"] val pf_const_value : Goal.goal sigma -> pconstant -> constr +[@@ocaml.deprecated "Use Environ.constant_value_in"] val pf_conv_x : Goal.goal sigma -> constr -> constr -> bool +[@@ocaml.deprecated "Use the version in Tacmach.New"] (** {6 Pretty-printing functions (debug only). } *) val pr_gls : Goal.goal sigma -> Pp.t diff --git a/theories/micromega/ZifyPow.v b/theories/micromega/ZifyPow.v new file mode 100644 index 0000000000..d208696c0f --- /dev/null +++ b/theories/micromega/ZifyPow.v @@ -0,0 +1 @@ +Require Export ZifyInst. |