{"update": {"autokarma": false, "autotime": false, "stable_karma": 3, "stable_days": 0, "unstable_karma": -3, "require_bugs": false, "require_testcases": false, "display_name": "", "notes": "This update removes an obsolete ExcludeArch tag from ocaml-zip.  Besides ocaml-zip, flocq and why3, the other updates are just rebuilds due to the updated packages.\r\n\r\nChanges in flocq 2.4.0:\r\n- moved some lemmas from Fcalc_digits to Fcore_digits and made them axiom-free\r\n- added theorems about double rounding being innocuous (Fappli_double_round.v)\r\n- improved a bit the efficiency of IEEE-754 arithmetic\r\n\r\nChanges in why3 0.84:\r\n\r\nTools:\r\n- file generated by \"why3session html f.mlw\" is now \"f/why3session.html\" and not \"f/f.html\"\r\n- the default behavior of why3 has been moved to the \"prove\" subcommand\r\n- options --exec, --extract, and --realize, have been moved to subcommands: execute, extract, and realize\r\n- why3replayer has been moved to the \"replay\" subcommand\r\n- other tools have been moved to why3 subcommands too: config, doc, ide, session, wc; for local usage, the old commands are still available\r\n\r\nProof sessions:\r\n- session files are split in two parts: \"why3session.xml\" and \"why3shapes\". The latter file contains the checksums and the shapes for the goals. That second file is not strictly needed for replaying a proof session, it is only useful when input programs are modified, to track obsolete goals. If Why3 is compiled with compression support (provided by ocamlzip library) then files for shapes are compressed into why3shapes.gz.\r\n\r\nLibrary:\r\n- renamed array.ArraySorted -> array.IntArraySorted. array.ArraySorted is now generic, with type and order relation parameters\r\n- reduced amount of \"use export\" in the standard library: theories now only export the symbols they define. Users may need to insert more \"use import\" in their theories (typically int.Int, option.Option, list.List, etc.).\r\n\r\nProvers:\r\n- fixed Coq printer (former Coq proofs may have to be updated, by removing non-emptiness constraints from polymorphic type applications)\r\n- support for Coq8.4pl4\r\n- support for Isabelle2014\r\n- support for CVC4 1.4\r\n- updated support for TPTP TFA syntax (used by provers Beagle and Princess)\r\n\r\nTransformations:\r\n- new transformation \"compute_in_goal\" that simplifies the goal, by computation, as much as possible\r\n\r\nChanges in why3 0.85:\r\n\r\nLanguage:\r\n- fix a soundness bug in the detection of aliases when calling a WhyML function: some alias could have been forgotten when a type variable was substituted with a mutable type\r\n\r\nSessions:\r\n- use the full path of identifiers when the user introduces namespaces (BTS #17181)\r\n\r\nTransformations:\r\n- fix a soundness bug in \"compute_in_goal\" regarding the handling of logical implication.\r\n- several improvements to \"compute_in_goal\":\r\n    - left-hand side of rewrite rules can be any symbols, not only non-interpreted ones.\r\n    - perform beta-reduction when possible\r\n    - the maximal number of reduction steps can be increased using meta \"compute_max_steps\"\r\n    - the transformation is documented in details in the manual\r\n- new transformation \"compute_specified\":\r\n    - less aggressive variant of \"compute_in_goal\"\r\n    - Unfolding of definitions is controlled using meta \"rewrite_def\"\r\n- fixed a bug in \"eliminate_if\" when applied on inductive definitions\r\n\r\nProvers:\r\n- fixed wrong warning when detecting Isabelle2014\r\n", "type": "enhancement", "status": "stable", "request": null, "severity": "unspecified", "suggest": "unspecified", "locked": false, "pushed": true, "critpath": false, "critpath_groups": null, "close_bugs": true, "date_submitted": "2014-09-08 21:20:02", "date_modified": "2014-09-19 04:18:49", "date_approved": null, "date_testing": "2014-09-19 17:44:24", "date_stable": "2014-09-23 04:33:15", "alias": "FEDORA-2014-10505", "test_gating_status": null, "from_tag": null, "date_pushed": "2014-09-23 04:33:15", "meets_testing_requirements": false, "url": "https://bodhi.stg.fedoraproject.org/updates/FEDORA-2014-10505", "title": "flocq-2.4.0-1.fc21 frama-c-1.10-18.fc21 gappalib-coq-1.0.0-12.fc21 ocaml-zip-1.05-4.fc21 why-2.34-10.fc21 why3-0.85-2.fc21", "version_hash": "7a1fcd139767366d9f81105ee0ad63977b0b8903", "release": {"name": "F21", "long_name": "Fedora 21", "version": "21", "id_prefix": "FEDORA", "branch": "f21", "dist_tag": "f21", "stable_tag": "f21-updates", "testing_tag": "f21-updates-testing", "candidate_tag": "f21-updates-candidate", "pending_signing_tag": "", "pending_testing_tag": "f21-updates-testing-pending", "pending_stable_tag": "f21-updates-pending", "override_tag": "f21-override", "mail_template": "fedora_errata_template", "state": "archived", "composed_by_bodhi": true, "create_automatic_updates": null, "package_manager": "dnf", "testing_repository": "updates-testing", "released_on": null, "eol": null, "critpath_mandatory_days_in_testing": 14, "mandatory_days_in_testing": 7, "critpath_min_karma": 2, "min_karma": 1, "setting_status": null}, "user": {"name": "jjames", "email": "loganjerry@gmail.com", "id": 339, "avatar": "https://seccdn.libravatar.org/avatar/258caf5973a37959eeea9164bfc32d49b0634d0792e85fce1f5acf0430f05ba2?s=24&d=retro", "openid": "jjames.id.stg.fedoraproject.org", "groups": [{"name": "packager"}, {"name": "provenpackager"}, {"name": "ipausers"}, {"name": "fedora-contributor"}, {"name": "signed_fpca"}, {"name": "fedorabugs"}, {"name": "trust admins"}]}, "comments": [{"karma": 0, "karma_critpath": 0, "text": "This update has been submitted for testing by jjames. ", "timestamp": "2014-09-08 21:20:09", "update_id": 27448, "user_id": 91, "id": 216105, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "bodhi", "email": null, "id": 91, "avatar": "https://apps.fedoraproject.org/img/icons/bodhi-24.png", "openid": "bodhi.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "AutoQA: depcheck test PASSED on i386. Result log:\nhttp://autoqa.fedoraproject.org/report/1fy5h (results are informative only)", "timestamp": "2014-09-08 21:47:52", "update_id": 27448, "user_id": 234, "id": 216106, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "autoqa", "email": null, "id": 234, "avatar": "https://seccdn.libravatar.org/avatar/37a8eec1ce19687d132fe29051dca629d164e2c4958ba141d5f4133a33f0688f?s=24&d=retro", "openid": "autoqa.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "AutoQA: depcheck test PASSED on x86_64. Result log:\nhttp://autoqa.fedoraproject.org/report/1fy5q (results are informative only)", "timestamp": "2014-09-08 21:50:06", "update_id": 27448, "user_id": 234, "id": 216107, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "autoqa", "email": null, "id": 234, "avatar": "https://seccdn.libravatar.org/avatar/37a8eec1ce19687d132fe29051dca629d164e2c4958ba141d5f4133a33f0688f?s=24&d=retro", "openid": "autoqa.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "This update is currently being pushed to the Fedora 21 testing updates repository.", "timestamp": "2014-09-10 01:20:31", "update_id": 27448, "user_id": 91, "id": 216108, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "bodhi", "email": null, "id": 91, "avatar": "https://apps.fedoraproject.org/img/icons/bodhi-24.png", "openid": "bodhi.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "This update has been pushed to testing", "timestamp": "2014-09-10 02:13:05", "update_id": 27448, "user_id": 91, "id": 216109, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "bodhi", "email": null, "id": 91, "avatar": "https://apps.fedoraproject.org/img/icons/bodhi-24.png", "openid": "bodhi.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "This update has reached 3 days in testing and can be pushed to stable now if the maintainer wishes", "timestamp": "2014-09-13 03:15:04", "update_id": 27448, "user_id": 91, "id": 216110, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "bodhi", "email": null, "id": 91, "avatar": "https://apps.fedoraproject.org/img/icons/bodhi-24.png", "openid": "bodhi.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "This update has been submitted for stable by jjames. ", "timestamp": "2014-09-15 19:32:20", "update_id": 27448, "user_id": 91, "id": 216111, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "bodhi", "email": null, "id": 91, "avatar": "https://apps.fedoraproject.org/img/icons/bodhi-24.png", "openid": "bodhi.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "AutoQA: upgradepath test PASSED on noarch. Result log:\nhttp://autoqa.fedoraproject.org/report/1gerg (results are informative only)", "timestamp": "2014-09-15 21:45:23", "update_id": 27448, "user_id": 234, "id": 216112, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "autoqa", "email": null, "id": 234, "avatar": "https://seccdn.libravatar.org/avatar/37a8eec1ce19687d132fe29051dca629d164e2c4958ba141d5f4133a33f0688f?s=24&d=retro", "openid": "autoqa.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "jjames has edited this update. New build(s): frama-c-1.10-18.fc21, why-2.34-10.fc21, why3-0.85-2.fc21. Removed build(s): frama-c-1.10-16.fc21, why-2.34-9.fc21, why3-0.84-1.fc21.", "timestamp": "2014-09-19 04:10:16", "update_id": 27448, "user_id": 91, "id": 216113, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "bodhi", "email": null, "id": 91, "avatar": "https://apps.fedoraproject.org/img/icons/bodhi-24.png", "openid": "bodhi.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "This update has been submitted for testing by jjames. ", "timestamp": "2014-09-19 04:10:47", "update_id": 27448, "user_id": 91, "id": 216114, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "bodhi", "email": null, "id": 91, "avatar": "https://apps.fedoraproject.org/img/icons/bodhi-24.png", "openid": "bodhi.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "AutoQA: depcheck test PASSED on i386. Result log:\nhttp://autoqa.fedoraproject.org/report/1gs9u (results are informative only)", "timestamp": "2014-09-19 04:27:54", "update_id": 27448, "user_id": 234, "id": 216115, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "autoqa", "email": null, "id": 234, "avatar": "https://seccdn.libravatar.org/avatar/37a8eec1ce19687d132fe29051dca629d164e2c4958ba141d5f4133a33f0688f?s=24&d=retro", "openid": "autoqa.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "AutoQA: depcheck test PASSED on x86_64. Result log:\nhttp://autoqa.fedoraproject.org/report/1gs9w (results are informative only)", "timestamp": "2014-09-19 04:29:47", "update_id": 27448, "user_id": 234, "id": 216116, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "autoqa", "email": null, "id": 234, "avatar": "https://seccdn.libravatar.org/avatar/37a8eec1ce19687d132fe29051dca629d164e2c4958ba141d5f4133a33f0688f?s=24&d=retro", "openid": "autoqa.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "This update is currently being pushed to the Fedora 21 testing updates repository.", "timestamp": "2014-09-19 15:53:49", "update_id": 27448, "user_id": 91, "id": 216117, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "bodhi", "email": null, "id": 91, "avatar": "https://apps.fedoraproject.org/img/icons/bodhi-24.png", "openid": "bodhi.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "This update has been pushed to testing", "timestamp": "2014-09-19 17:44:24", "update_id": 27448, "user_id": 91, "id": 216118, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "bodhi", "email": null, "id": 91, "avatar": "https://apps.fedoraproject.org/img/icons/bodhi-24.png", "openid": "bodhi.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "This update has been submitted for stable by jjames. ", "timestamp": "2014-09-22 19:38:29", "update_id": 27448, "user_id": 91, "id": 216119, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "bodhi", "email": null, "id": 91, "avatar": "https://apps.fedoraproject.org/img/icons/bodhi-24.png", "openid": "bodhi.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "AutoQA: upgradepath test PASSED on noarch. Result log:\nhttp://autoqa.fedoraproject.org/report/1h729 (results are informative only)", "timestamp": "2014-09-22 23:46:56", "update_id": 27448, "user_id": 234, "id": 216120, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "autoqa", "email": null, "id": 234, "avatar": "https://seccdn.libravatar.org/avatar/37a8eec1ce19687d132fe29051dca629d164e2c4958ba141d5f4133a33f0688f?s=24&d=retro", "openid": "autoqa.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "This update is currently being pushed to the Fedora 21 stable updates repository.", "timestamp": "2014-09-23 03:35:30", "update_id": 27448, "user_id": 91, "id": 216121, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "bodhi", "email": null, "id": 91, "avatar": "https://apps.fedoraproject.org/img/icons/bodhi-24.png", "openid": "bodhi.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "This update is currently being pushed to the Fedora 21 stable updates repository.", "timestamp": "2014-09-23 03:49:59", "update_id": 27448, "user_id": 91, "id": 216122, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "bodhi", "email": null, "id": 91, "avatar": "https://apps.fedoraproject.org/img/icons/bodhi-24.png", "openid": "bodhi.id.stg.fedoraproject.org", "groups": []}}, {"karma": 0, "karma_critpath": 0, "text": "This update has been pushed to stable", "timestamp": "2014-09-23 04:33:15", "update_id": 27448, "user_id": 91, "id": 216123, "bug_feedback": [], "testcase_feedback": [], "user": {"name": "bodhi", "email": null, "id": 91, "avatar": "https://apps.fedoraproject.org/img/icons/bodhi-24.png", "openid": "bodhi.id.stg.fedoraproject.org", "groups": []}}], "builds": [{"nvr": "flocq-2.4.0-1.fc21", "signed": true, "release_id": null, "type": "rpm", "epoch": null}, {"nvr": "frama-c-1.10-18.fc21", "signed": true, "release_id": null, "type": "rpm", "epoch": null}, {"nvr": "gappalib-coq-1.0.0-12.fc21", "signed": true, "release_id": null, "type": "rpm", "epoch": null}, {"nvr": "ocaml-zip-1.05-4.fc21", "signed": true, "release_id": null, "type": "rpm", "epoch": null}, {"nvr": "why-2.34-10.fc21", "signed": true, "release_id": null, "type": "rpm", "epoch": null}, {"nvr": "why3-0.85-2.fc21", "signed": true, "release_id": null, "type": "rpm", "epoch": null}], "bugs": [], "updateid": "FEDORA-2014-10505", "karma": 0, "content_type": "rpm", "test_cases": []}, "can_edit": false, "ci_allowed": false}