diff options
80 files changed, 519 insertions, 294 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 fc0cdebcf0..87101ecae7 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,7 +18,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2020-05-18-V3" + CACHEKEY: "bionic_coq-V2020-05-19-V33" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -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/.ocamlformat b/.ocamlformat index 62e609fb55..a0d4ef6bbb 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,4 +1,4 @@ -version=0.14.0 +version=0.14.2 profile=ocamlformat # to enable a whole directory, put "disable=false" in dir/.ocamlformat @@ -11,4 +11,4 @@ cases-exp-indent=2 field-space=loose exp-grouping=preserve break-cases=fit -doc-comments-val=before +doc-comments=before 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/checker/check.ml b/checker/check.ml index 6d307b3c5e..1ff1425dea 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -119,11 +119,12 @@ let check_one_lib admit senv (dir,m) = if LibrarySet.mem dir admit then (Flags.if_verbose Feedback.msg_notice (str "Admitting library: " ++ pr_dirpath dir); - Safe_checking.unsafe_import senv md m.library_extra_univs dig) + Safe_checking.unsafe_import (fst senv) md m.library_extra_univs dig), + (snd senv) else (Flags.if_verbose Feedback.msg_notice (str "Checking library: " ++ pr_dirpath dir); - Safe_checking.import senv md m.library_extra_univs dig) + Safe_checking.import (fst senv) (snd senv) md m.library_extra_univs dig) in register_loaded_library m; senv @@ -435,6 +436,6 @@ let recheck_library senv ~norec ~admit ~check = Flags.if_verbose Feedback.msg_notice (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++ prlist (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed)); - let senv = List.fold_left (check_one_lib nochk) senv needed in + let senv = List.fold_left (check_one_lib nochk) (senv, Cmap.empty) needed in Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked"); senv diff --git a/checker/check.mli b/checker/check.mli index bb19f09d2e..93274204a3 100644 --- a/checker/check.mli +++ b/checker/check.mli @@ -30,4 +30,4 @@ val add_load_path : physical_path * logical_path -> unit val recheck_library : safe_environment -> norec:object_file list -> admit:object_file list -> - check:object_file list -> safe_environment + check:object_file list -> safe_environment * Cset.t Cmap.t diff --git a/checker/check_stat.ml b/checker/check_stat.ml index ee7170df48..0a2da7435c 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -38,8 +38,14 @@ let pr_assumptions ass axs = else hv 2 (str ass ++ str ":" ++ fnl() ++ prlist_with_sep fnl str axs) -let pr_axioms env = - let csts = fold_constants (fun c cb acc -> if not (Declareops.constant_has_body cb) then Constant.to_string c :: acc else acc) env [] in +let pr_axioms env opac = + let add c cb acc = + if Declareops.constant_has_body cb then acc else + match Cmap.find_opt c opac with + | None -> Cset.add c acc + | Some s -> Cset.union s acc in + let csts = fold_constants add env Cset.empty in + let csts = Cset.fold (fun c acc -> Constant.to_string c :: acc) csts [] in pr_assumptions "Axioms" csts let pr_type_in_type env = @@ -56,20 +62,20 @@ let pr_nonpositive env = let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in pr_assumptions "Inductives whose positivity is assumed" inds -let print_context env = +let print_context env opac = if !output_context then begin Feedback.msg_notice (hov 0 (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++ str"===============" ++ fnl() ++ fnl() ++ str "* " ++ hov 0 (pr_engagement env ++ fnl()) ++ fnl() ++ - str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++ + str "* " ++ hov 0 (pr_axioms env opac ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_nonpositive env ++ fnl())) ) end -let stats env = - print_context env; +let stats env opac = + print_context env opac; print_memory_stat () diff --git a/checker/check_stat.mli b/checker/check_stat.mli index 8796bcda76..987d50b469 100644 --- a/checker/check_stat.mli +++ b/checker/check_stat.mli @@ -10,4 +10,4 @@ val memory_stat : bool ref val output_context : bool ref -val stats : Environ.env -> unit +val stats : Environ.env -> Names.Cset.t Names.Cmap.t -> unit diff --git a/checker/checker.ml b/checker/checker.ml index 0522d43417..086acc482c 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -407,6 +407,6 @@ let run senv = let start () = let senv = init() in - let senv = run senv in - Check_stat.stats (Safe_typing.env_of_safe_env senv); + let senv, opac = run senv in + Check_stat.stats (Safe_typing.env_of_safe_env senv) opac; exit 0 diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 2f795ff8d9..999f44bf1d 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -15,7 +15,25 @@ let indirect_accessor = ref { let set_indirect_accessor f = indirect_accessor := f -let check_constant_declaration env kn cb = +let register_opacified_constant env opac kn cb = + let rec gather_consts s c = + match Constr.kind c with + | Constr.Const (c, _) -> Cset.add c s + | _ -> Constr.fold gather_consts s c + in + let wo_body = + Cset.fold + (fun kn s -> + if Declareops.constant_has_body (lookup_constant kn env) then s else + match Cmap.find_opt kn opac with + | None -> Cset.add kn s + | Some s' -> Cset.union s' s) + (gather_consts Cset.empty cb) + Cset.empty + in + Cmap.add kn wo_body opac + +let check_constant_declaration env opac kn cb opacify = Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ Constant.print kn); let env = CheckFlags.set_local_flags cb.const_typing_flags env in let poly, env = @@ -54,11 +72,13 @@ let check_constant_declaration env kn cb = with NotConvertible -> Type_errors.error_actual_type env j ty) | None -> () in - () + match body with + | Some body when opacify -> register_opacified_constant env opac kn body + | Some _ | None -> opac -let check_constant_declaration env kn cb = - let () = check_constant_declaration env kn cb in - Environ.add_constant kn cb env +let check_constant_declaration env opac kn cb opacify = + let opac = check_constant_declaration env opac kn cb opacify in + Environ.add_constant kn cb env, opac (** {6 Checking modules } *) @@ -80,18 +100,32 @@ let mk_mtb mp sign delta = mod_delta = delta; mod_retroknowledge = ModTypeRK; } -let rec check_module env mp mb = +let collect_constants_without_body sign mp = + let collect_sf s lab = function + | SFBconst cb -> + let c = Constant.make2 mp lab in + if Declareops.constant_has_body cb then s else Cset.add c s + | SFBmind _ | SFBmodule _ | SFBmodtype _ -> s in + match sign with + | MoreFunctor _ -> Cset.empty (* currently ignored *) + | NoFunctor struc -> + List.fold_left (fun s (lab,mb) -> collect_sf s lab mb) Cset.empty struc + +let rec check_module env opac mp mb = Flags.if_verbose Feedback.msg_notice (str " checking module: " ++ str (ModPath.to_string mp)); let env = Modops.add_retroknowledge mb.mod_retroknowledge env in - let (_:module_signature) = - check_signature env mb.mod_type mb.mod_mp mb.mod_delta + let sign, opac = + check_signature env opac mb.mod_type mb.mod_mp mb.mod_delta Cset.empty in - let optsign = match mb.mod_expr with - |Struct sign -> Some (check_signature env sign mb.mod_mp mb.mod_delta, mb.mod_delta) - |Algebraic me -> Some (check_mexpression env me mb.mod_mp mb.mod_delta) - |Abstract|FullStruct -> None + let optsign, opac = match mb.mod_expr with + |Struct sign_struct -> + let opacify = collect_constants_without_body sign mb.mod_mp in + let sign, opac = check_signature env opac sign_struct mb.mod_mp mb.mod_delta opacify in + Some (sign, mb.mod_delta), opac + |Algebraic me -> Some (check_mexpression env opac me mb.mod_mp mb.mod_delta), opac + |Abstract|FullStruct -> None, opac in - match optsign with + let () = match optsign with |None -> () |Some (sign,delta) -> let mtb1 = mk_mtb mp sign delta @@ -100,35 +134,37 @@ let rec check_module env mp mb = let cu = Subtyping.check_subtypes env mtb1 mtb2 in if not (Environ.check_constraints cu env) then CErrors.user_err Pp.(str "Incorrect universe constraints for module subtyping"); + in + opac and check_module_type env mty = Flags.if_verbose Feedback.msg_notice (str " checking module type: " ++ str (ModPath.to_string mty.mod_mp)); - let (_:module_signature) = - check_signature env mty.mod_type mty.mod_mp mty.mod_delta in + let (_:module_signature), _ = + check_signature env Cmap.empty mty.mod_type mty.mod_mp mty.mod_delta Cset.empty in () -and check_structure_field env mp lab res = function +and check_structure_field env opac mp lab res opacify = function | SFBconst cb -> let c = Constant.make2 mp lab in - check_constant_declaration env c cb + check_constant_declaration env opac c cb (Cset.mem c opacify) | SFBmind mib -> let kn = KerName.make mp lab in let kn = Mod_subst.mind_of_delta_kn res kn in - CheckInductive.check_inductive env kn mib + CheckInductive.check_inductive env kn mib, opac | SFBmodule msb -> - let () = check_module env (MPdot(mp,lab)) msb in - Modops.add_module msb env + let opac = check_module env opac (MPdot(mp,lab)) msb in + Modops.add_module msb env, opac | SFBmodtype mty -> check_module_type env mty; - add_modtype mty env + add_modtype mty env, opac -and check_mexpr env mse mp_mse res = match mse with +and check_mexpr env opac mse mp_mse res = match mse with | MEident mp -> let mb = lookup_module mp env in let mb = Modops.strengthen_and_subst_mb mb mp_mse false in mb.mod_type, mb.mod_delta | MEapply (f,mp) -> - let sign, delta = check_mexpr env f mp_mse res in + let sign, delta = check_mexpr env opac f mp_mse res in let farg_id, farg_b, fbody_b = Modops.destr_functor sign in let mtb = Modops.module_type_of_module (lookup_module mp env) in let cu = Subtyping.check_subtypes env mtb farg_b in @@ -139,22 +175,22 @@ and check_mexpr env mse mp_mse res = match mse with | MEwith _ -> CErrors.user_err Pp.(str "Unsupported 'with' constraint in module implementation") -and check_mexpression env sign mp_mse res = match sign with +and check_mexpression env opac sign mp_mse res = match sign with | MoreFunctor (arg_id, mtb, body) -> check_module_type env mtb; let env' = Modops.add_module_type (MPbound arg_id) mtb env in - let body, delta = check_mexpression env' body mp_mse res in + let body, delta = check_mexpression env' opac body mp_mse res in MoreFunctor(arg_id,mtb,body), delta - | NoFunctor me -> check_mexpr env me mp_mse res + | NoFunctor me -> check_mexpr env opac me mp_mse res -and check_signature env sign mp_mse res = match sign with +and check_signature env opac sign mp_mse res opacify = match sign with | MoreFunctor (arg_id, mtb, body) -> check_module_type env mtb; let env' = Modops.add_module_type (MPbound arg_id) mtb env in - let body = check_signature env' body mp_mse res in - MoreFunctor(arg_id,mtb,body) + let body, opac = check_signature env' opac body mp_mse res Cset.empty in + MoreFunctor(arg_id,mtb,body), opac | NoFunctor struc -> - let (_:env) = List.fold_left (fun env (lab,mb) -> - check_structure_field env mp_mse lab res mb) env struc + let (_:env), opac = List.fold_left (fun (env, opac) (lab,mb) -> + check_structure_field env opac mp_mse lab res opacify mb) (env, opac) struc in - NoFunctor struc + NoFunctor struc, opac diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli index 58eb135b50..194f6c6e16 100644 --- a/checker/mod_checking.mli +++ b/checker/mod_checking.mli @@ -10,4 +10,4 @@ val set_indirect_accessor : Opaqueproof.indirect_accessor -> unit -val check_module : Environ.env -> Names.ModPath.t -> Declarations.module_body -> unit +val check_module : Environ.env -> Names.Cset.t Names.Cmap.t -> Names.ModPath.t -> Declarations.module_body -> Names.Cset.t Names.Cmap.t diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml index b5beab532e..55bfa36ce5 100644 --- a/checker/safe_checking.ml +++ b/checker/safe_checking.ml @@ -11,14 +11,14 @@ open Declarations open Environ -let import senv clib univs digest = +let import senv opac clib univs digest = let mb = Safe_typing.module_of_library clib in let env = Safe_typing.env_of_safe_env senv in let env = push_context_set ~strict:true (Safe_typing.univs_of_library clib) env in let env = push_context_set ~strict:true univs env in let env = Modops.add_retroknowledge mb.mod_retroknowledge env in - Mod_checking.check_module env mb.mod_mp mb; - let (_,senv) = Safe_typing.import clib univs digest senv in senv + let opac = Mod_checking.check_module env opac mb.mod_mp mb in + let (_,senv) = Safe_typing.import clib univs digest senv in senv, opac let unsafe_import senv clib univs digest = let (_,senv) = Safe_typing.import clib univs digest senv in senv diff --git a/checker/safe_checking.mli b/checker/safe_checking.mli index 21566555d4..b4abc52a74 100644 --- a/checker/safe_checking.mli +++ b/checker/safe_checking.mli @@ -12,5 +12,5 @@ open Safe_typing (*i*) -val import : safe_environment -> compiled_library -> Univ.ContextSet.t -> vodigest -> safe_environment +val import : safe_environment -> Names.Cset.t Names.Cmap.t -> compiled_library -> Univ.ContextSet.t -> vodigest -> safe_environment * Names.Cset.t Names.Cmap.t val unsafe_import : safe_environment -> compiled_library -> Univ.ContextSet.t -> vodigest -> safe_environment 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/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 51a602303a..0d2f1dfbc7 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-05-18-V3" +# CACHEKEY: "bionic_coq-V2020-05-19-V33" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -58,7 +58,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ # EDGE switch ENV COMPILER_EDGE="4.10.0" \ - BASE_OPAM_EDGE="dune.2.5.0 dune-release.1.3.3 ocamlformat.0.14.0" + BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3 ocamlformat.0.14.2" # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index fb84155392..bfb25e72dd 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/807ca93fadd5197c2260490de0c76e500562dc05.tar.gz"; - sha256 = "10yq8bnls77fh3pk5chkkb1sv5lbdgyk1rr2v9xn71rr1k2x563p"; + url = "https://github.com/NixOS/nixpkgs/archive/17812e653d89c46d68b7b10e290b1c16758f4e47.tar.gz"; + sha256 = "1zcb70dyfqc8l2ywpbvxmpfshapdi0g365m3rhmwpagqg47pnyxs"; }) 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/03-notations/11986-float-low-level-printing.rst b/doc/changelog/03-notations/11986-float-low-level-printing.rst new file mode 100644 index 0000000000..f3d85cadc6 --- /dev/null +++ b/doc/changelog/03-notations/11986-float-low-level-printing.rst @@ -0,0 +1,5 @@ +- **Added:** + Add flag ``Printing Float`` to print primitive floats as hexadecimal + instead of decimal values. This is included in ``Set Printing All``. + (`#11986 <https://github.com/coq/coq/pull/11986>`_, + by Pierre Roux). diff --git a/doc/changelog/07-commands-and-options/12295-master+fix12234-show-proof.rst b/doc/changelog/07-commands-and-options/12295-master+fix12234-show-proof.rst new file mode 100644 index 0000000000..259253ec79 --- /dev/null +++ b/doc/changelog/07-commands-and-options/12295-master+fix12234-show-proof.rst @@ -0,0 +1,4 @@ +- **Fixed:** + A printing bug in the presence of elimination principles with local definitions + (`#12295 <https://github.com/coq/coq/pull/12295>`_, + by Hugo Herbelin; fixes `#12233 <https://github.com/coq/coq/pull/12233>`_). 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/doc/changelog/08-tools/12076-fix-5030.rst b/doc/changelog/08-tools/12076-fix-5030.rst new file mode 100644 index 0000000000..afb59b1cde --- /dev/null +++ b/doc/changelog/08-tools/12076-fix-5030.rst @@ -0,0 +1,4 @@ +- **Fixed:** + Fix #5030 (coqchk reports names from opaque modules as axioms) + (`#12076 <https://github.com/coq/coq/pull/12076>`_, + by Pierre Roux). diff --git a/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst b/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst new file mode 100644 index 0000000000..8a43f5af94 --- /dev/null +++ b/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst @@ -0,0 +1,4 @@ +- **Changed:** + The pretty-timed scripts and targets now print a newline at the end of their + tables, rather than creating text with no trailing newline (`#12368 + <https://github.com/coq/coq/pull/12368>`_, by Jason Gross). diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 899173a83a..b2b68482ef 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -1062,11 +1062,17 @@ Floating-point constants are parsed and pretty-printed as (17-digit) decimal constants. This ensures that the composition :math:`\text{parse} \circ \text{print}` amounts to the identity. -.. warn:: The constant @numeral is not a binary64 floating-point value. A closest value will be used and unambiguously printed @numeral. [inexact-float,parsing] +.. warn:: The constant @numeral is not a binary64 floating-point value. A closest value @numeral will be used and unambiguously printed @numeral. [inexact-float,parsing] Not all decimal constants are floating-point values. This warning is generated when parsing such a constant (for instance ``0.1``). +.. flag:: Printing Float + + Turn this flag off (it is on by default) to deactivate decimal + printing of floating-point constants. They will then be printed + with an hexadecimal representation. + .. example:: .. coqtop:: all 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/interp/constrextern.ml b/interp/constrextern.ml index 8097935ec2..63079993c8 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -888,12 +888,19 @@ let q_infinity () = qualid_of_ref "num.float.infinity" let q_neg_infinity () = qualid_of_ref "num.float.neg_infinity" let q_nan () = qualid_of_ref "num.float.nan" +let get_printing_float = Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Float"] + ~value:true + let extern_float f scopes = if Float64.is_nan f then CRef(q_nan (), None) else if Float64.is_infinity f then CRef(q_infinity (), None) else if Float64.is_neg_infinity f then CRef(q_neg_infinity (), None) else - let s = Float64.(to_string f) in + let s = + let hex = !Flags.raw_print || not (get_printing_float ()) in + if hex then Float64.to_hex_string f else Float64.to_string f in let n = NumTok.Signed.of_string s in extern_prim_token_delimiter_if_required (Numeral n) "float" "float_scope" scopes diff --git a/kernel/float64.ml b/kernel/float64.ml index 53fc13b04b..76005a3dc6 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -19,29 +19,27 @@ let is_nan (f : float) = f <> f let is_infinity f = f = infinity let is_neg_infinity f = f = neg_infinity -(* Printing a binary64 float in 17 decimal places and parsing it again - will yield the same float. We assume [to_string_raw] is not given a - [nan] or an infinity as input. *) -let to_string_raw f = Printf.sprintf "%.17g" f - (* OCaml gives a sign to nan values which should not be displayed as all NaNs are considered equal here. OCaml prints infinities as "inf" (resp. "-inf") but we want "infinity" (resp. "neg_infinity"). *) -let to_string f = +let to_string_raw fmt f = if is_nan f then "nan" else if is_infinity f then "infinity" else if is_neg_infinity f then "neg_infinity" - else to_string_raw f + else Printf.sprintf fmt f + +let to_hex_string = to_string_raw "%h" + +(* Printing a binary64 float in 17 decimal places and parsing it again + will yield the same float. *) +let to_string = to_string_raw "%.17g" let of_string = float_of_string (* Compiles a float to OCaml code *) let compile f = - let s = - if is_nan f then "nan" else if is_neg_infinity f then "neg_infinity" - else Printf.sprintf "%h" f in - Printf.sprintf "Float64.of_float (%s)" s + Printf.sprintf "Float64.of_float (%s)" (to_hex_string f) let of_float f = f diff --git a/kernel/float64.mli b/kernel/float64.mli index d43ff4553f..0afbfa89da 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -19,9 +19,19 @@ val is_nan : t -> bool val is_infinity : t -> bool val is_neg_infinity : t -> bool -val to_string : t -> string val of_string : string -> t +(** Print a float exactly as an hexadecimal value (exact decimal + * printing would be possible but sometimes requires more than 700 + * digits). *) +val to_hex_string : t -> string + +(** Print a float as a decimal value. The printing is not exact (the + * real value printed is not always the given floating-point value), + * however printing is precise enough that forall float [f], + * [of_string (to_decimal_string f) = f]. *) +val to_string : t -> string + val compile : t -> string val of_float : float -> t diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index e004613ef3..5d6e7c51d0 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -370,6 +370,11 @@ let ehole_var = EConstr.mkVar (Id.of_string "_") let pr_econstr_pat env sigma c0 = let rec wipe_evar c = let open EConstr in if isEvar sigma c then ehole_var else map sigma wipe_evar c in + let dummy_decl = + let dummy_prod = mkProd (make_annot Anonymous Sorts.Relevant,mkProp,mkProp) in + let na = make_annot (EConstr.destVar sigma ehole_var) Sorts.Relevant in + Context.Named.Declaration.(LocalAssum (na, dummy_prod)) in + let env = Environ.push_named dummy_decl env in pr_econstr_env env sigma (wipe_evar c0) (* Turn (new) evars into metas *) diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml index 9861a060ab..8e87fc13ca 100644 --- a/plugins/syntax/float_syntax.ml +++ b/plugins/syntax/float_syntax.ml @@ -28,8 +28,8 @@ let warn_inexact_float = Pp.strbrk (Printf.sprintf "The constant %s is not a binary64 floating-point value. \ - A closest value will be used and unambiguously printed %s." - sn (Float64.to_string f))) + A closest value %s will be used and unambiguously printed %s." + sn (Float64.to_hex_string f) (Float64.to_string f))) let interp_float ?loc n = let sn = NumTok.Signed.to_string n in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index ff278baf9f..13946208bc 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -25,7 +25,7 @@ open Namegen open Libnames open Globnames open Mod_subst -open Context.Named.Declaration +open Context.Rel.Declaration open Ltac_pretype type detyping_flags = { @@ -125,21 +125,8 @@ let print_universes = ref false (** If true, prints local context of evars, whatever print_arguments *) let print_evar_arguments = ref false -let add_name na b t (nenv, env) = - let open Context.Rel.Declaration in - (* Is this just a dummy? Be careful, printing doesn't always give us - a correct env. *) - let r = Sorts.Relevant in - add_name na nenv, push_rel (match b with - | None -> LocalAssum (make_annot na r,t) - | Some b -> LocalDef (make_annot na r,b,t) - ) - env - -let add_name_opt na b t (nenv, env) = - match t with - | None -> Termops.add_name na nenv, env - | Some t -> add_name na b t (nenv, env) +let add_name decl (nenv, env) = + add_name (get_name decl) nenv, push_rel decl env (****************************************************************************) (* Tools for printing of Cases *) @@ -406,24 +393,28 @@ let update_name sigma na ((_,(e,_)),c) = | _ -> na +let get_domain env sigma c = + let (_,t,_) = EConstr.destProd sigma (Reductionops.whd_all env sigma (Retyping.get_type_of env sigma c)) in + t + let rec decomp_branch tags nal flags (avoid,env as e) sigma c = match tags with | [] -> (List.rev nal,(e,c)) | b::tags -> - let na,c,let_in,body,t = + let decl, c, let_in = match EConstr.kind sigma (strip_outer_cast sigma c), b with - | Lambda (na,t,c),false -> na.binder_name,c,true,None,Some t - | LetIn (na,b,t,c),true -> - na.binder_name,c,false,Some b,Some t + | Lambda (na,t,c),false -> LocalAssum (na,t), c, true + | LetIn (na,b,t,c),true -> LocalDef (na,b,t), c, false | _, false -> - Name default_dependent_ident,(applist (lift 1 c, [mkRel 1])), - false,None,None + let na = make_annot (Name default_dependent_ident) Sorts.Relevant (* dummy *) in + LocalAssum (na, get_domain (snd env) sigma c), applist (lift 1 c, [mkRel 1]), false | _, true -> - Anonymous,lift 1 c,false,None,None + let na = make_annot Anonymous Sorts.Relevant (* dummy *) in + LocalDef (na, mkProp (* dummy *), type1), lift 1 c, false in - let na',avoid' = compute_name sigma ~let_in ~pattern:true flags avoid env na c in + let na',avoid' = compute_name sigma ~let_in ~pattern:true flags avoid env (get_name decl) c in decomp_branch tags (na'::nal) flags - (avoid', add_name_opt na' body t env) sigma c + (avoid', add_name (set_name na' decl) env) sigma c let rec build_tree na isgoal e sigma ci cl = let mkpat n rhs pl = @@ -564,26 +555,29 @@ let rec share_names detype flags n l avoid env sigma c t = match EConstr.kind sigma c, EConstr.kind sigma t with (* factorize even when not necessary to have better presentation *) | Lambda (na,t,c), Prod (na',t',c') -> + let decl = LocalAssum (na,t) in let na = Nameops.Name.pick_annot na na' in let t' = detype flags avoid env sigma t in let id, avoid = next_name_away flags na.binder_name avoid in - let env = add_name (Name id) None t env in + let env = add_name (set_name (Name id) decl) env in share_names detype flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' (* May occur for fix built interactively *) | LetIn (na,b,t',c), _ when n > 0 -> + let decl = LocalDef (na,b,t') in let t'' = detype flags avoid env sigma t' in let b' = detype flags avoid env sigma b in let id, avoid = next_name_away flags na.binder_name avoid in - let env = add_name (Name id) (Some b) t' env in + let env = add_name (set_name (Name id) decl) env in share_names detype flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t) (* Only if built with the f/n notation or w/o let-expansion in types *) | _, LetIn (_,b,_,t) when n > 0 -> share_names detype flags n l avoid env sigma c (subst1 b t) (* If it is an open proof: we cheat and eta-expand *) | _, Prod (na',t',c') when n > 0 -> + let decl = LocalAssum (na',t') in let t'' = detype flags avoid env sigma t' in let id, avoid = next_name_away flags na'.binder_name avoid in - let env = add_name (Name id) None t' env in + let env = add_name (set_name (Name id) decl) env in let appc = mkApp (lift 1 c,[|mkRel 1|]) in share_names detype flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' (* If built with the f/n notation: we renounce to share names *) @@ -621,7 +615,7 @@ let detype_fix detype flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = Array.fold_left2 (fun (avoid, env, l) na ty -> let id, avoid = next_name_away flags na.binder_name avoid in - (avoid, add_name (Name id) None ty env, id::l)) + (avoid, add_name (set_name (Name id) (LocalAssum (na,ty))) env, id::l)) (avoid, env, []) names tys in let n = Array.length tys in let v = Array.map3 @@ -637,7 +631,7 @@ let detype_cofix detype flags avoid env sigma n (names,tys,bodies) = Array.fold_left2 (fun (avoid, env, l) na ty -> let id, avoid = next_name_away flags na.binder_name avoid in - (avoid, add_name (Name id) None ty env, id::l)) + (avoid, add_name (set_name (Name id) (LocalAssum (na,ty))) env, id::l)) (avoid, env, []) names tys in let ntys = Array.length tys in let v = Array.map2 @@ -734,9 +728,9 @@ and detype_r d flags avoid env sigma t = | _ -> CastConv d2 in GCast(d1,cast) - | Prod (na,ty,c) -> detype_binder d flags BProd avoid env sigma na None ty c - | Lambda (na,ty,c) -> detype_binder d flags BLambda avoid env sigma na None ty c - | LetIn (na,b,ty,c) -> detype_binder d flags BLetIn avoid env sigma na (Some b) ty c + | Prod (na,ty,c) -> detype_binder d flags BProd avoid env sigma (LocalAssum (na,ty)) c + | Lambda (na,ty,c) -> detype_binder d flags BLambda avoid env sigma (LocalAssum (na,ty)) c + | LetIn (na,b,ty,c) -> detype_binder d flags BLetIn avoid env sigma (LocalDef (na,b,ty)) c | App (f,args) -> let mkapp f' args' = match DAst.get f' with @@ -770,6 +764,7 @@ and detype_r d flags avoid env sigma t = else noparams () | Evar (evk,cl) -> + let open Context.Named.Declaration in let bound_to_itself_or_letin decl c = match decl with | LocalDef _ -> true @@ -823,12 +818,12 @@ and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl = (Array.map3 (detype_eqn d flags avoid env sigma) constructs consnargsl bl) and detype_eqn d flags avoid env sigma constr construct_nargs branch = - let make_pat x avoid env b body ty ids = + let make_pat decl avoid env b ids = if force_wildcard () && noccurn sigma 1 b then - DAst.make @@ PatVar Anonymous,avoid,(add_name Anonymous body ty env),ids + DAst.make @@ PatVar Anonymous,avoid,(add_name (set_name Anonymous decl) env),ids else - let na,avoid' = compute_name sigma ~let_in:false ~pattern:true flags avoid env x b in - DAst.make (PatVar na),avoid',(add_name na body ty env),add_vname ids na + let na,avoid' = compute_name sigma ~let_in:false ~pattern:true flags avoid env (get_name decl) b in + DAst.make (PatVar na),avoid',(add_name (set_name na decl) env),add_vname ids na in let rec buildrec ids patlist avoid env l b = match EConstr.kind sigma b, l with @@ -837,11 +832,11 @@ and detype_eqn d flags avoid env sigma constr construct_nargs branch = [DAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)], detype d flags avoid env sigma b) | Lambda (x,t,b), false::l -> - let pat,new_avoid,new_env,new_ids = make_pat x.binder_name avoid env b None t ids in + let pat,new_avoid,new_env,new_ids = make_pat (LocalAssum (x,t)) avoid env b ids in buildrec new_ids (pat::patlist) new_avoid new_env l b | LetIn (x,b,t,b'), true::l -> - let pat,new_avoid,new_env,new_ids = make_pat x.binder_name avoid env b' (Some b) t ids in + let pat,new_avoid,new_env,new_ids = make_pat (LocalDef (x,b,t)) avoid env b' ids in buildrec new_ids (pat::patlist) new_avoid new_env l b' | Cast (c,_,_), l -> (* Oui, il y a parfois des cast *) @@ -856,18 +851,22 @@ and detype_eqn d flags avoid env sigma constr construct_nargs branch = termes seront construits à partir de la syntaxe Cases *) (* nommage de la nouvelle variable *) let new_b = applist (lift 1 b, [mkRel 1]) in + let typ = get_domain (snd env) sigma b in let pat,new_avoid,new_env,new_ids = - make_pat Anonymous avoid env new_b None mkProp ids in + make_pat (LocalAssum (make_annot Anonymous Sorts.Relevant (* dummy *),typ)) avoid env new_b ids in buildrec new_ids (pat::patlist) new_avoid new_env l new_b in buildrec Id.Set.empty [] avoid env construct_nargs branch -and detype_binder d flags bk avoid env sigma {binder_name=na} body ty c = +and detype_binder d flags bk avoid env sigma decl c = + let na = get_name decl in + let body = get_value decl in + let ty = get_type decl in let na',avoid' = match bk with | BLetIn -> compute_name sigma ~let_in:true ~pattern:false flags avoid env na c | _ -> compute_name sigma ~let_in:false ~pattern:false flags avoid env na c in - let r = detype d flags avoid' (add_name na' body ty env) sigma c in + let r = detype d flags avoid' (add_name (set_name na' decl) env) sigma c in match bk with | BProd -> GProd (na',Explicit,detype d { flags with flg_isgoal = false } avoid env sigma ty, r) | BLambda -> GLambda (na',Explicit,detype d { flags with flg_isgoal = false } avoid env sigma ty, r) @@ -883,7 +882,6 @@ let detype_rel_context d flags where avoid env sigma sign = let rec aux avoid env = function | [] -> [] | decl::rest -> - let open Context.Rel.Declaration in let na = get_name decl in let t = get_type decl in let na',avoid' = @@ -898,7 +896,7 @@ let detype_rel_context d flags where avoid env sigma sign = in let b' = Option.map (detype d flags avoid env sigma) b in let t' = detype d flags avoid env sigma t in - (na',Explicit,b',t') :: aux avoid' (add_name na' b t env) rest + (na',Explicit,b',t') :: aux avoid' (add_name (set_name na' decl) env) rest in aux avoid env (List.rev sign) let detype_names isgoal avoid nenv env sigma t = @@ -916,7 +914,6 @@ let detype_rel_context d ?(lax = false) where avoid env sigma sign = detype_rel_context d flags where avoid env sigma sign let detype_closed_glob ?lax isgoal avoid env sigma t = - let open Context.Rel.Declaration in let convert_id cl id = try Id.Map.find id cl.idents with Not_found -> id 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..d4ad438d61 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -115,9 +115,13 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \ coqdoc ssr primitive/uint63 primitive/float ltac2 # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS) +SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk output-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 @@ -188,6 +192,7 @@ summary: $(call summary_dir, "IDE tests", ide); \ $(call summary_dir, "VI tests", vio); \ $(call summary_dir, "Coqchk tests", coqchk); \ + $(call summary_dir, "Output tests with coqchk", output-coqchk); \ $(call summary_dir, "Coqwc tests", coqwc); \ $(call summary_dir, "Coq makefile", coq-makefile); \ $(call summary_dir, "Coqdoc tests", coqdoc); \ @@ -458,6 +463,43 @@ $(addsuffix .log,$(wildcard output-coqtop/*.v)): %.v.log: %.v %.out $(PREREQUISI fi; \ } > "$@" +output-coqchk: $(addsuffix .log,$(wildcard output-coqchk/*.v)) +$(addsuffix .log,$(wildcard output-coqchk/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) + @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" + $(HIDE){ \ + opts="$(if $(findstring modules/,$<),-R modules Mods)"; \ + echo $(call log_intro,$<); \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \ + if [ $$R = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error! (should be accepted)"; \ + $(FAIL); \ + fi; \ + } > "$@" + @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi + $(HIDE)if ! grep -q -F "Error!" $@; then { \ + echo $(call log_intro,$<); \ + output=$*.out.real; \ + export LC_CTYPE=C; \ + export LANG=C; \ + $(coqchk) -o -silent $(call get_set_impredicativity,$<) $(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-Q $(shell dirname $<) "" -norec $(shell basename $< .v)) 2>&1 \ + | sed 's/File "[^"]*"/File "stdin"/' \ + > $$output; \ + diff -a -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \ + if [ $$R = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + rm $$output; \ + else \ + echo $(log_failure); \ + echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ + fi; \ + } > "$(shell dirname $<)/$(shell basename $< .v).chk.log"; fi + .PHONY: approve-output approve-output: output output-coqtop $(HIDE)for f in output/*.out.real; do \ @@ -470,6 +512,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/bugs/closed/bug_12233.v b/test-suite/bugs/closed/bug_12233.v new file mode 100644 index 0000000000..3cbf084594 --- /dev/null +++ b/test-suite/bugs/closed/bug_12233.v @@ -0,0 +1,5 @@ +Theorem thm (A:Prop) (H:exists m:nat, True) : True. +destruct H as ([|],?). +assert A. +Show Proof. (* was raising Not_found since 8.7 *) +Abort. 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/coq-makefile/timing/after/time-of-build-both.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired index 541b307b5e..85aeab2c69 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired @@ -3,4 +3,4 @@ 0m00.47s | 394716 ko | Total Time / Peak Mem | 0m00.45s | 394392 ko || +0m00.01s || 324 ko | +4.44% | +0.08% ----------------------------------------------------------------------------------------------------------------------------- 0m00.42s | 394716 ko | Fast.vo | 0m00.02s | 57164 ko || +0m00.40s || 337552 ko | +1999.99% | +590.49% -0m00.05s | 57124 ko | Slow.vo | 0m00.43s | 394392 ko || -0m00.38s || -337268 ko | -88.37% | -85.51%
\ No newline at end of file +0m00.05s | 57124 ko | Slow.vo | 0m00.43s | 394392 ko || -0m00.38s || -337268 ko | -88.37% | -85.51% diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired index 71e4ee0b32..ed5454b480 100644 --- a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired +++ b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired @@ -1,9 +1,9 @@ After | Code | Before || Change | % Change ---------------------------------------------------------------------------------------------------- - 0m14.06s | Total | 0m00.72s || +0m13.34s | +1854.02% + 0m15.00s | Total | 0m00.72s || +0m14.28s | +1983.61% ---------------------------------------------------------------------------------------------------- -0m13.582s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m00.353s || +0m13.22s | +3747.59% -0m00.335s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.225s || +0m00.11s | +48.88% -0m00.152s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.142s || +0m00.01s | +7.04% +0m14.578s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m00.356s || +0m14.22s | +3994.94% +0m00.284s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.225s || +0m00.05s | +26.22% + 0m00.14s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.139s || +0m00.00s | +0.71% 0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | N/A || +0m00.00s | N/A - N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | 0m00.s || +0m00.00s | N/A
\ No newline at end of file + N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | 0m00.s || +0m00.00s | N/A diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-absolute.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-absolute.log.expected index e7d289858b..948e28fbc6 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-absolute.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-absolute.log.expected @@ -23,4 +23,4 @@ 0m07.33s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.40s | 578344 ko || -0m00.07s || -3956 ko | -0.94% | -0.68% 0m01.93s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.73s | 546112 ko || +0m00.19s || -1940 ko | +11.56% | -0.35% 0m01.85s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.95s | 648632 ko || -0m00.09s || -2332 ko | -5.12% | -0.35% - 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12%
\ No newline at end of file + 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-auto.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-auto.log.expected index 36f86e0e1e..ea36822c8d 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-auto.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-auto.log.expected @@ -23,4 +23,4 @@ 0m07.33s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.40s | 578344 ko || -0m00.07s || -3956 ko | -0.94% | -0.68% 0m01.93s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.73s | 546112 ko || +0m00.19s || -1940 ko | +11.56% | -0.35% 0m01.85s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.95s | 648632 ko || -0m00.09s || -2332 ko | -5.12% | -0.35% - 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12%
\ No newline at end of file + 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-diff.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-diff.log.expected index 6415223693..b6c21a3145 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-diff.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real-diff.log.expected @@ -23,4 +23,4 @@ 3m22.96s | 3302508 ko | Specific/NISTP256/AMD64/femul | 3m37.80s | 3307052 ko || -0m14.84s || -4544 ko | -6.81% | -0.13% 2m35.79s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m59.21s | 1549104 ko || -0m23.42s || -94408 ko | -13.06% | -6.09% 3m01.77s | 1589516 ko | Specific/solinas32_2e255m765_13limbs/femul | 3m27.94s | 1656912 ko || -0m26.16s || -67396 ko | -12.58% | -4.06% - 4m16.77s | 1617000 ko | Specific/X25519/C64/ladderstep | 5m16.83s | 1621500 ko || -1m00.06s || -4500 ko | -18.95% | -0.27%
\ No newline at end of file + 4m16.77s | 1617000 ko | Specific/X25519/C64/ladderstep | 5m16.83s | 1621500 ko || -1m00.06s || -4500 ko | -18.95% | -0.27% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real.log.expected index 36f86e0e1e..ea36822c8d 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real.log.expected @@ -23,4 +23,4 @@ 0m07.33s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.40s | 578344 ko || -0m00.07s || -3956 ko | -0.94% | -0.68% 0m01.93s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.73s | 546112 ko || +0m00.19s || -1940 ko | +11.56% | -0.35% 0m01.85s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.95s | 648632 ko || -0m00.09s || -2332 ko | -5.12% | -0.35% - 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12%
\ No newline at end of file + 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-absolute.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-absolute.log.expected index 84d20f484a..a964c29da8 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-absolute.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-absolute.log.expected @@ -23,4 +23,4 @@ 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.22s | 578344 ko || -0m00.04s || -3956 ko | -0.55% | -0.68% 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.58s | 546112 ko || +0m00.13s || -1940 ko | +8.86% | -0.35% 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.72s | 648632 ko || -0m00.05s || -2332 ko | -2.90% | -0.35% - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12%
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-auto.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-auto.log.expected index 7576dca88b..59af8c3145 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-auto.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-auto.log.expected @@ -23,4 +23,4 @@ 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.22s | 578344 ko || -0m00.04s || -3956 ko | -0.55% | -0.68% 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.58s | 546112 ko || +0m00.13s || -1940 ko | +8.86% | -0.35% 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.72s | 648632 ko || -0m00.05s || -2332 ko | -2.90% | -0.35% - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12%
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-diff.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-diff.log.expected index 1173a6fe29..5ee974c9f3 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-diff.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user-diff.log.expected @@ -23,4 +23,4 @@ 3m09.62s | 3302508 ko | Specific/NISTP256/AMD64/femul | 3m22.52s | 3307052 ko || -0m12.90s || -4544 ko | -6.36% | -0.13% 2m23.70s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m44.11s | 1549104 ko || -0m20.41s || -94408 ko | -12.43% | -6.09% 2m48.52s | 1589516 ko | Specific/solinas32_2e255m765_13limbs/femul | 3m12.95s | 1656912 ko || -0m24.42s || -67396 ko | -12.66% | -4.06% - 4m01.34s | 1617000 ko | Specific/X25519/C64/ladderstep | 4m59.49s | 1621500 ko || -0m58.15s || -4500 ko | -19.41% | -0.27%
\ No newline at end of file + 4m01.34s | 1617000 ko | Specific/X25519/C64/ladderstep | 4m59.49s | 1621500 ko || -0m58.15s || -4500 ko | -19.41% | -0.27% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected index 7576dca88b..59af8c3145 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected @@ -23,4 +23,4 @@ 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.22s | 578344 ko || -0m00.04s || -3956 ko | -0.55% | -0.68% 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.58s | 546112 ko || +0m00.13s || -1940 ko | +8.86% | -0.35% 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.72s | 648632 ko || -0m00.05s || -2332 ko | -2.90% | -0.35% - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12%
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected index 94122d8190..317497c68a 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected @@ -23,4 +23,4 @@ 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-user.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-user.log.expected index 94122d8190..317497c68a 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-user.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-user.log.expected @@ -23,4 +23,4 @@ 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected index 6104c78380..ee9fca7eb4 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected @@ -304,4 +304,4 @@ 0m00.04s | 54440 ko | bedrock2/deps/coqutil/src/dlet 0m00.04s | 54804 ko | bedrock2/deps/coqutil/src/sanity 0m00.04s | 56096 ko | bedrock2/deps/riscv-coq/src/Utility/MMIOTrace - 0m00.03s | 54716 ko | bedrock2/compiler/src/util/LogGoal
\ No newline at end of file + 0m00.03s | 54716 ko | bedrock2/compiler/src/util/LogGoal diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-real.v.timing.diff.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-real.v.timing.diff.expected index 76b0a35cb2..37f144b19b 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-real.v.timing.diff.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-real.v.timing.diff.expected @@ -26,4 +26,4 @@ 0m00.s | Chars 186-194 ~ 202-210 [exact~I.] | N/A || +0m00.00s | N/A N/A | Chars 186-198 ~ 202-214 [constructor.] | 0m00.s || +0m00.00s | N/A 0m00.s | Chars 195-199 ~ 215-219 [Qed.] | 0m00.s || +0m00.00s | N/A - 0m00.s | Chars 200-257 ~ 220-277 [Goal~_~List.repeat~Z.div_eucl~...] | 0m00.s || +0m00.00s | N/A
\ No newline at end of file + 0m00.s | Chars 200-257 ~ 220-277 [Goal~_~List.repeat~Z.div_eucl~...] | 0m00.s || +0m00.00s | N/A diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-user.v.timing.diff.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-user.v.timing.diff.expected index 1e27d5d12b..a77215b67d 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-user.v.timing.diff.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-user.v.timing.diff.expected @@ -26,4 +26,4 @@ 0m00.s | Chars 173-183 ~ 189-199 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A 0m00.s | Chars 186-194 ~ 202-210 [exact~I.] | N/A || +0m00.00s | N/A N/A | Chars 186-198 ~ 202-214 [constructor.] | 0m00.s || +0m00.00s | N/A - 0m00.s | Chars 195-199 ~ 215-219 [Qed.] | 0m00.s || +0m00.00s | N/A
\ No newline at end of file + 0m00.s | Chars 195-199 ~ 215-219 [Qed.] | 0m00.s || +0m00.00s | N/A diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-absolute.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-absolute.log.expected index 2a2d2c1b2f..9d6231f2ce 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-absolute.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-absolute.log.expected @@ -23,4 +23,4 @@ 0m01.85s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.95s | 648632 ko || -0m00.09s || -2332 ko | -5.12% | -0.35% 0m07.33s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.40s | 578344 ko || -0m00.07s || -3956 ko | -0.94% | -0.68% 0m01.93s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.73s | 546112 ko || +0m00.19s || -1940 ko | +11.56% | -0.35% - 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12%
\ No newline at end of file + 0m01.38s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.18s | 539160 ko || +0m00.19s || 648 ko | +16.94% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-auto.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-auto.log.expected index 7e4cfaec1c..4864c1aaf7 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-auto.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-auto.log.expected @@ -23,4 +23,4 @@ 0m27.81s | 756080 ko | Specific/NISTP256/AMD64/fenz | 0m28.91s | 756216 ko || -0m01.10s || -136 ko | -3.80% | -0.01% 0m22.81s | 766300 ko | Specific/X25519/C64/feadd | 0m23.43s | 766168 ko || -0m00.62s || 132 ko | -2.64% | +0.01% 0m11.15s | 687760 ko | Specific/X25519/C64/Synthesis | 0m11.23s | 687812 ko || -0m00.08s || -52 ko | -0.71% | -0.00% - 0m31.00s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m32.08s | 765212 ko || -0m01.07s || -4 ko | -3.36% | -0.00%
\ No newline at end of file + 0m31.00s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m32.08s | 765212 ko || -0m01.07s || -4 ko | -3.36% | -0.00% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-diff.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-diff.log.expected index 7842f91f1f..27d3a9c683 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-diff.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real-diff.log.expected @@ -23,4 +23,4 @@ 0m43.34s | 793376 ko | Specific/NISTP256/AMD64/fesub | 0m43.78s | 799668 ko || -0m00.43s || -6292 ko | -1.00% | -0.78% 0m39.72s | 825448 ko | Specific/X25519/C64/femul | 0m42.98s | 839624 ko || -0m03.25s || -14176 ko | -7.58% | -1.68% 3m01.77s | 1589516 ko | Specific/solinas32_2e255m765_13limbs/femul | 3m27.94s | 1656912 ko || -0m26.16s || -67396 ko | -12.58% | -4.06% - 2m35.79s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m59.21s | 1549104 ko || -0m23.42s || -94408 ko | -13.06% | -6.09%
\ No newline at end of file + 2m35.79s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m59.21s | 1549104 ko || -0m23.42s || -94408 ko | -13.06% | -6.09% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real.log.expected index 7e4cfaec1c..4864c1aaf7 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-real.log.expected @@ -23,4 +23,4 @@ 0m27.81s | 756080 ko | Specific/NISTP256/AMD64/fenz | 0m28.91s | 756216 ko || -0m01.10s || -136 ko | -3.80% | -0.01% 0m22.81s | 766300 ko | Specific/X25519/C64/feadd | 0m23.43s | 766168 ko || -0m00.62s || 132 ko | -2.64% | +0.01% 0m11.15s | 687760 ko | Specific/X25519/C64/Synthesis | 0m11.23s | 687812 ko || -0m00.08s || -52 ko | -0.71% | -0.00% - 0m31.00s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m32.08s | 765212 ko || -0m01.07s || -4 ko | -3.36% | -0.00%
\ No newline at end of file + 0m31.00s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m32.08s | 765212 ko || -0m01.07s || -4 ko | -3.36% | -0.00% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-absolute.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-absolute.log.expected index ea116a804f..48e168657c 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-absolute.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-absolute.log.expected @@ -23,4 +23,4 @@ 0m01.67s | 646300 ko | Specific/Framework/SynthesisFramework | 0m01.72s | 648632 ko || -0m00.05s || -2332 ko | -2.90% | -0.35% 0m07.18s | 574388 ko | Compilers/Z/Bounds/Pipeline/Definition | 0m07.22s | 578344 ko || -0m00.04s || -3956 ko | -0.55% | -0.68% 0m01.72s | 544172 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.58s | 546112 ko || +0m00.13s || -1940 ko | +8.86% | -0.35% - 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12%
\ No newline at end of file + 0m01.19s | 539808 ko | Compilers/Z/Bounds/Pipeline | 0m01.04s | 539160 ko || +0m00.14s || 648 ko | +14.42% | +0.12% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-auto.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-auto.log.expected index 128f140662..fc26998b8f 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-auto.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-auto.log.expected @@ -23,4 +23,4 @@ 0m25.50s | 756080 ko | Specific/NISTP256/AMD64/fenz | 0m26.41s | 756216 ko || -0m00.91s || -136 ko | -3.44% | -0.01% 0m20.93s | 766300 ko | Specific/X25519/C64/feadd | 0m21.41s | 766168 ko || -0m00.48s || 132 ko | -2.24% | +0.01% 0m10.37s | 687760 ko | Specific/X25519/C64/Synthesis | 0m10.30s | 687812 ko || +0m00.06s || -52 ko | +0.67% | -0.00% - 0m28.51s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m29.46s | 765212 ko || -0m00.94s || -4 ko | -3.22% | -0.00%
\ No newline at end of file + 0m28.51s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m29.46s | 765212 ko || -0m00.94s || -4 ko | -3.22% | -0.00% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-diff.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-diff.log.expected index 79dc49892f..1fcdb84025 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-diff.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user-diff.log.expected @@ -23,4 +23,4 @@ 0m39.59s | 793376 ko | Specific/NISTP256/AMD64/fesub | 0m40.09s | 799668 ko || -0m00.50s || -6292 ko | -1.24% | -0.78% 0m36.32s | 825448 ko | Specific/X25519/C64/femul | 0m39.50s | 839624 ko || -0m03.17s || -14176 ko | -8.05% | -1.68% 2m48.52s | 1589516 ko | Specific/solinas32_2e255m765_13limbs/femul | 3m12.95s | 1656912 ko || -0m24.42s || -67396 ko | -12.66% | -4.06% - 2m23.70s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m44.11s | 1549104 ko || -0m20.41s || -94408 ko | -12.43% | -6.09%
\ No newline at end of file + 2m23.70s | 1454696 ko | Specific/solinas32_2e255m765_12limbs/femul | 2m44.11s | 1549104 ko || -0m20.41s || -94408 ko | -12.43% | -6.09% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user.log.expected index 128f140662..fc26998b8f 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/005-correct-diff-sorting-order-mem/time-of-build-both-user.log.expected @@ -23,4 +23,4 @@ 0m25.50s | 756080 ko | Specific/NISTP256/AMD64/fenz | 0m26.41s | 756216 ko || -0m00.91s || -136 ko | -3.44% | -0.01% 0m20.93s | 766300 ko | Specific/X25519/C64/feadd | 0m21.41s | 766168 ko || -0m00.48s || 132 ko | -2.24% | +0.01% 0m10.37s | 687760 ko | Specific/X25519/C64/Synthesis | 0m10.30s | 687812 ko || +0m00.06s || -52 ko | +0.67% | -0.00% - 0m28.51s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m29.46s | 765212 ko || -0m00.94s || -4 ko | -3.22% | -0.00%
\ No newline at end of file + 0m28.51s | 765208 ko | Specific/NISTP256/AMD64/feopp | 0m29.46s | 765212 ko || -0m00.94s || -4 ko | -3.22% | -0.00% 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/test-suite/output-coqchk/bug_5030.out b/test-suite/output-coqchk/bug_5030.out new file mode 100644 index 0000000000..bef45bf2f6 --- /dev/null +++ b/test-suite/output-coqchk/bug_5030.out @@ -0,0 +1,14 @@ + +CONTEXT SUMMARY +=============== + +* Theory: Set is predicative + +* Axioms: <none> + +* Constants/Inductives relying on type-in-type: <none> + +* Constants/Inductives relying on unsafe (co)fixpoints: <none> + +* Inductives whose positivity is assumed: <none> + diff --git a/test-suite/output-coqchk/bug_5030.v b/test-suite/output-coqchk/bug_5030.v new file mode 100644 index 0000000000..543784e3c9 --- /dev/null +++ b/test-suite/output-coqchk/bug_5030.v @@ -0,0 +1,10 @@ +Module Type testt. +Parameter proof : True. +End testt. + +Module Export test : testt. +Definition proof := I. +End test. + +Lemma true : True. +Proof. apply proof. Qed. diff --git a/test-suite/output/FloatExtraction.out b/test-suite/output/FloatExtraction.out index dd8189c56f..539ec9b2bf 100644 --- a/test-suite/output/FloatExtraction.out +++ b/test-suite/output/FloatExtraction.out @@ -1,16 +1,18 @@ File "stdin", line 25, characters 8-12: Warning: The constant 0.01 is not a binary64 floating-point value. A closest -value will be used and unambiguously printed 0.01. [inexact-float,parsing] +value 0x1.47ae147ae147bp-7 will be used and unambiguously printed 0.01. +[inexact-float,parsing] File "stdin", line 25, characters 20-25: Warning: The constant -0.01 is not a binary64 floating-point value. A closest -value will be used and unambiguously printed -0.01. [inexact-float,parsing] +value -0x1.47ae147ae147bp-7 will be used and unambiguously printed -0.01. +[inexact-float,parsing] File "stdin", line 25, characters 27-35: Warning: The constant 1.7e+308 is not a binary64 floating-point value. A -closest value will be used and unambiguously printed 1.6999999999999999e+308. -[inexact-float,parsing] +closest value 0x1.e42d130773b76p+1023 will be used and unambiguously printed +1.6999999999999999e+308. [inexact-float,parsing] File "stdin", line 25, characters 37-46: Warning: The constant -1.7e-308 is not a binary64 floating-point value. A -closest value will be used and unambiguously printed +closest value -0x0.c396c98f8d899p-1022 will be used and unambiguously printed -1.7000000000000002e-308. [inexact-float,parsing] (** val infinity : Float64.t **) diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out index 4a5a700879..0b18e9a3d2 100644 --- a/test-suite/output/FloatSyntax.out +++ b/test-suite/output/FloatSyntax.out @@ -6,13 +6,13 @@ : float File "stdin", line 9, characters 6-13: Warning: The constant 2.5e123 is not a binary64 floating-point value. A -closest value will be used and unambiguously printed 2.4999999999999999e+123. -[inexact-float,parsing] +closest value 0x1.e412f0f768fadp+409 will be used and unambiguously printed +2.4999999999999999e+123. [inexact-float,parsing] 2.4999999999999999e+123%float : float File "stdin", line 10, characters 7-16: Warning: The constant -2.5e-123 is not a binary64 floating-point value. A -closest value will be used and unambiguously printed +closest value -0x1.a71368f0f3047p-408 will be used and unambiguously printed -2.5000000000000001e-123. [inexact-float,parsing] (-2.5000000000000001e-123)%float : float @@ -28,13 +28,13 @@ closest value will be used and unambiguously printed : float File "stdin", line 19, characters 6-13: Warning: The constant 2.5e123 is not a binary64 floating-point value. A -closest value will be used and unambiguously printed 2.4999999999999999e+123. -[inexact-float,parsing] +closest value 0x1.e412f0f768fadp+409 will be used and unambiguously printed +2.4999999999999999e+123. [inexact-float,parsing] 2.4999999999999999e+123 : float File "stdin", line 20, characters 7-16: Warning: The constant -2.5e-123 is not a binary64 floating-point value. A -closest value will be used and unambiguously printed +closest value -0x1.a71368f0f3047p-408 will be used and unambiguously printed -2.5000000000000001e-123. [inexact-float,parsing] -2.5000000000000001e-123 : float @@ -56,16 +56,24 @@ closest value will be used and unambiguously printed : float File "stdin", line 30, characters 6-11: Warning: The constant 1e309 is not a binary64 floating-point value. A closest -value will be used and unambiguously printed infinity. +value infinity will be used and unambiguously printed infinity. [inexact-float,parsing] infinity : float File "stdin", line 31, characters 6-12: Warning: The constant -1e309 is not a binary64 floating-point value. A -closest value will be used and unambiguously printed neg_infinity. -[inexact-float,parsing] +closest value neg_infinity will be used and unambiguously printed +neg_infinity. [inexact-float,parsing] neg_infinity : float +0x1p-1 + : float +0.5 + : float +0x1p-1 + : float +0.5 + : float 2 : nat 2%float diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v index 36ffc27239..d3eb6d2e4c 100644 --- a/test-suite/output/FloatSyntax.v +++ b/test-suite/output/FloatSyntax.v @@ -30,6 +30,15 @@ Check -0xb.2cp-2. Check 1e309. Check -1e309. +Set Printing All. +Check 0.5. +Unset Printing All. +Check 0.5. +Unset Printing Float. +Check 0.5. +Set Printing Float. +Check 0.5. + Open Scope nat_scope. Check 2. diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index c4620f5b50..a3078af4a1 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -468,6 +468,7 @@ def make_table_string(stats_dict, for name in names]) def print_or_write_table(table, files): + if table[-1] != '\n': table += '\n' if len(files) == 0 or '-' in files: if hasattr(sys.stdout, 'buffer'): sys.stdout.buffer.write(table.encode("utf-8")) 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..c77d4909da 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 @@ -1215,19 +1210,20 @@ let get_hide_obligations = ~key:["Hide"; "Obligations"] ~value:false -let declare_obligation prg obl body ty uctx = +let declare_obligation prg obl ~uctx ~types ~body = + let univs = UState.univ_entry ~poly:prg.prg_poly uctx in let body = prg.prg_reduce body in - let ty = Option.map prg.prg_reduce ty in + let types = Option.map prg.prg_reduce types in match obl.obl_status with | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)}) | force, Evar_kinds.Define opaque -> let opaque = (not force) && opaque in let poly = prg.prg_poly in let ctx, body, ty, args = - if not poly then shrink_body body ty - else ([], body, ty, [||]) + if not poly then shrink_body body types + else ([], body, types, [||]) in - let ce = definition_entry ?types:ty ~opaque ~univs:uctx body in + let ce = definition_entry ?types:ty ~opaque ~univs body in (* ppedrot: seems legit to have obligations as local *) let constant = declare_constant ~name:obl.obl_name @@ -1239,7 +1235,7 @@ let declare_obligation prg obl body ty uctx = add_hint (Locality.make_section_locality None) prg constant; definition_message obl.obl_name; let body = - match uctx with + match univs with | Entries.Polymorphic_entry (_, uctx) -> Some (DefinedObl (constant, Univ.UContext.instance uctx)) | Entries.Monomorphic_entry _ -> @@ -1626,8 +1622,7 @@ let obligation_terminator entries uctx {name; num; auto} = in let obl = {obl with obl_status = (false, status)} in let uctx = if prg.prg_poly then uctx else UState.union prg.prg_ctx uctx in - let univs = UState.univ_entry ~poly:prg.prg_poly uctx in - let defined, obl = declare_obligation prg obl body ty univs in + let defined, obl = declare_obligation prg obl ~body ~types:ty ~uctx in let prg_ctx = if prg.prg_poly then (* Polymorphic *) @@ -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..647896e2f5 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 @@ -443,26 +439,21 @@ module ProgramDecl : sig -> Names.Id.t list -> fixpoint_kind option -> Vernacexpr.decl_notation list - -> ( Names.Id.t - * Constr.types - * Evar_kinds.t Loc.located - * (bool * Evar_kinds.obligation_definition_status) - * Int.Set.t - * unit Proofview.tactic option ) - array + -> RetrieveObl.obligation_info -> (Constr.constr -> Constr.constr) -> t val set_uctx : uctx:UState.t -> t -> t end -(** [declare_obligation] Save an obligation *) +(** [declare_obligation prg obl ~uctx ~types ~body] Save an obligation + [obl] for program definition [prg] *) val declare_obligation : ProgramDecl.t -> Obligation.t - -> Constr.types - -> Constr.types option - -> Entries.universes_entry + -> uctx:UState.t + -> types:Constr.types option + -> body:Constr.types -> bool * Obligation.t module State : sig @@ -521,7 +512,6 @@ val obl_substitution : -> (Id.t * (Constr.types * Constr.types)) list val dependencies : Obligation.t array -> int -> Int.Set.t -val err_not_transp : unit -> unit (* This is a hack to make it possible for Obligations to craft a Qed * behind the scenes. The fix_exn the Stm attaches to the Future proof diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 5fdee9f2d4..a8eac8fd2d 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -53,7 +53,6 @@ module Error = struct end -let assumption_message = Declare.assumption_message let default_tactic = ref (Proofview.tclUNIT ()) let evar_of_obligation o = Evd.make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) @@ -183,18 +182,16 @@ and solve_obligation_by_tac prg obls i tac = match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac prg.prg_poly (Evd.evar_universe_context evd) with | None -> None - | Some (t, ty, ctx) -> - let prg = ProgramDecl.set_uctx ~uctx:ctx prg in + | Some (t, ty, uctx) -> + let prg = ProgramDecl.set_uctx ~uctx prg in (* Why is uctx not used above? *) - let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in - let def, obl' = declare_obligation prg obl t ty uctx in + let def, obl' = declare_obligation prg obl ~body:t ~types:ty ~uctx in 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_global = UState.from_env (Global.env ()) in + let uctx = UState.merge_subst uctx_global (UState.subst uctx) in + Some (ProgramDecl.set_uctx ~uctx prg)) else Some prg else None @@ -254,27 +251,32 @@ and auto_solve_obligations n ?oblset tac : progress = open Pp +let show_single_obligation i n obls x = + let x = subst_deps_obl obls x in + let env = Global.env () in + let sigma = Evd.from_env env in + let msg = + str "Obligation" ++ spc () + ++ int (succ i) + ++ spc () ++ str "of" ++ spc () ++ Id.print n ++ str ":" ++ spc () + ++ hov 1 (Printer.pr_constr_env env sigma x.obl_type + ++ str "." ++ fnl ()) in + Feedback.msg_info msg + let show_obligations_of_prg ?(msg = true) prg = let n = prg.prg_name in let {obls; remaining} = prg.prg_obligations in let showed = ref 5 in if msg then Feedback.msg_info (int remaining ++ str " obligation(s) remaining: "); - Array.iteri (fun i x -> - match x.obl_body with - | None -> - if !showed > 0 then ( - decr showed; - let x = subst_deps_obl obls x in - let env = Global.env () in - let sigma = Evd.from_env env in - Feedback.msg_info - ( str "Obligation" ++ spc () - ++ int (succ i) - ++ spc () ++ str "of" ++ spc () ++ Id.print n ++ str ":" ++ spc () - ++ hov 1 - ( Printer.pr_constr_env env sigma x.obl_type - ++ str "." ++ fnl () ) ) ) - | Some _ -> ()) + Array.iteri + (fun i x -> + match x.obl_body with + | None -> + if !showed > 0 then begin + decr showed; + show_single_obligation i n obls x + end + | Some _ -> ()) obls let show_obligations ?(msg = true) n = @@ -373,7 +375,7 @@ let admit_prog prg = let kn = Declare.declare_constant ~name:x.obl_name ~local:Declare.ImportNeedQualified (Declare.ParameterEntry (None, (x.obl_type, ctx), None)) ~kind:Decls.(IsAssumption Conjectural) in - assumption_message x.obl_name; + Declare.assumption_message x.obl_name; obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x | Some _ -> ()) obls; 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 |