diff options
Diffstat (limited to 'doc')
11 files changed, 129 insertions, 25 deletions
diff --git a/doc/changelog/02-specification-language/12121-master+fix11903-warn-non-truly-fixpoint.rst b/doc/changelog/02-specification-language/12121-master+fix11903-warn-non-truly-fixpoint.rst new file mode 100644 index 0000000000..d69a94205f --- /dev/null +++ b/doc/changelog/02-specification-language/12121-master+fix11903-warn-non-truly-fixpoint.rst @@ -0,0 +1,5 @@ +- **Added:** + New warning on using :cmd:`Fixpoint` or :cmd:`CoFixpoint` for + definitions which are not recursive + (`#12121 <https://github.com/coq/coq/pull/12121>`_, + by Hugo Herbelin) diff --git a/doc/changelog/03-notations/12163-fix-12159.rst b/doc/changelog/03-notations/12163-fix-12159.rst new file mode 100644 index 0000000000..978ed561dd --- /dev/null +++ b/doc/changelog/03-notations/12163-fix-12159.rst @@ -0,0 +1,11 @@ +- **Fixed:** + Numeral Notations now play better with multiple scopes for the same + inductive type. Previously, when multiple numeral notations were defined + for the same inductive, only the last one was considered for + printing. Now, among the notations that are usable for printing and either + have a scope delimiter or are open, the selection is made according + to the order of open scopes, or according to the last defined + notation if no appropriate scope is open + (`#12163 <https://github.com/coq/coq/pull/12163>`_, + fixes `#12159 <https://github.com/coq/coq/pull/12159>`_, + by Pierre Roux, review by Hugo Herbelin and Jason Gross). diff --git a/doc/changelog/09-coqide/12068-master+coqide-completion-no-matched.rst b/doc/changelog/09-coqide/12068-master+coqide-completion-no-matched.rst new file mode 100644 index 0000000000..dbb4bdecab --- /dev/null +++ b/doc/changelog/09-coqide/12068-master+coqide-completion-no-matched.rst @@ -0,0 +1,5 @@ +- **Fixed:** + New patch presumably fixing the random Coq 8.11 segfault issue with CoqIDE completion + (`#12068 <https://github.com/coq/coq/pull/12068>`_, + by Hugo Herbelin, presumably fixing + `#11943 <https://github.com/coq/coq/pull/11943>`_). diff --git a/doc/changelog/10-standard-library/12121-master+fix11903-warn-non-truly-fixpoint.rst b/doc/changelog/10-standard-library/12121-master+fix11903-warn-non-truly-fixpoint.rst new file mode 100644 index 0000000000..f22fff0736 --- /dev/null +++ b/doc/changelog/10-standard-library/12121-master+fix11903-warn-non-truly-fixpoint.rst @@ -0,0 +1,5 @@ +- **Fixed:** + :cmd:`Fixpoint`\s of the standard library without a recursive call turned + into ordinary :cmd:`Definition`\s + (`#12121 <https://github.com/coq/coq/pull/12121>`_, + by Hugo Herbelin; fixes `#11903 <https://github.com/coq/coq/pull/11903>`_). diff --git a/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst b/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst new file mode 100644 index 0000000000..37aaf697b5 --- /dev/null +++ b/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst @@ -0,0 +1,4 @@ +- **Added:** + new lemmas in ``List``: ``incl_map``, ``incl_filter``, ``NoDup_filter``, ``incl_Forall_in_iff`` + (`#12237 <https://github.com/coq/coq/pull/12237>`_, + by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12263-fix-haskell-extraction.rst b/doc/changelog/10-standard-library/12263-fix-haskell-extraction.rst new file mode 100644 index 0000000000..c80a070181 --- /dev/null +++ b/doc/changelog/10-standard-library/12263-fix-haskell-extraction.rst @@ -0,0 +1,9 @@ +- **Fixed:** + In Haskell extraction with ``ExtrHaskellString``, equality comparisons on + strings and characters are now guaranteed to be uniquely well-typed, even in + very polymorphic contexts under ``unsafeCoerce``; this is achieved by adding + type annotations to the extracted code, and by making ``ExtrHaskellString`` + export ``ExtrHaskellBasic`` (`#12263 + <https://github.com/coq/coq/pull/12263>`_, fixes `#12257 + <https://github.com/coq/coq/issues/12257>`_ and `#12258 + <https://github.com/coq/coq/issues/12258>`_, by Jason Gross). diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index e5af39c8fb..b125d21a3c 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1108,6 +1108,75 @@ between universes for inductive types in the Type hierarchy. Check infinite_loop (lam (@id Lam)) : False. +.. example:: Non strictly positive occurrence + + It is less obvious why inductive type definitions with occurences + that are positive but not strictly positive are harmful. + We will see that in presence of an impredicative type they + are unsound: + + .. coqtop:: all + + Fail Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A. + + If we were to accept this definition we could derive a contradiction + by creating an injective function from :math:`A → \Prop` to :math:`A`. + + This function is defined by composing the injective constructor of + the type :math:`A` with the function :math:`λx. λz. z = x` injecting + any type :math:`T` into :math:`T → \Prop`. + + .. coqtop:: none + + Unset Positivity Checking. + Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A. + Set Positivity Checking. + + .. coqtop:: all + + Definition f (x: A -> Prop): A := introA (fun z => z = x). + + .. coqtop:: in + + Lemma f_inj: forall x y, f x = f y -> x = y. + Proof. + unfold f; intros ? ? H; injection H. + set (F := fun z => z = y); intro HF. + symmetry; replace (y = x) with (F y). + + unfold F; reflexivity. + + rewrite <- HF; reflexivity. + Qed. + + The type :math:`A → \Prop` can be understood as the powerset + of the type :math:`A`. To derive a contradiction from the + injective function :math:`f` we use Cantor's classic diagonal + argument. + + .. coqtop:: all + + Definition d: A -> Prop := fun x => exists s, x = f s /\ ~s x. + Definition fd: A := f d. + + .. coqtop:: in + + Lemma cantor: (d fd) <-> ~(d fd). + Proof. + split. + + intros [s [H1 H2]]; unfold fd in H1. + replace d with s. + * assumption. + * apply f_inj; congruence. + + intro; exists d; tauto. + Qed. + + Lemma bad: False. + Proof. + pose cantor; tauto. + Qed. + + This derivation was first presented by Thierry Coquand and Christine + Paulin in :cite:`CP90`. + .. _Template-polymorphism: Template polymorphism diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 3b5233502d..cf4d432f64 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -90,9 +90,7 @@ list of assertion commands is given in :ref:`Assertions`. The command .. cmd:: Save @ident :name: Save - Forces the name of the original goal to be :token:`ident`. This - command can only be used if the original goal - was opened using the :cmd:`Goal` command. + Forces the name of the original goal to be :token:`ident`. .. cmd:: Admitted @@ -821,7 +819,7 @@ in compacted hypotheses: .. .. image:: ../_static/diffs-coqide-compacted.png - :alt: coqide with Set Diffs on with compacted hyptotheses + :alt: coqide with Set Diffs on with compacted hypotheses Controlling the effect of proof editing commands ------------------------------------------------ diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 28c5359a04..4be18ccda9 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -286,7 +286,7 @@ example, the null and all list function(al)s can be defined as follows: .. coqtop:: all Variable d: Set. - Fixpoint null (s : list d) := + Definition null (s : list d) := if s is nil then true else false. Variable a : d -> bool. Fixpoint all (s : list d) : bool := diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index a3fc069e6c..de0d912c03 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -48,28 +48,22 @@ def coqdoc(coq_code, coqdoc_bin=None): finally: os.remove(filename) -def is_whitespace_string(elem): - return isinstance(elem, NavigableString) and elem.strip() == "" - -def strip_soup(soup, pred): - """Strip elements matching pred from front and tail of soup.""" - while soup.contents and pred(soup.contents[-1]): - soup.contents.pop() - - skip = 0 - for elem in soup.contents: - if not pred(elem): - break - skip += 1 - - soup.contents[:] = soup.contents[skip:] +def first_string_node(node): + """Return the first string node, or None if does not exist""" + while node.children: + node = next(node.children) + if isinstance(node, NavigableString): + return node def lex(source): """Convert source into a stream of (css_classes, token_string).""" coqdoc_output = coqdoc(source) soup = BeautifulSoup(coqdoc_output, "html.parser") root = soup.find(class_='code') - strip_soup(root, is_whitespace_string) + # strip the leading '\n' + first = first_string_node(root) + if first and first.string[0] == '\n': + first.string.replace_with(first.string[1:]) for elem in root.children: if isinstance(elem, NavigableString): yield [], elem diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 9d51d2198a..df11960403 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -905,9 +905,13 @@ class CoqtopBlocksTransform(Transform): return isinstance(node, nodes.Element) and 'coqtop_options' in node @staticmethod - def split_sentences(source): - """Split Coq sentences in source. Could be improved.""" - return re.split(r"(?<=(?<!\.)\.)\s+", source) + def split_lines(source): + """Split Coq input in chunks + + A chunk is a minimal sequence of consecutive lines of the input that + ends with a '.' + """ + return re.split(r"(?<=(?<!\.)\.)\s+\n", source) @staticmethod def parse_options(node): @@ -986,7 +990,7 @@ class CoqtopBlocksTransform(Transform): repl.sendone('Unset Coqtop Exit On Error.') if options['warn']: repl.sendone('Set Warnings "default".') - for sentence in self.split_sentences(node.rawsource): + for sentence in self.split_lines(node.rawsource): pairs.append((sentence, repl.sendone(sentence))) if options['abort']: repl.sendone('Abort All.') |