diff options
29 files changed, 227 insertions, 197 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 4a6555a4f7..6ceb7f54b2 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1087,11 +1087,10 @@ function make_menhir { make_ocaml make_findlib make_ocamlbuild - # This is the version required by latest CompCert - if build_prep https://gitlab.inria.fr/fpottier/menhir/-/archive/20190626 menhir-20190626 tar.gz 1 ; then - # Note: menhir doesn't support -j 8, so don't pass MAKE_OPT - log2 make all PREFIX="$PREFIXOCAML" - log2 make install PREFIX="$PREFIXOCAML" + if build_prep https://gitlab.inria.fr/fpottier/menhir/-/archive/20200525 menhir-20200525 tar.gz 1 ; then + # ToDo: don't know if this is the intended / most reliable to do it, but it works + log2 dune build @install + log2 dune install menhir menhirSdk menhirLib build_post fi } @@ -1194,10 +1193,10 @@ function make_elpi { make_dune make_re - if build_prep https://github.com/LPCIC/elpi/archive v1.11.0 tar.gz; then + if build_prep https://github.com/LPCIC/elpi/archive v1.11.0 tar.gz 1 elpi; then - log2 make build DUNE_OPTS="-p elpi" - log2 make install DUNE_OPTS="-p elpi" + log2 dune build -p elpi + log2 dune install elpi build_post @@ -1712,10 +1711,8 @@ function make_addon_menhir { touch "$FLAGFILES/menhir-addon.started" # Menhir executable install_glob "$PREFIXOCAML/bin" 'menhir.exe' "$PREFIXCOQ/bin/" - # Menhir Standard library - install_glob "$PREFIXOCAML/share/menhir/" '*.mly' "$PREFIXCOQ/share/menhir/" # Menhir PDF doc - install_glob "$PREFIXOCAML/share/doc/menhir/" '*.pdf' "$PREFIXCOQ/doc/menhir/" + install_glob "$PREFIXOCAML/doc/menhir/" '*.pdf' "$PREFIXCOQ/doc/menhir/" touch "$FLAGFILES/menhir-addon.finished" LOGTARGET=other installer_addon_end @@ -1730,7 +1727,8 @@ function make_addon_menhirlib { if build_prep_overlay menhirlib; then installer_addon_section menhirlib "Menhirlib" "Coq support library for using Menhir generated parsers in Coq" "" # The supplied makefiles don't work in any way on cygwin - cd src + # ToDo: dune also doesn't seem to work for the coq files + cd coq-menhirlib/src echo -R . MenhirLib > _CoqProject ls -1 *.v >> _CoqProject log1 coq_makefile -f _CoqProject -o Makefile.coq @@ -1816,7 +1814,7 @@ function make_addon_coquelicot { installer_addon_dependency_end if build_prep_overlay coquelicot; then installer_addon_section coquelicot "Coquelicot" "Coq library for real analysis" "" - logn autogen ./autogen.sh + log1 autoreconf -i -s logn configure ./configure --libdir="$PREFIXCOQ/lib/coq/user-contrib/Coquelicot" logn remake ./remake logn remake-install ./remake install @@ -1882,7 +1880,7 @@ function make_addon_quickchick { function make_addon_flocq { if build_prep_overlay flocq; then installer_addon_section flocq "Flocq" "Coq library for floating point arithmetic" "" - log1 autoconf + log1 autoreconf logn configure ./configure logn remake ./remake --jobs=$MAKE_THREADS logn install ./remake install @@ -1901,7 +1899,7 @@ function make_addon_interval { installer_addon_dependency_end if build_prep_overlay interval; then installer_addon_section interval "Interval" "Coq library and tactic for proving real inequalities" "" - logn autogen ./autogen.sh + log1 autoreconf logn configure ./configure logn remake ./remake --jobs=$MAKE_THREADS logn install ./remake install @@ -1930,7 +1928,9 @@ function make_addon_gappa_tool { install_boost if build_prep_overlay gappa_tool; then installer_addon_section gappa_tool "Gappa tool" "Stand alone tool for automated generation of numerical arithmetic proofs" "" - logn autogen ./autogen.sh + log1 autoreconf + # Note: configure.in seems to reference this file + touch stamp-config_h.in logn configure ./configure --build="$HOST" --host="$HOST" --target="$TARGET" --prefix="$PREFIXCOQ" logn remake ./remake --jobs=$MAKE_THREADS logn install ./remake -d install @@ -1947,7 +1947,7 @@ function make_addon_gappa { installer_addon_dependency_end if build_prep_overlay gappa_plugin ; then installer_addon_section gappa "Gappa plugin" "Coq plugin for the Gappa tool" "" - logn autogen ./autogen.sh + log1 autoreconf logn configure ./configure logn remake ./remake logn install ./remake install diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 4ebc637a68..9737e1b2e0 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -283,8 +283,9 @@ ######################################################################## # menhirlib ######################################################################## +# Note: menhirlib is now in subfolder coq-menhirlib of menhir : "${menhirlib_CI_REF:=master}" -: "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/coq-menhirlib}" +: "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/menhir}" : "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}" ######################################################################## @@ -13,7 +13,7 @@ dune-dbg.in ../checker/coqchk.bc ../topbin/coqc_bin.bc - ../ide/coqide_main.bc + ../ide/coqide/coqide_main.bc ; We require all the OCaml libs to be in place and searchable ; by OCamlfind, this is a bit of a hack but until Dune gets ; proper ocamldebug support we have to live with that. diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 498f167eb1..47dfbad3a0 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -8,7 +8,7 @@ case $1 in ;; coqide) shift - exe=_build/default/ide/coqide_main.bc + exe=_build/default/ide/coqide/coqide_main.bc ;; coqc) shift diff --git a/doc/changelog/04-tactics/12423-rm-info.rst b/doc/changelog/04-tactics/12423-rm-info.rst new file mode 100644 index 0000000000..bf20453e6b --- /dev/null +++ b/doc/changelog/04-tactics/12423-rm-info.rst @@ -0,0 +1,2 @@ +- **Removed:** Removed info tactic that was deprecated in 8.5. + (`#12423 <https://github.com/coq/coq/pull/12423>`_, by Jim Fehrle). diff --git a/doc/changelog/10-standard-library/12484-fix12483.rst b/doc/changelog/10-standard-library/12484-fix12483.rst deleted file mode 100644 index 95e7c150a3..0000000000 --- a/doc/changelog/10-standard-library/12484-fix12483.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Fix the specification of :n:`PrimFloat.leb` which made - :n:`(x <= y)%float` true for any non NaN :n:`x` and :n:`y`. - (`#12484 <https://github.com/coq/coq/pull/12484>`_, - fixes `#12483 <https://github.com/coq/coq/issues/12483>`_, - by Pierre Roux). diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 12fd038fb6..b0ef792bd1 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -361,6 +361,7 @@ it is an atomic universe (i.e. not an algebraic max() universe). to the sort :g:`Set` and only collapses floating universes between themselves. +.. _explicit-universes: Explicit Universes ------------------- @@ -387,7 +388,7 @@ to universes and explicitly instantiate polymorphic definitions. Polymorphic Universe @ident In the monorphic case, this command declares a new global universe - named :g:`ident`, which can be referred to using its qualified name + named :token:`ident`, which can be referred to using its qualified name as well. Global universe names live in a separate namespace. The command supports the :attr:`universes(polymorphic)` attribute (or the ``Polymorphic`` prefix) only in sections, meaning the universe diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 51c80e697e..8427300dc4 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -96,6 +96,16 @@ Changes in 8.12+beta1 .. contents:: :local: +Kernel +^^^^^^ + +- **Fixed:** + Specification of :n:`PrimFloat.leb` which made + :n:`(x <= y)%float` true for any non NaN :n:`x` and :n:`y`. + (`#12484 <https://github.com/coq/coq/pull/12484>`_, + fixes `#12483 <https://github.com/coq/coq/issues/12483>`_, + by Pierre Roux). + Specification language, type inference ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -1040,8 +1050,9 @@ Reference manual `#11423 <https://github.com/coq/coq/pull/11423>`_, `#11705 <https://github.com/coq/coq/pull/11705>`_, `#11718 <https://github.com/coq/coq/pull/11718>`_, - `#11720 <https://github.com/coq/coq/pull/11720>`_ - and `#11961 <https://github.com/coq/coq/pull/11961>`_, by Jim + `#11720 <https://github.com/coq/coq/pull/11720>`_, + `#11961 <https://github.com/coq/coq/pull/11961>`_ + and `#12103 <https://github.com/coq/coq/pull/12103>`_, by Jim Fehrle, reviewed by Théo Zimmermann). - **Added:** A glossary of terms and an index of attributes @@ -1068,10 +1079,11 @@ Reference manual `#11720 <https://github.com/coq/coq/pull/11720>`_ `#11797 <https://github.com/coq/coq/pull/11797>`_, `#11913 <https://github.com/coq/coq/pull/11913>`_, - `#11958 <https://github.com/coq/coq/pull/11958>`_ - `#11960 <https://github.com/coq/coq/pull/11960>`_ - and `#11961 <https://github.com/coq/coq/pull/11961>`_, by Jim - Fehrle, reviewed by Théo Zimmermann). + `#11958 <https://github.com/coq/coq/pull/11958>`_, + `#11960 <https://github.com/coq/coq/pull/11960>`_, + `#11961 <https://github.com/coq/coq/pull/11961>`_ + and `#12103 <https://github.com/coq/coq/pull/12103>`_, by Jim + Fehrle, reviewed by Théo Zimmermann and Jason Gross). Infrastructure and dependencies ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index 9943e0aa76..955f48b772 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -44,10 +44,11 @@ fun and forall gets identical. Moreover, parentheses can be omitted in the case of a single sequence of bindings sharing the same type (e.g.: :g:`fun (x y z : A) => t` can be shortened in :g:`fun x y z : A => t`). -.. index:: fun ... => ... +.. index:: fun +.. index:: forall -Abstractions: fun ------------------ +Functions (fun) and function types (forall) +------------------------------------------- .. insertprodn term_forall_or_fun term_forall_or_fun @@ -69,11 +70,6 @@ a let-binder occurs in the list of binders, it is expanded to a let-in definition (see Section :ref:`let-in`). -.. index:: forall - -Products: forall ----------------- - The expression :n:`forall @ident : @type, @term` denotes the *product* of the variable :n:`@ident` of type :n:`@type`, over the term :n:`@term`. As for abstractions, :g:`forall` is followed by a binder list, and products @@ -92,8 +88,8 @@ Non dependent product types have a special notation: :g:`A -> B` stands for :g:`forall _ : A, B`. The *non dependent product* is used both to denote the propositional implication and function types. -Applications ------------- +Function application +-------------------- .. insertprodn term_application arg diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index d7f7259ab0..64b29c1c0b 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -417,8 +417,16 @@ more precise description of the scope of these settings): .. FIXME Convert "Extraction Language" to an option. -Flags, options and tables are identified by a series of identifiers, each with an initial -capital letter. +.. insertprodn setting_name setting_name + +.. prodn:: + setting_name ::= {+ @ident } + +.. + + Flags, options and tables are identified by a series of + identifiers. By convention, each of the identifiers start with an + initial capital letter. Flags, options and tables appear in the HTML documentation in blue or gray boxes after the labels "Flag", "Option" and "Table". In the pdf, @@ -428,11 +436,6 @@ they appear after a boldface label. They are listed in the .. cmd:: Set @setting_name {? {| @int | @string } } :name: Set - .. insertprodn setting_name setting_name - - .. prodn:: - setting_name ::= {+ @ident } - If :n:`@setting_name` is a flag, no value may be provided; the flag is set to on. If :n:`@setting_name` is an option, a value of the appropriate type @@ -533,4 +536,4 @@ Newly opened modules and sections inherit the current settings. :cmd:`Unset` commands. If your goal is to define project-wide settings, you should rather use the command-line arguments ``-set`` and ``-unset`` for setting flags and options - (cf. :ref:`command-line-options`). + (see :ref:`command-line-options`). diff --git a/doc/sphinx/language/core/sorts.rst b/doc/sphinx/language/core/sorts.rst index 03581b95dd..3517d70005 100644 --- a/doc/sphinx/language/core/sorts.rst +++ b/doc/sphinx/language/core/sorts.rst @@ -30,14 +30,16 @@ and :math:`\Set`. The sort :math:`\Prop` intends to be the type of logical propositions. If :math:`M` is a logical proposition then it denotes the class of terms representing -proofs of :math:`M`. An object :math:`m` belonging to :math:`M` witnesses the fact that :math:`M` is -provable. An object of type :math:`\Prop` is called a proposition. +proofs of :math:`M`. An object :math:`m` belonging to :math:`M` +:term:`witnesses <witness>` the fact that :math:`M` is +provable. An object of type :math:`\Prop` is called a :gdef:`proposition`. We denote propositions by :n:`@form`. This constitutes a semantic subclass of the syntactic class :n:`@term`. The sort :math:`\SProp` is like :math:`\Prop` but the propositions in :math:`\SProp` are known to have irrelevant proofs (all proofs are -equal). Objects of type :math:`\SProp` are called strict propositions. +equal). Objects of type :math:`\SProp` are called +:gdef:`strict propositions <strict proposition>`. See :ref:`sprop` for information about using :math:`\SProp`, and :cite:`Gilbert:POPL2019` for meta theoretical considerations. @@ -66,12 +68,12 @@ Formally, we call :math:`\Sort` the set of sorts which is defined by: \Sort \equiv \{\SProp,\Prop,\Set,\Type(i)\;|\; i~∈ ℕ\} -Their properties, such as: :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and -:math:`\Type(i):\Type(i+1)`, are defined in Section :ref:`subtyping-rules`. +Their properties, such as :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and +:math:`\Type(i):\Type(i+1)`, are described in :ref:`subtyping-rules`. The user does not have to mention explicitly the index :math:`i` when -referring to the universe :math:`\Type(i)`. One only writes :math:`\Type`. The system -itself generates for each instance of :math:`\Type` a new index for the +referring to the universe :math:`\Type(i)`. One only writes `Type`. The system +itself generates for each instance of `Type` a new index for the universe and checks that the constraints between these indexes can be solved. From the user point of view we consequently have :math:`\Type:\Type`. We shall make precise in the typing rules the constraints between the @@ -81,8 +83,8 @@ indices. .. _Implementation-issues: **Implementation issues** In practice, the Type hierarchy is -implemented using *algebraic -universes*. An algebraic universe :math:`u` is either a variable (a qualified +implemented using algebraic universes. +An :gdef:`algebraic universe` :math:`u` is either a variable (a qualified identifier with a number) or a successor of an algebraic universe (an expression :math:`u+1`), or an upper bound of algebraic universes (an expression :math:`\max(u_1 ,...,u_n )`), or the base universe (the expression @@ -94,6 +96,6 @@ constraints between the universe variables is maintained globally. To ensure the existence of a mapping of the universes to the positive integers, the graph of constraints must remain acyclic. Typing expressions that violate the acyclicity of the graph of constraints -results in a Universe inconsistency error. +results in a :exn:`Universe inconsistency` error. -.. seealso:: :ref:`printing-universes`. +.. seealso:: :ref:`printing-universes`, :ref:`explicit-universes`. diff --git a/lib/future.ml b/lib/future.ml index 661637fcd1..23d089fb6b 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -67,8 +67,8 @@ and 'a computation = 'a comput ref let unnamed = "unnamed" -let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x = - ref (Ongoing (name, CEphemeron.create (uuid, f, ref x))) +let create ?(name=unnamed) ?(uuid=UUID.fresh ()) ~fix_exn x = + ref (Ongoing (name, CEphemeron.create (uuid, fix_exn, ref x))) let get x = match !x with | Finished v -> unnamed, UUID.invalid, id, ref (Val v) @@ -97,9 +97,7 @@ let peek_val kx = let _, _, _, x = get kx in match !x with let uuid kx = let _, id, _, _ = get kx in id -let from_val ?(fix_exn=id) v = create fix_exn (Val v) - -let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn +let from_val v = create ~fix_exn:id (Val v) let create_delegate ?(blocking=true) ~name fix_exn = let assignment signal ck = fun v -> @@ -116,7 +114,7 @@ let create_delegate ?(blocking=true) ~name fix_exn = let cond = Condition.create () in (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock), (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in - let ck = create ~name fix_exn (Delegated wait) in + let ck = create ~name ~fix_exn (Delegated wait) in ck, assignment signal ck (* TODO: get rid of try/catch to be stackless *) @@ -143,12 +141,12 @@ let force x = match compute x with let chain ck f = let name, uuid, fix_exn, c = get ck in - create ~uuid ~name fix_exn (match !c with + create ~uuid ~name ~fix_exn (match !c with | Closure _ | Delegated _ -> Closure (fun () -> f (force ck)) | Exn _ as x -> x | Val v -> Val (f v)) -let create fix_exn f = create fix_exn (Closure f) +let create ~fix_exn f = create ~fix_exn (Closure f) let replace kx y = let _, _, _, x = get kx in diff --git a/lib/future.mli b/lib/future.mli index 7a85c37970..612a67f962 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -47,21 +47,11 @@ type fix_exn = Exninfo.iexn -> Exninfo.iexn by forcing the computations or any computation that is chained after it. It is used by STM to attach errors to their corresponding states, and to communicate to the code catching the exception a valid state id. *) -val create : fix_exn -> (unit -> 'a) -> 'a computation +val create : fix_exn:fix_exn -> (unit -> 'a) -> 'a computation (* Usually from_val is used to create "fake" futures, to use the same API - as if a real asynchronous computations was there. In this case fixing - the exception is not needed, but *if* the future is chained, the fix_exn - argument should really be given *) -val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation - -(* To get the fix_exn of a computation and build a Lemmas.declaration_hook. - * When a future enters the environment a corresponding hook is run to perform - * some work. If this fails, then its failure has to be annotated with the - * same state id that corresponds to the future computation end. I.e. Qed - * is split into two parts, the lazy one (the future) and the eager one - * (the hook), both performing some computations for the same state id. *) -val fix_exn_of : 'a computation -> fix_exn + as if a real asynchronous computations was there. *) +val from_val : 'a -> 'a computation (* Run remotely, returns the function to assign. If not blocking (the default) it raises NotReady if forced before the diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 0e661543db..996f6b3eb3 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -173,8 +173,7 @@ GRAMMAR EXTEND Gram { TacFun (it,body) } | "let"; isrec = [IDENT "rec" -> { true } | -> { false } ]; llc = LIST1 let_clause SEP "with"; "in"; - body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } - | IDENT "info"; tc = tactic_expr LEVEL "5" -> { TacInfo tc } ] ] + body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ] ; (* Tactic arguments to the right of an application *) tactic_arg_compat: diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index d74e981c6d..6233807016 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -642,7 +642,6 @@ let pr_goal_selector ~toplevel s = let lcall = 1 let leval = 1 let ltatom = 1 - let linfo = 5 let level_of p = match p with LevelLe n -> n | LevelLt n -> n-1 | LevelSome -> lseq @@ -988,11 +987,6 @@ let pr_goal_selector ~toplevel s = keyword "infoH" ++ spc () ++ pr_tac (LevelLe ltactical) t), ltactical - | TacInfo t -> - hov 1 ( - keyword "info" ++ spc () - ++ pr_tac (LevelLe ltactical) t), - linfo | TacOr (t1,t2) -> hov 1 ( pr_tac (LevelLt lorelse) t1 ++ spc () diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index b77fb3acc7..b261096b63 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -225,7 +225,6 @@ and 'a gen_tactic_expr = 'a gen_tactic_expr * Id.t option | TacId of 'n message_token list | TacFail of global_flag * int or_var * 'n message_token list - | TacInfo of 'a gen_tactic_expr | TacLetIn of rec_flag * (lname * 'a gen_tactic_arg) list * 'a gen_tactic_expr diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index cfa224319c..650349b586 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -224,7 +224,6 @@ and 'a gen_tactic_expr = 'a gen_tactic_expr * Id.t option | TacId of 'n message_token list | TacFail of global_flag * int or_var * 'n message_token list - | TacInfo of 'a gen_tactic_expr | TacLetIn of rec_flag * (lname * 'a gen_tactic_arg) list * 'a gen_tactic_expr diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index bcfdb5318e..afa79a88db 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -649,7 +649,6 @@ and intern_tactic_seq onlytac ist = function | TacDo (n,tac) -> ist.ltacvars, TacDo (intern_int_or_var ist n,intern_pure_tactic ist tac) | TacTry tac -> ist.ltacvars, TacTry (intern_pure_tactic ist tac) - | TacInfo tac -> ist.ltacvars, TacInfo (intern_pure_tactic ist tac) | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_pure_tactic ist tac) | TacTimeout (n,tac) -> ist.ltacvars, TacTimeout (intern_int_or_var ist n,intern_tactic onlytac ist tac) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 97f7a198e6..705a1a62ce 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1035,13 +1035,6 @@ let type_uconstr ?(flags = (constr_flags ())) understand_ltac flags env sigma vars expected_type term end -let warn_deprecated_info = - CWarnings.create ~name:"deprecated-info-tactical" ~category:"deprecated" - (fun () -> - strbrk "The general \"info\" tactic is currently not working." ++ spc()++ - strbrk "There is an \"Info\" command to replace it." ++fnl () ++ - strbrk "Some specific verbose tactics may also exist, such as info_eauto.") - (* Interprets an l-tac expression into a value *) let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftactic.t = (* The name [appl] of applied top-level Ltac names is ignored in @@ -1154,9 +1147,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l) | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac) | TacArg a -> interp_tactic ist (TacArg a) - | TacInfo tac -> - warn_deprecated_info (); - eval_tactic ist tac | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) | TacAlias {loc; v=(s,l)} -> diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index ed298b7e66..c2f1589b74 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -200,7 +200,6 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacTimeout (n,tac) -> TacTimeout (n,subst_tactic subst tac) | TacTime (s,tac) -> TacTime (s,subst_tactic subst tac) | TacTry tac -> TacTry (subst_tactic subst tac) - | TacInfo tac -> TacInfo (subst_tactic subst tac) | TacRepeat tac -> TacRepeat (subst_tactic subst tac) | TacOr (tac1,tac2) -> TacOr (subst_tactic subst tac1,subst_tactic subst tac2) diff --git a/stm/stm.ml b/stm/stm.ml index 04f08e488b..b72cee7a9d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -830,8 +830,6 @@ module State : sig ?redefine:bool -> ?cache:bool -> ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit - val fix_exn_ref : (Exninfo.iexn -> Exninfo.iexn) ref - val install_cached : Stateid.t -> unit (* val install_parsing_state : Stateid.t -> unit *) val is_cached : ?cache:bool -> Stateid.t -> bool @@ -865,8 +863,6 @@ end = struct (* {{{ *) (* cur_id holds Stateid.dummy in case the last attempt to define a state * failed, so the global state may contain garbage *) let cur_id = ref Stateid.dummy - let fix_exn_ref = ref (fun x -> x) - let freeze () = { id = !cur_id; vernac_state = Vernacstate.freeze_interp_state ~marshallable:false } let unfreeze st = Vernacstate.unfreeze_interp_state st.vernac_state; @@ -1001,10 +997,7 @@ end = struct (* {{{ *) try stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^ if cache then "Y)" else "N)"); - let good_id = match safe_id with None -> !cur_id | Some id -> id in - fix_exn_ref := exn_on id ~valid:good_id; f (); - fix_exn_ref := (fun x -> x); if cache then cache_state ~marshallable:false id; stm_prerr_endline (fun () -> "setting cur id to "^str_id); cur_id := id; @@ -1495,7 +1488,9 @@ end = struct (* {{{ *) feedback (InProgress ~-1) let build_proof_here ~doc ?loc ~drop_pt (id,valid) eop = - Future.create (State.exn_on id ~valid) (fun () -> + (* [~fix_exn:exn_on] here does more than amending the exn + information, it also updates the STM state *) + Future.create ~fix_exn:(State.exn_on id ~valid) (fun () -> let wall_clock1 = Unix.gettimeofday () in Reach.known_state ~doc ~cache:(VCS.is_interactive ()) eop; let wall_clock2 = Unix.gettimeofday () in @@ -1509,38 +1504,45 @@ end = struct (* {{{ *) try VCS.restore document; VCS.print (); - let proof, future_proof, time = + let proof, time = let wall_clock = Unix.gettimeofday () in let fp = build_proof_here ~doc:dummy_doc (* XXX should be document *) ?loc ~drop_pt:drop exn_info stop in let proof = Future.force fp in - proof, fp, Unix.gettimeofday () -. wall_clock in + proof, Unix.gettimeofday () -. wall_clock in (* We typecheck the proof with the kernel (in the worker) to spot * the few errors tactics don't catch, like the "fix" tactic building * a bad fixpoint *) - let fix_exn = Future.fix_exn_of future_proof in (* STATE: We use the current installed imperative state *) let st = State.freeze () in if not drop then begin - let checked_proof = Future.chain future_proof (fun p -> - - (* Unfortunately close_future_proof and friends are not pure so we need - to set the state manually here *) + (* Unfortunately close_future_proof and friends are not pure so we need + to set the state manually here *) State.unfreeze st; let pobject, _info = - PG_compat.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in + PG_compat.close_future_proof ~feedback_id:stop (Future.from_val proof) in let st = Vernacstate.freeze_interp_state ~marshallable:false in let opaque = Declare.Opaque in - stm_qed_delay_proof ~st ~id:stop - ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))) in - ignore(Future.join checked_proof); - end; + try + let _pstate = + stm_qed_delay_proof ~st ~id:stop + ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None)) in + () + with exn -> + (* If [stm_qed_delay_proof] fails above we need to use the + exn callback in the same way than build_proof_here; + actually [fix_exn] there does more more than just + modifying exn info, it also updates the STM state *) + let iexn = Exninfo.capture exn in + let iexn = State.exn_on (fst exn_info) ~valid:(snd exn_info) iexn in + Exninfo.iraise iexn + end; (* STATE: Restore the state XXX: handle exn *) State.unfreeze st; RespBuiltProof(proof,time) with | e when CErrors.noncritical e || e = Stack_overflow -> - let (e, info) = Exninfo.capture e in + let e, info = Exninfo.capture e in (* This can happen if the proof is broken. The error has also been * signalled as a feedback, hence we can silently recover *) let e_error_at, e_safe_id = match Stateid.get info with @@ -3310,7 +3312,6 @@ let unreachable_state_hook = Hooks.unreachable_state_hook let document_add_hook = Hooks.document_add_hook let document_edit_hook = Hooks.document_edit_hook let sentence_exec_hook = Hooks.sentence_exec_hook -let () = Declare.Obls.stm_get_fix_exn := (fun () -> !State.fix_exn_ref) type document = VCS.vcs let backup () = VCS.backup () diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 315c42097d..65f79b6a51 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -490,12 +490,18 @@ let assert_before_gen b naming t = let assert_before na = assert_before_gen false (naming_of_name na) let assert_before_replacing id = assert_before_gen true (NamingMustBe (CAst.make id)) -let assert_after_then_gen b naming t tac = +let replace_error_option err tac = + match err with + | None -> tac + | Some (e, info) -> + Proofview.tclORELSE tac (fun _ -> Proofview.tclZERO ~info e) + +let assert_after_then_gen ?err b naming t tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> let id = find_name b (LocalAssum (make_annot Anonymous Sorts.Relevant,t)) naming gl in Tacticals.New.tclTHENFIRST - (internal_cut_rev b id t) + (replace_error_option err (internal_cut_rev b id t)) (tac id) end @@ -1366,7 +1372,7 @@ let do_replace id = function [Ti] and the first one (resp last one) being [G] whose hypothesis [id] is replaced by P using the proof given by [tac] *) -let clenv_refine_in with_evars targetid id sigma0 clenv tac = +let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac = let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in let clenv = { clenv with evd = Typeclasses.resolve_typeclasses @@ -1383,7 +1389,7 @@ let clenv_refine_in with_evars targetid id sigma0 clenv tac = Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd)) (Tacticals.New.tclTHENLAST - (assert_after_then_gen with_clear naming new_hyp_typ tac) exact_tac) + (assert_after_then_gen ?err with_clear naming new_hyp_typ tac) exact_tac) (********************************************) (* Elimination tactics *) @@ -1668,24 +1674,28 @@ let descend_in_conjunctions avoid tac (err, info) c = let (_, elim) = build_case_analysis_scheme env sigma (ind,u) false sort in let elim = EConstr.of_constr elim in NotADefinedRecordUseScheme elim in - Tacticals.New.tclORELSE0 - (Tacticals.New.tclFIRST - (List.init n (fun i -> + let or_tac t1 t2 e = Proofview.tclORELSE (t1 e) t2 in + List.fold_right or_tac + (List.init n (fun i (err, info) -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in match make_projection env sigma params cstr sign elim i n c u with | None -> - let info = Exninfo.reify () in - Tacticals.New.tclFAIL ~info 0 (mt()) + Proofview.tclZERO ~info err | Some (p,pt) -> Tacticals.New.tclTHENS - (assert_before_gen false (NamingAvoid avoid) pt) - [refiner ~check:true EConstr.Unsafe.(to_constr p); + (Proofview.tclORELSE + (assert_before_gen false (NamingAvoid avoid) pt) + (fun _ -> Proofview.tclZERO ~info err)) + [Proofview.tclORELSE + (refiner ~check:true EConstr.Unsafe.(to_constr p)) + (fun _ -> Proofview.tclZERO ~info err); (* Might be ill-typed due to forbidden elimination. *) - Tacticals.New.onLastHypId (tac (not isrec))] - end))) - (Proofview.tclZERO ~info err) + Tacticals.New.onLastHypId (tac (err, info) (not isrec))] + end)) + (fun (err, info) -> Proofview.tclZERO ~info err) + (err, info) | None -> Proofview.tclZERO ~info err with RefinerError _|UserError _ -> Proofview.tclZERO ~info err end @@ -1750,7 +1760,7 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars let tac = if with_destruct then descend_in_conjunctions Id.Set.empty - (fun b id -> + (fun _ b id -> Tacticals.New.tclTHEN (try_main_apply b (mkVar id)) (clear [id])) @@ -1879,7 +1889,7 @@ let apply_in_once ?(respect_opaque = false) with_delta let t' = Tacmach.New.pf_get_hyp_typ id gl in let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in let targetid = find_name true (LocalAssum (make_annot Anonymous Sorts.Relevant,t')) naming gl in - let rec aux idstoclear with_destruct c = + let rec aux ?err idstoclear with_destruct c = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -1891,18 +1901,17 @@ let apply_in_once ?(respect_opaque = false) with_delta if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in try let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in - clenv_refine_in with_evars targetid id sigma clause + clenv_refine_in ?err with_evars targetid id sigma clause (fun id -> - Tacticals.New.tclTHENLIST [ - apply_clear_request clear_flag false c; - clear idstoclear; - tac id - ]) + replace_error_option err ( + apply_clear_request clear_flag false c <*> + clear idstoclear) <*> + tac id) with e when with_destruct && CErrors.noncritical e -> - let (e, info) = Exninfo.capture e in + let err = Option.default (Exninfo.capture e) err in (descend_in_conjunctions (Id.Set.singleton targetid) - (fun b id -> aux (id::idstoclear) b (mkVar id)) - (e, info) c) + (fun err b id -> aux ~err (id::idstoclear) b (mkVar id)) + err c) end in aux [] with_destruct d diff --git a/test-suite/interactive/ParalITP_fail_on_qed.v b/test-suite/interactive/ParalITP_fail_on_qed.v new file mode 100644 index 0000000000..37692ed254 --- /dev/null +++ b/test-suite/interactive/ParalITP_fail_on_qed.v @@ -0,0 +1,54 @@ +(* Some boilerplate *) +Fixpoint fib n := match n with + | O => 1 + | S m => match m with + | O => 1 + | S o => fib o + fib m end end. + +Ltac sleep n := + try (cut (fib n = S (fib n)); reflexivity). + +(* Tune that depending on your PC *) +Let time := 10. + + +(* Beginning of demo *) + +Section Demo. + +Variable i : True. + +Lemma a (n : nat) : nat. +Proof using. + revert n. + fix f 1. + apply f. +Qed. + +Lemma b : True. +Proof using i. + sleep time. + idtac. + sleep time. + (* Here we use "a" *) + exact I. +Qed. + +Lemma work_here : True /\ True. +Proof using i. +(* Jump directly here, Coq reacts immediately *) +split. + exact b. (* We can use the lemmas above *) +exact I. +Qed. + +End Demo. + +From Coq Require Import Program.Tactics. +Obligation Tactic := idtac. +Program Definition foo : nat -> nat * nat := + fix f (n : nat) := (0,_). + +Next Obligation. +intros f n; apply (f n). +Qed. diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 4c0ee1b5bd..767b3c1922 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -23,11 +23,11 @@ Module Pair (X: PO) (Y: PO) <: PO. Hint Unfold le. Lemma le_refl : forall p : T, le p p. - info auto. + auto. Qed. Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3. - unfold le; intuition; info eauto. + unfold le; intuition; eauto. Qed. Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2. @@ -39,9 +39,9 @@ Module Pair (X: PO) (Y: PO) <: PO. enough (t0 = t2) as ->. reflexivity. - info auto. + auto. - info auto. + auto. Qed. End Pair. @@ -53,5 +53,5 @@ Require Nat. Module NN := Pair Nat Nat. Lemma zz_min : forall p : NN.T, NN.le (0, 0) p. - info auto with arith. + auto with arith. Qed. diff --git a/test-suite/output/auto.v b/test-suite/output/auto.v index 92917cdfc7..7b295dd1cb 100644 --- a/test-suite/output/auto.v +++ b/test-suite/output/auto.v @@ -1,4 +1,4 @@ -(* testing info/debug auto/eauto *) +(* testing info_*/debug auto/eauto *) Goal False \/ (True -> True). info_auto. diff --git a/test-suite/output/bug12442.out b/test-suite/output/bug12442.out new file mode 100644 index 0000000000..644ef6cd7c --- /dev/null +++ b/test-suite/output/bug12442.out @@ -0,0 +1,6 @@ +The command has indeed failed with message: +No product even after head-reduction. +The command has indeed failed with message: +Not an inductive product. +The command has indeed failed with message: +Not an inductive product. diff --git a/test-suite/output/bug12442.v b/test-suite/output/bug12442.v new file mode 100644 index 0000000000..481989a4e9 --- /dev/null +++ b/test-suite/output/bug12442.v @@ -0,0 +1,10 @@ +Parameter A B : Prop. +Axiom P : inhabited (A -> B). + +Goal A -> True. +Proof. + Fail intros ?%P ?. + Fail intros []%P. + intro a. + Fail apply P in a as []. +Abort. diff --git a/vernac/declare.ml b/vernac/declare.ml index e3144b2d24..59922c662a 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -140,9 +140,9 @@ let default_univ_entry = Entries.Monomorphic_entry Univ.ContextSet.empty (** [univsbody] are universe-constraints attached to the body-only, used in vio-delayed opaque constants and private poly universes *) -let definition_entry_core ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types +let definition_entry_core ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body = - { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff); + { proof_entry_body = Future.from_val ((body,univsbody), eff); proof_entry_secctx = section_vars; proof_entry_type = types; proof_entry_universes = univs; @@ -151,7 +151,7 @@ let definition_entry_core ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id proof_entry_inline_code = inline} let definition_entry = - definition_entry_core ?fix_exn:None ?eff:None ?univsbody:None ?feedback_id:None ?section_vars:None + definition_entry_core ?eff:None ?univsbody:None ?feedback_id:None ?section_vars:None type proof_object = { name : Names.Id.t @@ -369,9 +369,9 @@ let record_aux env s_ty s_bo = (keep_hyps env s_bo)) in Aux_file.record_in_aux "context_used" v -let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types +let pure_definition_entry ?(opaque=false) ?(inline=false) ?types ?(univs=default_univ_entry) body = - { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), ()); + { proof_entry_body = Future.from_val ((body,Univ.ContextSet.empty), ()); proof_entry_secctx = None; proof_entry_type = types; proof_entry_universes = univs; @@ -504,17 +504,6 @@ let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd = let () = register_constant kn kind local in kn -let get_cd_fix_exn = function - | DefinitionEntry de -> - Future.fix_exn_of de.proof_entry_body - | _ -> fun x -> x - -let declare_constant ?local ~name ~kind cd = - try declare_constant ?local ~name ~kind cd - with exn -> - let exn = Exninfo.capture exn in - Exninfo.iraise (get_cd_fix_exn cd exn) - let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind de = let kn, eff = let de = @@ -1010,29 +999,22 @@ let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe = let () = Hook.(call ?hook { S.uctx; obls = []; scope; dref}) in dref -let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = - try declare_assumption ~name ~scope ~hook ~impargs ~uctx pe - with exn -> - let exn = Exninfo.capture exn in - let exn = Option.cata (fun fix -> fix exn) exn fix_exn in - Exninfo.iraise exn - (* Preparing proof entries *) -let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma = +let prepare_definition ?opaque ?inline ~poly ~udecl ~types ~body sigma = let env = Global.env () in Pretyping.check_evars_are_solved ~program_mode:false env sigma; let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true sigma (fun nf -> nf body, Option.map nf types) in let univs = Evd.check_univ_decl ~poly sigma udecl in - let entry = definition_entry_core ?fix_exn ?opaque ?inline ?types ~univs body in + let entry = definition_entry ?opaque ?inline ?types ~univs body in let uctx = Evd.evar_universe_context sigma in entry, uctx let declare_definition_core ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook - ~obls ~poly ?inline ~types ~body ?fix_exn sigma = - let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in + ~obls ~poly ?inline ~types ~body sigma = + let entry, uctx = prepare_definition ~opaque ~poly ~udecl ~types ~body ?inline sigma in declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry let declare_definition = declare_definition_core ~obls:[] @@ -1454,8 +1436,6 @@ let subst_prog subst prg = ( Vars.replace_vars subst' prg.prg_body , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_type ) -let stm_get_fix_exn = ref (fun _ x -> x) - let declare_definition prg = let varsubst = obligation_substitution true prg in let sigma = Evd.from_ctx prg.prg_ctx in @@ -1471,12 +1451,11 @@ let declare_definition prg = , Decls.(IsDefinition prg.prg_kind) , prg.prg_implicits ) in - let fix_exn = !stm_get_fix_exn () in let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in (* XXX: This is doing normalization twice *) let kn = declare_definition_core ~name ~scope ~kind ~impargs ?hook ~obls - ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma + ~opaque ~poly ~udecl ~types ~body sigma in let pm = progmap_remove !State.prg_ref prg in State.prg_ref := pm; diff --git a/vernac/declare.mli b/vernac/declare.mli index ef4f8c4825..979bdd4334 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -305,13 +305,11 @@ val declare_definition -> ?inline:bool -> types:EConstr.t option -> body:EConstr.t - -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> Evd.evar_map -> GlobRef.t val declare_assumption - : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) - -> name:Id.t + : name:Id.t -> scope:locality -> hook:Hook.t option -> impargs:Impargs.manual_implicits @@ -495,11 +493,6 @@ val obl_substitution : val dependencies : Obligation.t array -> int -> Int.Set.t -(* 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 - * is not available here, so we provide a side channel to get it *) -val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) ref - end (** Creating high-level proofs with an associated constant *) |