diff options
27 files changed, 150 insertions, 92 deletions
diff --git a/.github/SUPPORT.md b/.github/SUPPORT.md index b6f2e942e9..978f011f23 100644 --- a/.github/SUPPORT.md +++ b/.github/SUPPORT.md @@ -1,28 +1,22 @@ -# Support # +[![Zulip][zulip-badge]][zulip-link] +[![Discourse][discourse-badge]][discourse-link] + +[discourse-badge]: https://img.shields.io/badge/Discourse-forum-informational.svg +[discourse-link]: https://coq.discourse.group/ -Get in touch with the user community and ask questions about Coq on -our [Discourse forum][]. Posts in other languages than English are -explicitly welcome there. There is also a historic mailing list called -the [Coq-Club][] which has lots of subscribers, and an IRC channel -(`irc://irc.freenode.net/#coq`). +[zulip-badge]: https://img.shields.io/badge/Zulip-chat-informational.svg +[zulip-link]: https://coq.zulipchat.com/ + +# Support # -In addition, you may also ask questions about Coq on [Stack -Overflow][] (use the tag [coq][Stack Overflow tag]) or on the -meta-theory of Coq on the [TCS Stack Exchange][] (which also has a -[coq][TCS SE tag] tag). +<!-- content copied verbatim from "Questions and discussion" in README.md --> -You can reach the Coq development team through the [development -category][] of the above mentioned Discourse forum, the [Gitter -channel][], and of course the bug tracker. +We have a number of channels to reach the user community and the +development team: -See also [coq.inria.fr/community](https://coq.inria.fr/community.html). +- Our [Zulip chat][zulip-link], for casual and high traffic discussions. +- Our [Discourse forum][discourse-link], for more structured and easily browsable discussions and Q&A. +- Our historical mailing list, the [Coq-Club](https://sympa.inria.fr/sympa/info/coq-club). -[Discourse forum]: https://coq.discourse.group -[Coq-Club]: https://sympa.inria.fr/sympa/arc/coq-club -[Stack Overflow]: https://stackoverflow.com -[Stack Overflow tag]: https://stackoverflow.com/questions/tagged/coq -[TCS Stack Exchange]: https://cstheory.stackexchange.com/ -[TCS SE tag]: https://cstheory.stackexchange.com/questions/tagged/coq -[development category]: https://coq.discourse.group/c/coq-development -[Gitter channel]: https://gitter.im/coq/coq -[bug tracker]: https://github.com/coq/coq/issues +See also [coq.inria.fr/community](https://coq.inria.fr/community.html), which +lists several other active platforms. diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index fae2c64484..87101ecae7 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -366,12 +366,11 @@ pkg:opam: dependencies: [] script: - set -e - - opam pin add --kind=path coq.$COQ_VERSION . - - opam pin add --kind=path coqide-server.$COQ_VERSION . - - opam pin add --kind=path coqide.$COQ_VERSION . + - opam pin add --kind=path coq.dev . + - opam pin add --kind=path coqide-server.dev . + - opam pin add --kind=path coqide.dev . - set +e variables: - COQ_VERSION: "8.13" OPAM_SWITCH: "edge" OPAM_VARIANT: "+flambda" only: *full-ci @@ -699,6 +698,9 @@ library:ci-coquelicot: library:ci-cross_crypto: extends: .ci-template +library:ci-engine_bench: + extends: .ci-template + library:ci-fcsl_pcm: extends: .ci-template diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md index 0720cf6210..0d8751de7e 100644 --- a/CODE_OF_CONDUCT.md +++ b/CODE_OF_CONDUCT.md @@ -11,7 +11,7 @@ Their goal is that everyone feels safe and welcome when contributing to Coq or interacting with others in Coq related forums. These rules apply to all spaces managed by the Coq development team. -This includes the GitHub repository, the mailing lists, the Gitter channel, +This includes the GitHub repository, the Discourse forum, the Zulip chat, the mailing lists, physical events like Coq working groups and workshops, and any other forums created or managed by the development team which the community uses for communication. In addition, violations of these rules outside these spaces may diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 525ced7fee..8a09e43c94 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -179,7 +179,8 @@ Learn how to write a Coq plugin, and about best practices, in the Coq progress, so do not hesitate to expand it, or ask questions. If you want quick feedback on best practices, or how to talk to the -Coq API, a good place to hang out is the Coq [Gitter channel][Gitter]. +Coq API, a good place to hang out is the [Coq devs & plugin devs +stream][Zulip-dev] of our Zulip chat. Finally, we strongly encourage authors of plugins to submit their plugins to join Coq's continuous integration (CI) early on. Indeed, @@ -285,7 +286,7 @@ GitHub account). You can file a bug for any of the following: It would help if you search the existing issues before reporting a bug. This can be difficult, so consider it extra credit. We don't mind duplicate bug reports. If unsure, you are always very welcome to -ask on our [Discourse forum][Discourse] or [Gitter chat][Gitter] +ask on our [Discourse forum][Discourse] or [Zulip chat][Zulip] before, after, or while writing a bug report. It is better if you can test that your bug is still present in the @@ -364,7 +365,7 @@ Being in this team will grant you the following access: idea for a new feature). - **Creating new labels:** if you feel a `part:` label is missing, do not hesitate to create it. If you are not sure, you may discuss it - with other contributors and developers on [Gitter][] first. + with other contributors and developers on [Zulip][Zulip-dev] first. - **Closing issues:** if a bug cannot be reproduced anymore, is a duplicate, or should not be considered a bug report in the first place, you should close it. When doing so, try putting an @@ -1133,7 +1134,7 @@ before a change is ready on your side. When opening a draft PR, make sure to give it a descriptive enough title so that interested developers still notice it in their notification feed. You may also advertise it by talking about it in -our [developer chat][Gitter]. If you know which developer would be +our [developer chat][Zulip-dev]. If you know which developer would be able to provide useful feedback to you, you may also ping them. ###### Turning a PR into draft mode ###### @@ -1182,8 +1183,9 @@ documentation is still a work-in-progress. ### Online forum and chat to talk to developers ### We have a [Discourse forum][Discourse] (see in particular the [Coq -development category][Discourse-development-category]) and a [Gitter -chat][Gitter]. Feel free to join any of them and ask questions. +development][Discourse-development-category] category) and a [Zulip +chat][Zulip] (see in particular the [Coq devs & plugin devs][Zulip-dev] +stream). Feel free to join any of them and ask questions. People are generally happy to help and very reactive. Obviously, the issue tracker is also a good place to ask questions, @@ -1267,7 +1269,6 @@ can be found [on the wiki][wiki-CUDW]. [GitHub-wiki-extensions]: https://help.github.com/en/articles/editing-wiki-content [GitLab-coq]: https://gitlab.com/coq [GitLab-doc]: https://docs.gitlab.com/ -[Gitter]: https://gitter.im/coq/coq [JasonGross-coq-tools]: https://github.com/JasonGross/coq-tools [jenkins-doc]: https://github.com/coq/coq/wiki/Jenkins-(automated-benchmarking) [kind-documentation]: https://github.com/coq/coq/issues?q=is%3Aopen+is%3Aissue+label%3A%22kind%3A+documentation%22 @@ -1311,3 +1312,5 @@ can be found [on the wiki][wiki-CUDW]. [wiki-CUDW]: https://github.com/coq/coq/wiki/CoqImplementorsWorkshop [wiki-WG]: https://github.com/coq/coq/wiki/Coq-Working-Groups [YouTube]: https://www.youtube.com/channel/UCbJo6gYYr0OF18x01M4THdQ +[Zulip]: https://coq.zulipchat.com +[Zulip-dev]: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs diff --git a/Makefile.ci b/Makefile.ci index af92d476ba..9b7008f765 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -23,6 +23,7 @@ CI_TARGETS= \ ci-coq_tools \ ci-coqprime \ ci-elpi \ + ci-engine_bench \ ci-ext_lib \ ci-equations \ ci-fcsl_pcm \ @@ -2,7 +2,8 @@ [![GitLab][gitlab-badge]][gitlab-link] [![Azure Pipelines][azure-badge]][azure-link] -[![Gitter][gitter-badge]][gitter-link] +[![Zulip][zulip-badge]][zulip-link] +[![Discourse][discourse-badge]][discourse-link] [![DOI][doi-badge]][doi-link] [gitlab-badge]: https://gitlab.com/coq/coq/badges/master/pipeline.svg @@ -11,8 +12,11 @@ [azure-badge]: https://dev.azure.com/coq/coq/_apis/build/status/coq.coq?branchName=master [azure-link]: https://dev.azure.com/coq/coq/_build/latest?definitionId=1?branchName=master -[gitter-badge]: https://badges.gitter.im/coq/coq.svg -[gitter-link]: https://gitter.im/coq/coq +[discourse-badge]: https://img.shields.io/badge/Discourse-forum-informational.svg +[discourse-link]: https://coq.discourse.group/ + +[zulip-badge]: https://img.shields.io/badge/Zulip-chat-informational.svg +[zulip-link]: https://coq.zulipchat.com/ [doi-badge]: https://zenodo.org/badge/DOI/10.5281/zenodo.1003420.svg [doi-link]: https://doi.org/10.5281/zenodo.1003420 @@ -102,12 +106,12 @@ approach some problems you may encounter. We have a number of channels to reach the user community and the development team: -- Our [Discourse forum](https://coq.discourse.group). -- Our mailing list, the [Coq-Club](https://sympa.inria.fr/sympa/info/coq-club). -- Our [Gitter channel][gitter-link], which is a good way to reach - developers for quick chat and development questions. +- Our [Zulip chat][zulip-link], for casual and high traffic discussions. +- Our [Discourse forum][discourse-link], for more structured and easily browsable discussions and Q&A. +- Our historical mailing list, the [Coq-Club](https://sympa.inria.fr/sympa/info/coq-club). -See also [coq.inria.fr/community](https://coq.inria.fr/community.html). +See also [coq.inria.fr/community](https://coq.inria.fr/community.html), which +lists several other active platforms. ## Bug reports diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index d5c6096100..801e29ac95 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -179,6 +179,11 @@ but if you wish to save more time you can skip the job by setting This means you will need to change its value when the Docker image needs to be updated. You can do so for a single pipeline by starting -it through the web interface. +it through the web interface. Here is a direct link that you can use +to trigger such a build: +`https://gitlab.com/coq/coq/pipelines/new?var[SKIP_DOCKER]=false&ref=pr-XXXXX`. +Note that this link will give a 404 error if you are not logged in or +a member of the Coq organization on GitLab. To request to join the +Coq organization, go to https://gitlab.com/coq to request access. See also [`docker/README.md`](docker/README.md). diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 5f7d0b5789..19ba9de245 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -239,6 +239,13 @@ : "${elpi_hb_CI_ARCHIVEURL:=${elpi_hb_CI_GITURL}/archive}" ######################################################################## +# Engine-Bench +######################################################################## +: "${engine_bench_CI_REF:=master}" +: "${engine_bench_CI_GITURL:=https://github.com/mit-plv/engine-bench}" +: "${engine_bench_CI_ARCHIVEURL:=${engine_bench_CI_GITURL}/archive}" + +######################################################################## # fcsl-pcm ######################################################################## : "${fcsl_pcm_CI_REF:=master}" diff --git a/dev/ci/ci-engine_bench.sh b/dev/ci/ci-engine_bench.sh new file mode 100755 index 0000000000..fda7649f88 --- /dev/null +++ b/dev/ci/ci-engine_bench.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download engine_bench + +( cd "${CI_BUILD_DIR}/engine_bench" && make coq && make coq-perf-Sanity ) diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index ce64aebdc7..82e4bd1e1e 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -49,10 +49,26 @@ ask_confirmation() { fi } +curl_paginate_array() { + # as per https://developer.github.com/v3/guides/traversing-with-pagination/#changing-the-number-of-items-received, GitHub will never give us more than 100 + url="$1?per_page=100" + # we keep fetching pages until the response is below the per-page limit (possibly 0 elements) + page=1 + while true; do + response="$(curl -s "${url}&page=${page}")" + echo "${response}" + if [ "$(jq 'length' <<< "$response")" -lt 100 ]; then # done + break + fi + page=$(($page + 1)) + done | jq '[.[]]' # we concatenate the arrays +} + check_util jq check_util curl check_util git check_util gpg +check_util grep # command line parsing @@ -70,6 +86,8 @@ fi # Fetching PR metadata +# The main API call returns a dict/object, not an array, so we don't +# bother paginating PRDATA=$(curl -s "$API/pulls/$PR") TITLE=$(echo "$PRDATA" | jq -r '.title') @@ -203,7 +221,7 @@ fi # Generate commit message info "Fetching review data" -reviews=$(curl -s "$API/pulls/$PR/reviews") +reviews=$(curl_paginate_array "$API/pulls/$PR/reviews") msg="Merge PR #$PR: $TITLE" has_state() { diff --git a/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst b/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst new file mode 100644 index 0000000000..5b35090d7e --- /dev/null +++ b/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst @@ -0,0 +1,5 @@ +- **Changed:** + :cmd:Redirect now obeys the :opt:`Printing Width` and + :opt:`Printing Depth` flags. + (`#12358 <https://github.com/coq/coq/pull/12358>`_, + by Emilio Jesus Gallego Arias). diff --git a/engine/evd.ml b/engine/evd.ml index 5642145f6d..ff13676818 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -697,8 +697,7 @@ let empty = { extras = Store.empty; } -let from_env e = - { empty with universes = UState.make ~lbound:(Environ.universes_lbound e) (Environ.universes e) } +let from_env e = { empty with universes = UState.from_env e } let from_ctx ctx = { empty with universes = ctx } @@ -862,9 +861,6 @@ let universe_subst evd = let merge_context_set ?loc ?(sideff=false) rigid evd ctx' = {evd with universes = UState.merge ?loc ~sideff rigid evd.universes ctx'} -let merge_universe_subst evd subst = - {evd with universes = UState.merge_subst evd.universes subst } - let with_context_set ?loc rigid d (a, ctx) = (merge_context_set ?loc rigid d ctx, a) diff --git a/engine/evd.mli b/engine/evd.mli index c6c4a71b22..d9b7bd76e7 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -636,7 +636,6 @@ val merge_universe_context : evar_map -> UState.t -> evar_map val set_universe_context : evar_map -> UState.t -> evar_map val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map -val merge_universe_subst : evar_map -> UnivSubst.universe_opt_subst -> evar_map val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a diff --git a/engine/uState.ml b/engine/uState.ml index 99ac5f2ce8..7c60d8317c 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -63,6 +63,8 @@ let make ~lbound u = uctx_universes_lbound = lbound; uctx_initial_universes = u} +let from_env e = make ~lbound:(Environ.universes_lbound e) (Environ.universes e) + let is_empty ctx = ContextSet.is_empty ctx.uctx_local && LMap.is_empty ctx.uctx_univ_variables diff --git a/engine/uState.mli b/engine/uState.mli index 533a501b59..45a0f9964e 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -29,6 +29,8 @@ val make : lbound:UGraph.Bound.t -> UGraph.t -> t val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t +val from_env : Environ.env -> t + val is_empty : t -> bool val union : t -> t -> t diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache.test-suite Binary files differindex 046cb067c5..046cb067c5 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache.test-suite diff --git a/test-suite/Makefile b/test-suite/Makefile index f0f838680e..5dd4f42af3 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -117,7 +117,11 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \ # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS) -PREREQUISITELOG = $(addsuffix .log,$(wildcard prerequisite/*.v)) +.csdp.cache: .csdp.cache.test-suite + cp $< $@ + chmod u+w $@ + +PREREQUISITELOG = $(addsuffix .log,$(wildcard prerequisite/*.v)) .csdp.cache ####################################################################### # Phony targets @@ -470,6 +474,7 @@ approve-output: output output-coqtop output/MExtraction.out: ../plugins/micromega/micromega.ml $(SHOW) GEN $@ $(HIDE) cp $< $@ + $(HIDE) chmod u+w $@ $(HIDE) echo >> $@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index 30be5e6456..ab89e12592 100755 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh @@ -9,10 +9,18 @@ cd _test || exit 1 mkdir -p src mkdir -p theories/sub -cp ../../template/theories/sub/testsub.v theories/sub -cp ../../template/theories/test.v theories -cp ../../template/src/test.mlg src -cp ../../template/src/test_aux.mli src -cp ../../template/src/test.mli src -cp ../../template/src/test_plugin.mlpack src -cp ../../template/src/test_aux.ml src +cp_file() { + local _TARGET=$1 + cp ../../template/$_TARGET $_TARGET + chmod u+w $_TARGET +} + +# We chmod +w as to fix the case where the sources are read-only, as +# for example when using Dune's cache. +cp_file theories/sub/testsub.v +cp_file theories/test.v +cp_file src/test.mlg +cp_file src/test_aux.mli +cp_file src/test.mli +cp_file src/test_plugin.mlpack +cp_file src/test_aux.ml diff --git a/test-suite/misc/redirect_printing.out b/test-suite/misc/redirect_printing.out new file mode 100644 index 0000000000..4f45c4d4c2 --- /dev/null +++ b/test-suite/misc/redirect_printing.out @@ -0,0 +1,2 @@ +nat_ind + : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n diff --git a/test-suite/misc/redirect_printing.sh b/test-suite/misc/redirect_printing.sh new file mode 100755 index 0000000000..7da17407f3 --- /dev/null +++ b/test-suite/misc/redirect_printing.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +$coqc misc/redirect_printing.v +diff -u redirect_test.out misc/redirect_printing.out diff --git a/test-suite/misc/redirect_printing.v b/test-suite/misc/redirect_printing.v new file mode 100644 index 0000000000..2f9096bcb8 --- /dev/null +++ b/test-suite/misc/redirect_printing.v @@ -0,0 +1,2 @@ +Set Printing Width 999999. +Redirect "redirect_test" Check nat_ind. diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 5323c9f1c6..bb640a83f6 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -385,7 +385,7 @@ let build_beq_scheme mode kn = Vars.substl subst cores.(i) in create_input fix), - UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())) + UState.from_env (Global.env ())) let beq_scheme_kind = declare_mutual_scheme_object "_beq" @@ -707,7 +707,7 @@ let make_bl_scheme mode mind = let lnonparrec,lnamesparrec = (* TODO subst *) context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal = compute_bl_goal ind lnamesparrec nparrec in - let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let uctx = UState.from_env (Global.env ()) in let side_eff = side_effect_of_mode mode in let bl_goal = EConstr.of_constr bl_goal in let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal @@ -840,7 +840,7 @@ let make_lb_scheme mode mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal = compute_lb_goal ind lnamesparrec nparrec in - let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let uctx = UState.from_env (Global.env ()) in let side_eff = side_effect_of_mode mode in let lb_goal = EConstr.of_constr lb_goal in let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal @@ -1010,7 +1010,7 @@ let make_eq_decidability mode mind = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let u = Univ.Instance.empty in - let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let uctx = UState.from_env (Global.env ()) in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let side_eff = side_effect_of_mode mode in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index eac8f92e2e..d56917271c 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -126,7 +126,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in + let term, ty, uctx, obls = Declare.prepare_obligation ~name ~body ~types evd in let _ : Declare.Obls.progress = Obligations.add_definition ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls diff --git a/vernac/declare.ml b/vernac/declare.ml index c291890dce..333b186b22 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1007,25 +1007,20 @@ let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry -let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = +let prepare_obligation ~name ~types ~body sigma = + let env = Global.env () in + let types = match types with + | Some t -> t + | None -> Retyping.get_type_of env sigma body + in let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false - sigma (fun nf -> nf body, Option.map nf types) + sigma (fun nf -> nf body, nf types) in - let univs = Evd.check_univ_decl ~poly sigma udecl in - let ce = definition_entry ?opaque ?inline ?types ~univs body in - let env = Global.env () in - let (c,ctx), sideff = Future.force ce.proof_entry_body in - assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private); - assert(Univ.ContextSet.is_empty ctx); RetrieveObl.check_evars env sigma; - let c = EConstr.of_constr c in - let typ = match ce.proof_entry_type with - | Some t -> EConstr.of_constr t - | None -> Retyping.get_type_of env sigma c - in - let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in + let body, types = EConstr.(of_constr body, of_constr types) in + let obls, _, body, cty = RetrieveObl.retrieve_obligations env name sigma 0 body types in let uctx = Evd.evar_universe_context sigma in - c, cty, uctx, obls + body, cty, uctx, obls let prepare_parameter ~poly ~udecl ~types sigma = let env = Global.env () in @@ -1641,7 +1636,7 @@ let obligation_terminator entries uctx {name; num; auto} = universes and constraints if any *) defined then - UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) + UState.from_env (Global.env ()) else uctx in update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto @@ -1673,9 +1668,7 @@ let obligation_admitted_terminator {name; num; auto} ctx' dref = if not prg.prg_poly (* Not polymorphic *) then (* The universe context was declared globally, we continue from the new global environment. *) - let ctx = - UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) - in + let ctx = UState.from_env (Global.env ()) in let ctx' = UState.merge_subst ctx (UState.subst ctx') in (Univ.Instance.empty, ctx') else diff --git a/vernac/declare.mli b/vernac/declare.mli index 82b0cff8d9..62bc6a34bf 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -367,11 +367,7 @@ val declare_mutually_recursive (** Prepare API, to be removed once we provide the corresponding 1-step API *) val prepare_obligation - : ?opaque:bool - -> ?inline:bool - -> name:Id.t - -> poly:bool - -> udecl:UState.universe_decl + : name:Id.t -> types:EConstr.t option -> body:EConstr.t -> Evd.evar_map diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 5fdee9f2d4..bbc20d5e30 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -191,10 +191,9 @@ and solve_obligation_by_tac prg obls i tac = obls.(i) <- obl'; if def && not prg.prg_poly then ( (* Declare the term constraints with the first obligation only *) - let evd = Evd.from_env (Global.env ()) in - let evd = Evd.merge_universe_subst evd (UState.subst ctx) in - let ctx' = Evd.evar_universe_context evd in - Some (ProgramDecl.set_uctx ~uctx:ctx' prg)) + let uctx = UState.from_env (Global.env ()) in + let uctx = UState.merge_subst uctx (UState.subst ctx) in + Some (ProgramDecl.set_uctx ~uctx prg)) else Some prg else None diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 2d8734ff7f..a28d8f605b 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -404,6 +404,7 @@ let with_output_to_file fname func input = let channel = open_out (String.concat "." [fname; "out"]) in let old_fmt = !std_ft, !err_ft, !deep_ft in let new_ft = Format.formatter_of_out_channel channel in + set_gp new_ft (get_gp !std_ft); std_ft := new_ft; err_ft := new_ft; deep_ft := new_ft; @@ -412,6 +413,7 @@ let with_output_to_file fname func input = std_ft := Util.pi1 old_fmt; err_ft := Util.pi2 old_fmt; deep_ft := Util.pi3 old_fmt; + Format.pp_print_flush new_ft (); close_out channel; output with reraise -> @@ -419,6 +421,7 @@ let with_output_to_file fname func input = std_ft := Util.pi1 old_fmt; err_ft := Util.pi2 old_fmt; deep_ft := Util.pi3 old_fmt; + Format.pp_print_flush new_ft (); close_out channel; Exninfo.iraise reraise |