-------------------------------------------------------------------------------- Fedora Update Notification FEDORA-2021-8b73a471c5 2021-06-22 01:01:06.903138 --------------------------------------------------------------------------------
Name : flocq Product : Fedora 34 Version : 3.4.0 Release : 5.fc34 URL : http://flocq.gforge.inria.fr/ Summary : Formalization of floating point numbers for Coq Description : Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq. -------------------------------------------------------------------------------- Update Information: Changes in coq 8.13.2: - Fix crash when using `vm_compute` on an irreducible `PArray.set` - Fix crash when loading `.vo` files containing a `vm_compute` normalized primitive array - Fix `Ltac2.Array.init` computational complexity Changes in ocaml-menhir 20210310: - Menhir now detects and rejects grammars that have a cycle and grammars that exhibit hidden left recursion. A grammar has a cycle when a nonterminal symbol `A` expands (in one or more steps) to itself. This implies that the grammar is ambiguous. A grammar has hidden left recursion when a nonterminal symbol `A` expands (in one step) to `B beta`, where `B` expands (in zero or more steps) to nothing and `beta` expands (in zero or more steps) to `A ...`. This implies that the grammar is not in the class `LR(k)` for any value of `k`. Both of these anomalies create a shift/reduce conflict which, if resolved in favor of reduction, leads to a nonterminating parser. - Disallow the escape sequence `\n` in a token alias. It was allowed by mistake. Disallowing it ensures that the `## Concrete syntax:` comments generated as part of `.messages` files fit on a single line. - Internal changes in the expansion of `%inline` symbols, eliminating certain useless variable renamings that would appear in semantic actions after expansion. - Internal changes in the code back-end, eliminating certain useless bindings of variables to a unit value. Changes in ocaml-menhir 20210419: - Mention the demo `coq- minicalc` in the manual. - Parsers generated with the Coq mode now have support for non-certified basic error reporting without an additional parser. This is supported thanks to an extension of the return type `parse_result` in the coq- menhirlib library and thanks to the new generated helper function `Aut.N_of_state`. See the new demo `coq-syntax-errors` and the updated manual for more details. (Contributed by Brian Ward.) All other builds are simple rebuilds due to the changes above. -------------------------------------------------------------------------------- ChangeLog: * Tue Jun 8 2021 Jerry James <[email protected]> - 3.4.0-5 - Rebuild for coq 8.13.2 -------------------------------------------------------------------------------- This update can be installed with the "dnf" update program. Use su -c 'dnf upgrade --advisory FEDORA-2021-8b73a471c5' at the command line. For more information, refer to the dnf documentation available at http://dnf.readthedocs.io/en/latest/command_ref.html#upgrade-command-label All packages are signed with the Fedora Project GPG key. More details on the GPG keys used by the Fedora Project can be found at https://fedoraproject.org/keys -------------------------------------------------------------------------------- _______________________________________________ package-announce mailing list -- [email protected] To unsubscribe send an email to [email protected] Fedora Code of Conduct: https://docs.fedoraproject.org/en-US/project/code-of-conduct/ List Guidelines: https://fedoraproject.org/wiki/Mailing_list_guidelines List Archives: https://lists.fedoraproject.org/archives/list/[email protected] Do not reply to spam on the list, report it: https://pagure.io/fedora-infrastructure
