diff options
| -rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 34 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 3 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/core/assumptions.rst | 16 | ||||
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 19 | ||||
| -rw-r--r-- | doc/sphinx/language/core/sorts.rst | 24 |
6 files changed, 51 insertions, 48 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}" ######################################################################## 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/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`. |