From 76965645274d33b2b102a5b5f77a19b2c955bd5a Mon Sep 17 00:00:00 2001 From: Brent Yorgey Date: Sat, 21 Dec 2024 21:25:52 -0600 Subject: [PATCH] More RTD fixes (#416) Fix the RTD configuration and a bunch of warnings. --- .readthedocs.yaml | 5 +++++ docs/introduction/files.rst | 1 - docs/reference/addition.rst | 6 +++--- docs/reference/collection-ops.rst | 2 +- docs/reference/compare.rst | 2 +- docs/reference/multiplication.rst | 2 +- docs/reference/natural.rst | 2 +- docs/reference/no-search.rst | 2 +- docs/reference/not-qual.rst | 2 +- docs/reference/numeric.rst | 2 +- docs/reference/operator.rst | 6 +++--- docs/reference/pattern-type.rst | 2 +- docs/reference/prop.rst | 19 +++++++++++-------- docs/reference/size.rst | 2 +- docs/reference/sum-type.rst | 2 +- docs/reference/types.rst | 3 +-- docs/reference/variable.rst | 2 +- docs/requirements.txt | 3 +++ docs/tutorial/typedefs.rst | 1 - 19 files changed, 37 insertions(+), 29 deletions(-) delete mode 100644 docs/introduction/files.rst create mode 100644 docs/requirements.txt diff --git a/.readthedocs.yaml b/.readthedocs.yaml index 0a1ab4e3..07650466 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -10,6 +10,11 @@ build: tools: python: "3.12" +# Explicitly set the version of Python and its requirements +python: + install: + - requirements: docs/requirements.txt + # Build documentation in the "docs/" directory with Sphinx sphinx: configuration: docs/conf.py diff --git a/docs/introduction/files.rst b/docs/introduction/files.rst deleted file mode 100644 index 7dd42e69..00000000 --- a/docs/introduction/files.rst +++ /dev/null @@ -1 +0,0 @@ -WITHIN A FILE, A VARIABLE CAN ONLY HAVE ONE VALUE diff --git a/docs/reference/addition.rst b/docs/reference/addition.rst index 7b1f247e..95664a8d 100644 --- a/docs/reference/addition.rst +++ b/docs/reference/addition.rst @@ -4,8 +4,8 @@ Addition .. note:: This page concerns the ``+`` operator on numbers; for the ``+`` - operator on :doc:`types `, see :doc:`sum types `; - or see the ``+`` (``overlay``) operator on :doc:`graphs `. + operator on :doc:`types `, see :doc:`sum types `; + or see the ``+`` (``overlay``) operator on :doc:`graphs `. Values of all :doc:`numeric types ` can be added using the ``+`` operator. For example: @@ -25,6 +25,6 @@ If you ask for the :doc:`type ` of ``+``, you get ~+~ : ℕ × ℕ → ℕ which says that it is a :doc:`function ` taking :doc:`a pair -of ` natural numbers and returning a natural number. +of ` natural numbers and returning a natural number. However, as mentioned above, it also works on other numeric types such as integers and rational numbers. diff --git a/docs/reference/collection-ops.rst b/docs/reference/collection-ops.rst index 8873b9f8..5bc1acb7 100644 --- a/docs/reference/collection-ops.rst +++ b/docs/reference/collection-ops.rst @@ -1,5 +1,5 @@ Collection operations -==================== +===================== The :doc:`Cartesian product ` of two collections (:doc:`finite sets `, :doc:`lists `, or :doc:`bags `) can be found diff --git a/docs/reference/compare.rst b/docs/reference/compare.rst index b8fead2a..bd96546e 100644 --- a/docs/reference/compare.rst +++ b/docs/reference/compare.rst @@ -20,7 +20,7 @@ can be compared: See the individual pages about each type for more information on how comparison works on values of that type. -:doc:`Functions `, on the other hand, cannot be +:doc:`Functions `, on the other hand, cannot be compared, because in general this would require testing the functions on every single possible input, of which there might be infinitely many. diff --git a/docs/reference/multiplication.rst b/docs/reference/multiplication.rst index d06bbec5..0ad13ac7 100644 --- a/docs/reference/multiplication.rst +++ b/docs/reference/multiplication.rst @@ -5,7 +5,7 @@ Multiplication This page concerns the ``*`` operator on numbers; for the ``*`` operator on :doc:`types `, see :doc:`pair types - `; or see the ``*`` (``connect``) operator on :doc:`graphs `. + `; or see the ``*`` (``connect``) operator on :doc:`graphs `. All :doc:`numeric types ` can be multiplied using the ``*`` operator. For example: diff --git a/docs/reference/natural.rst b/docs/reference/natural.rst index 68ea4d03..37e44efe 100644 --- a/docs/reference/natural.rst +++ b/docs/reference/natural.rst @@ -17,7 +17,7 @@ counting numbers 0, 1, 2, 3, 4, 5, ... 6 : ℕ Natural numbers cannot be directly :doc:`subtracted ` or -:doc:`divided `. However, ``N`` is a :doc:`subtype` of all +:doc:`divided `. However, ``N`` is a :doc:`subtypes` of all the other numeric types, so using subtraction or division with natural numbers will cause them to be automatically converted into a different type like :doc:`integers ` or :doc:`rationals diff --git a/docs/reference/no-search.rst b/docs/reference/no-search.rst index 05e4b9d3..799669a7 100644 --- a/docs/reference/no-search.rst +++ b/docs/reference/no-search.rst @@ -1,7 +1,7 @@ The type T is not searchable ============================ -When writing a :doc:`property ` using a ``forall``, we are +When writing a :doc:`property ` using a ``forall``, we are only allowed to use types which are *searchable*, that is, types for which we can effectively generate sample values. Note this is not the same thing as being finite. For example, the type of natural numbers diff --git a/docs/reference/not-qual.rst b/docs/reference/not-qual.rst index 420e6ba4..bc54b3c0 100644 --- a/docs/reference/not-qual.rst +++ b/docs/reference/not-qual.rst @@ -8,4 +8,4 @@ operations to types that do not allow that operation. For example: two :doc:`natural numbers ` - Trying to :doc:`compare ` two :doc:`functions - ` + ` diff --git a/docs/reference/numeric.rst b/docs/reference/numeric.rst index 14068b54..81184f5b 100644 --- a/docs/reference/numeric.rst +++ b/docs/reference/numeric.rst @@ -53,7 +53,7 @@ We can arrange the four numeric types in a diamond shape, like this: :alt: Diamond lattice :align: center -Each type is a subset, or :doc:`subtype`, of the type or types above +Each type is a subset, or :doc:`subtypes`, of the type or types above it. For example, the fact that :math:`\mathbb{N}` is below :math:`\mathbb{Z}` means that every natural number is also an integer. diff --git a/docs/reference/operator.rst b/docs/reference/operator.rst index 73f16310..d7d0d2d2 100644 --- a/docs/reference/operator.rst +++ b/docs/reference/operator.rst @@ -8,8 +8,8 @@ their two arguments, like ``1 + 2``. Disco has many built-in operators which are symbols (like ``+``, ``*``, ``/``, *etc.*) as well as a few which are words (like ``mod``, ``choose``, and ``divides``). -Disco also has three *unary* operators: :doc:`arithmetic negation ` (``-``) -and :doc:`logical negation ` (``¬`` or ``not``) are written in front of their +Disco also has three *unary* operators: :doc:`arithmetic negation ` (``-``) +and :doc:`logical negation ` (``¬`` or ``not``) are written in front of their one argument, and :doc:`factorial ` (``!``) is written after its argument. When multiple operators are used together, Disco uses their @@ -38,7 +38,7 @@ Note that in this case, we can write ``!`` or ``~!`` and Disco understands either one. The twiddle notation is also useful when giving an operator as an -argument to a :doc:`higher-order function `: +argument to a :doc:`higher-order function `: :: diff --git a/docs/reference/pattern-type.rst b/docs/reference/pattern-type.rst index f507f373..74ceea55 100644 --- a/docs/reference/pattern-type.rst +++ b/docs/reference/pattern-type.rst @@ -3,7 +3,7 @@ The pattern p is supposed to have type T, but instead... This is a similar sort of error as :doc:`notcon`, but concerns :doc:`patterns ` instead of :doc:`expressions `. -On the one hand, disco can figure out what :doc:`type ` a +On the one hand, disco can figure out what :doc:`type ` a pattern should be based on the type of the :doc:`function `. On the other hand, the pattern itself may correspond to a different type. For example, diff --git a/docs/reference/prop.rst b/docs/reference/prop.rst index a18700a3..f0390213 100644 --- a/docs/reference/prop.rst +++ b/docs/reference/prop.rst @@ -12,8 +12,8 @@ Any :doc:`Boolean ` expression can be used as a proposition. For example, ``T``, ``x > 5``, and ``(x < y) -> ((x == 2) \/ (x == 3))`` can all be used as propositions. -However, unlike Boolean expressions, propositions can use :doc:`quantifiers -`, that is, ``forall`` or ``exists``. For example, +However, unlike Boolean expressions, propositions can use +*quantifiers*, that is, ``forall`` or ``exists``. For example, ``forall x : Z. x^2 >= 0`` is a ``Prop`` (but not a ``Bool``). If you type a proposition at the Disco prompt, it will simply print @@ -23,12 +23,14 @@ whether a proposition is true or false, you have two options: - The built-in ``holds`` function tries its best to determine whether a proposition is true or false. If it returns a value at all, it is definitely correct. For example, - - ``holds ((5 < 3) \/ ((2 < 1) -> F))`` yields ``T`` - - ``holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (q \/ p))`` - yields ``T`` - - ``holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (p /\ q))`` - yields ``F`` - - ``holds (forall n:N. n < 529)`` yields ``F`` + + - ``holds ((5 < 3) \/ ((2 < 1) -> F))`` yields ``T`` + - ``holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (q \/ p))`` + yields ``T`` + - ``holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (p /\ q))`` + yields ``F`` + - ``holds (forall n:N. n < 529)`` yields ``F`` + However, sometimes it may simply get stuck in an infinite loop. For example, ``holds (forall n:N. n >= 0)`` will simply get stuck. Even though it is obvious to us that this proposition is true, ``holds`` @@ -41,6 +43,7 @@ whether a proposition is true or false, you have two options: output much more information than a simple ``T`` or ``F``, for example, showing a counterexample if a ``forall`` is false, or a witness if an ``exists`` is true. For example, + - ``:test forall p:Bool. forall q:Bool. (p \/ q) <-> (p /\ q)`` prints diff --git a/docs/reference/size.rst b/docs/reference/size.rst index 28eafe0d..e8ab36d0 100644 --- a/docs/reference/size.rst +++ b/docs/reference/size.rst @@ -1,7 +1,7 @@ Size ==== -The *size* of a :doc:`collection ` ``c`` (a :doc:`list +The *size* of a :doc:`collection ` ``c`` (a :doc:`list `, :doc:`bag `, or :doc:`set `) can be found using the notation ``|c|``. For example, diff --git a/docs/reference/sum-type.rst b/docs/reference/sum-type.rst index 80a98a7d..04dc177d 100644 --- a/docs/reference/sum-type.rst +++ b/docs/reference/sum-type.rst @@ -23,7 +23,7 @@ Sum types Note that the ``left`` or ``right`` ensures that ``A + B`` really does represent a *disjoint* union. For example, although the usual -:doc:`union ` operator is idempotent, that is, +:doc:`union ` operator is idempotent, that is, :math:`\mathbb{N} \cup \mathbb{N} = \mathbb{N}`, with a disjoint union of types ``N + N`` is not at all the same as ``N``. Elements of ``N + N`` look like either ``left(3)`` or ``right(3)``, that is, ``N + N`` diff --git a/docs/reference/types.rst b/docs/reference/types.rst index e7773ce2..092ff675 100644 --- a/docs/reference/types.rst +++ b/docs/reference/types.rst @@ -33,10 +33,9 @@ is a :doc:`subtype ` of the one it was expecting. type-sig type-annot polymorphism - type-annot algebraic-types typedef - collection-types + collections string prop subtypes diff --git a/docs/reference/variable.rst b/docs/reference/variable.rst index b9e5f2d0..e1cf6e40 100644 --- a/docs/reference/variable.rst +++ b/docs/reference/variable.rst @@ -8,7 +8,7 @@ a letter. For example, ``myHorse3``, ``some_name``, and ``X__17'x'_`` are all valid variable names. To define a variable, one must first use a :doc:`type signature -` to declare its :doc:`type` on a line by itself, like +` to declare its :doc:`type ` on a line by itself, like :: diff --git a/docs/requirements.txt b/docs/requirements.txt new file mode 100644 index 00000000..6f3aeb81 --- /dev/null +++ b/docs/requirements.txt @@ -0,0 +1,3 @@ +sphinx==7.2.6 +sphinx-rtd-theme==3.0.2 +sphinx-notfound-page==1.0.4 diff --git a/docs/tutorial/typedefs.rst b/docs/tutorial/typedefs.rst index ee3aa4c0..b4575029 100644 --- a/docs/tutorial/typedefs.rst +++ b/docs/tutorial/typedefs.rst @@ -70,7 +70,6 @@ Type definitions can also be parameterized. For example, we can make the ``Tree`` type polymorphic: .. literalinclude:: example/tydefs-poly.disco - :language: idris :caption: ::