-------------------------------------------------------------------------------- Fedora Update Notification FEDORA-2021-8b73a471c5 2021-06-22 01:01:06.903138 --------------------------------------------------------------------------------
Name : zenon Product : Fedora 34 Version : 0.8.4 Release : 23.fc34 URL : http://zenon-prover.org/ Summary : Automated theorem prover for first-order classical logic Description : Zenon is an automated theorem prover for first order classical logic with equality, based on the tableau method. Zenon can read input files in TPTP, Coq, Focal, and its own Zenon format. Zenon can directly generate Coq proofs (proof scripts or proof terms), which can be reinserted into Coq specifications. Zenon can also be extended. -------------------------------------------------------------------------------- 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]> - 0.8.4-23 - 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
