{"bugs":[{"bugid":960866,"firstseen":"2025-07-30T18:55:20.998149","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/why3-for-spark-2023.12.13-r2 - [gcc-16] Error: The value json has type Yojson.Safe.t"},{"bugid":967149,"firstseen":"2025-12-06T15:00:12.000226","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/why3-for-spark-2023.12.13-r2 - [boost-1.89] Error: This pattern should not be a constructor, the expected type is"}],"categories":[{"categoryid":395,"name":"app-editors","summary":"The app-editors category contains text editors."},{"categoryid":450,"name":"dev-lang","summary":"The dev-lang category contains various programming language implementations and related tools."},{"categoryid":314,"name":"dev-ml","summary":"The dev-ml category contains libraries and utilities relevant to the ML programming language."},{"categoryid":377,"name":"dev-tex","summary":"The dev-tex category contains libraries and tools useful when working with TeX and TeX-based environments such as LaTeX."},{"categoryid":317,"name":"sci-mathematics","summary":"The sci-mathematics category contains mathematical software."}],"changelog":[{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"c44f57d8c04b9cbd60f13ac7c293df8cf2863021","committime":"2026-02-20T12:15:47","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Signed-off-by: Alfredo Tupone ","commitid":"994856d12bbcfe399d8c28845129162921999f49","committime":"2026-02-19T16:54:54","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: drop 2021-r1"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Signed-off-by: Alfredo Tupone ","commitid":"74623283f93eb2743f0cbee2829c76f219ecbbc0","committime":"2026-02-19T16:52:26","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: fix for Yojson-3"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"2e19d4248cd6db11e146f2d07dfb02603739e220","committime":"2026-01-05T12:15:58","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"eschwartz@gentoo.org","authorname":"Eli Schwartz","body":"Signed-off-by: Eli Schwartz ","commitid":"b97aca920fbbe2bfb462187d5cadfb217e80e7dd","committime":"2026-01-05T05:43:38","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: Stabilize 2023.12.13-r2 amd64, #966462"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"aae9881664608ab9a11ddc73c200475c7f1c10fb","committime":"2025-10-08T17:33:43","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Signed-off-by: Alfredo Tupone ","commitid":"c0d7884cb1f0a6c2536f632cb8b12313fe0b3c42","committime":"2025-10-08T17:23:35","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: dev-lang\/ocaml dep redundant"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"1cf6de06e7b1eaceb3db3665ad29c1307d20e724","committime":"2025-04-12T07:35:42","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Closes: https:\/\/bugs.gentoo.org\/945325\nSigned-off-by: Alfredo Tupone ","commitid":"67657d68adb49d8c57f3b0130f4a558aef3c6407","committime":"2025-04-12T07:15:19","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: fix for c23"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"d46194717d8382718e382e00d0e14b964691cf7e","committime":"2025-03-28T22:20:10","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Closes: https:\/\/bugs.gentoo.org\/952833\nSigned-off-by: Alfredo Tupone ","commitid":"cf7298ab4cd527f36975ba536d2e0dd80b65ff0d","committime":"2025-03-28T22:00:08","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: fix with ocaml-5"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"0400f6e927f9ca09ac0cc4c4cd4d5b59b586c662","committime":"2025-02-24T22:03:33","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Closes: https:\/\/bugs.gentoo.org\/949519\nSigned-off-by: Alfredo Tupone ","commitid":"0d918a1667cb6a0ec75028c5817de5bb9c0e750f","committime":"2025-02-24T21:53:35","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: fix configure"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"ff884300726278915795d0490fc129c6e97c501b","committime":"2025-02-11T17:18:27","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Signed-off-by: Alfredo Tupone ","commitid":"5180293d985699615c664fd41f6ca48e5d3db1ff","committime":"2025-02-11T17:08:37","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: fix for spark"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"2fba4c12629d4b108c15ad0cc37e607aabd0894f","committime":"2025-02-08T22:03:59","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Signed-off-by: Alfredo Tupone ","commitid":"25f41bc933d17176258a0cb7a2dcddb4b3008cb7","committime":"2025-02-08T21:52:55","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: keyword 2023.12.13-r1 for ~arm64"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"a965ec468de829e7a8d13baa4f30625402038904","committime":"2025-02-08T21:03:29","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Signed-off-by: Alfredo Tupone ","commitid":"0ce761414e3e10334c3f5b0494aafc5cb9761400","committime":"2025-02-08T20:37:40","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: requires older coq"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"f2584959e6b24cf7bd72b0a9928b738128f28ac3","committime":"2025-02-07T21:03:38","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Signed-off-by: Alfredo Tupone ","commitid":"1eea6c611d6f09b6e77a2f06fdc3bf201b1b4db4","committime":"2025-02-07T20:52:53","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: add 2023.12.13"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"2417548e5eb903a890aadc819a4741d0ed1c799c","committime":"2024-12-31T17:03:23","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"sam@gentoo.org","authorname":"Sam James","body":"Signed-off-by: Sam James ","commitid":"662149e4459da877c9f4262ed3d9138a494cf4f3","committime":"2024-12-31T16:49:38","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: update HOMEPAGE"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"5996e3a15d5d1412f578218c6b6b8cdb86b07b8f","committime":"2024-11-28T19:03:20","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Signed-off-by: Alfredo Tupone ","commitid":"920389a3a3ffaad8194fab02688d0c2f32217e13","committime":"2024-11-28T18:43:48","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: VariableOrderWrong"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"78976fc16d2a4e9d6d9868ad02f189bf4a0bcc68","committime":"2023-12-29T22:46:55","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Closes: https:\/\/bugs.gentoo.org\/913497\nSigned-off-by: Alfredo Tupone ","commitid":"d58c273f2681691ec5eaf8101e35730a2b9bc2e8","committime":"2023-12-29T22:42:59","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: require ocamlopt"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"f432eb5754913a619202b44bab20a500bdedfc97","committime":"2023-04-02T21:23:31","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Closes: https:\/\/bugs.gentoo.org\/883167\nSigned-off-by: Alfredo Tupone ","commitid":"8395f9bd24c6d239774bcc990eaaca63b9d77ef2","committime":"2023-04-02T21:04:18","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: disable shuffle"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"101e775be1d6d513e96c2e47fa96d62bdcd017ea","committime":"2023-04-02T14:31:50","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Signed-off-by: Alfredo Tupone ","commitid":"aea65604ea143ed47ffbb54c9628113ec26908c9","committime":"2023-04-02T14:22:42","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: drop 2020"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"a2a7acf2c3027ac7f306db102df3827907cfcfa8","committime":"2023-04-02T13:31:51","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Signed-off-by: Alfredo Tupone ","commitid":"2dd73ad05b6f04585994edc2ff4b79638ab28850","committime":"2023-04-02T13:20:59","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: stabilize 2021-r1 for amd64"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"0faf56173a554fb9f07b8e9cc76dde5dbbb5f2c4","committime":"2023-04-02T13:01:51","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Signed-off-by: Alfredo Tupone ","commitid":"dd5f5eb5b4c7b6262816c4fcc5edee33abfd9261","committime":"2023-04-02T12:48:09","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: drop 2019-r3"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"f2b132b9e3d780e6c92cdfb2c262a18b705d7851","committime":"2023-04-02T11:31:57","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Signed-off-by: Alfredo Tupone ","commitid":"e3e8e816e8945f661507f1235fd1779fe7039d35","committime":"2023-04-02T11:24:42","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: stabilize 2020 for amd64"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"67dfb2fd1b4882e04df740fa7a188cce7a84aab2","committime":"2023-03-31T13:16:50","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Signed-off-by: Alfredo Tupone ","commitid":"e361aafd702c08c1f382bcfe2006331603d6f526","committime":"2023-03-31T13:12:01","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: require lablgtk-2"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"1c321a4792e41f999262b5b3473680cc8bd2f761","committime":"2022-11-26T14:01:55","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Signed-off-by: Alfredo Tupone ","commitid":"132e6e560929e0b0f4df7d56fbc7d1fc223ac64a","committime":"2022-11-26T13:44:45","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: stop using \nPortage 3.0.34 \/ pkgdev 0.2.1 \/ pkgcheck 0.10.11\nCloses: https:\/\/github.com\/gentoo\/gentoo\/pull\/26610\nSigned-off-by: Alfredo Tupone ","commitid":"e6e9b60f9793c4d9b0d56f5a72d8edf5a286bf6b","committime":"2022-07-26T19:39:39","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: use https"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"f247b5e1239a191195648730d5798b86ccff0e81","committime":"2022-06-27T09:01:34","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Closes: https:\/\/bugs.gentoo.org\/854555\nPackage-Manager: Portage-3.0.30, Repoman-3.0.3\nSigned-off-by: Alfredo Tupone ","commitid":"57ec03f6bdbbbb51b2909aa42a8d93f8acd0c544","committime":"2022-06-27T08:47:05","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: refix QA_FLAGS"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"abc3e26029632e9c945dc9d8a4bfd1ac134868c4","committime":"2022-06-27T06:31:26","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Closes: https:\/\/bugs.gentoo.org\/837278\nPackage-Manager: Portage-3.0.30, Repoman-3.0.3\nSigned-off-by: Alfredo Tupone ","commitid":"641255d69acd7ef55105d2032ffb42d889ed5902","committime":"2022-06-27T06:19:33","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: ignore some QA warnings"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"af62e1071bd0470d853a6f0392b388dce15bc7e8","committime":"2022-03-11T21:19:58","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Closes: https:\/\/bugs.gentoo.org\/834881\nPackage-Manager: Portage-3.0.30, Repoman-3.0.3\nSigned-off-by: Alfredo Tupone ","commitid":"ed2328c4b86578b7b8f53c2c4a372718635f26f6","committime":"2022-03-11T21:00:38","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: add USE to select sexp"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"453c573844cce5b43fcc0bb229dc891de9bc3eeb","committime":"2022-02-07T22:06:54","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Closes: https:\/\/bugs.gentoo.org\/799245\nPackage-Manager: Portage-3.0.30, Repoman-3.0.3\nSigned-off-by: Alfredo Tupone ","commitid":"ddc4457e1404d8eafbb724d1fc77656f5c049d6e","committime":"2022-02-07T21:48:12","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: ignore CFLAGS"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"fc6258f667ba828358ad338a16e2673162d32222","committime":"2022-02-07T13:06:49","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Package-Manager: Portage-3.0.30, Repoman-3.0.3\nSigned-off-by: Alfredo Tupone ","commitid":"0dad6929d837bb643f4e260f9eb1ca16b6b6c0ba","committime":"2022-02-07T12:50:40","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: works with new ocaml too"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"cf3bf955c05b0cf117abc4c20ee57bd0c6bb45bd","committime":"2022-02-07T10:06:52","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Package-Manager: Portage-3.0.30, Repoman-3.0.3\nSigned-off-by: Alfredo Tupone ","commitid":"ee9179423d62240ec33f0bb32d24c640169afbf3","committime":"2022-02-07T09:57:19","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: duplicate deps"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Package-Manager: Portage-3.0.30, Repoman-3.0.3\nSigned-off-by: Alfredo Tupone ","commitid":"c4284123349e1f898877a81d497bbaf1569cccfa","committime":"2022-02-07T09:54:50","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: fix doc deps"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"2c926e4fd4b45836fd8766829c30b9c793c2a38c","committime":"2022-02-06T19:21:21","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Package-Manager: Portage-3.0.30, Repoman-3.0.3\nSigned-off-by: Alfredo Tupone ","commitid":"6e412177eb38dfea270e9c6c8cf60375cc9ddd81","committime":"2022-02-06T15:52:17","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: drop old version"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"b59580e55af2b12e2555cded84bda061d647ae47","committime":"2021-09-18T17:06:21","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Package-Manager: Portage-3.0.20, Repoman-3.0.3\nSigned-off-by: Alfredo Tupone ","commitid":"cf52b47b1c4d265eadbfbfa9c0352a0c5bd4d5c8","committime":"2021-09-18T16:48:56","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: UnusedInherits"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"eebb55dcce9f6f70df249b241fe2872a88f4fe8f","committime":"2021-06-29T19:51:38","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Package-Manager: Portage-3.0.20, Repoman-3.0.2\nSigned-off-by: Alfredo Tupone ","commitid":"5047348a53133478c69ec7994c0dc81390e03dd3","committime":"2021-06-29T19:38:40","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: enabled hypothesis-selection"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"45678b6e3ca560b6e79fddb0f77b569ac6f6d4f0","committime":"2021-06-29T14:36:19","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Closes: https:\/\/bugs.gentoo.org\/799173\nPackage-Manager: Portage-3.0.20, Repoman-3.0.2\nSigned-off-by: Alfredo Tupone ","commitid":"3daf7a4558c0902de667621d1b3c3224418a5007","committime":"2021-06-29T14:16:08","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: disable hypothesis-selection"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"f45b709be2da2b4b1ac292644e3d67232e34bb2b","committime":"2021-06-12T19:05:09","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Package-Manager: Portage-3.0.18, Repoman-3.0.2\nSigned-off-by: Alfredo Tupone ","commitid":"fa8a6b65b706ccd8cd58fe0d9d3bd0b6d00a610b","committime":"2021-06-12T18:51:19","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: version bump to 2021"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"e214dcde757ffaeff56968e4ba061945000ee476","committime":"2021-02-10T17:37:33","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Closes: https:\/\/bugs.gentoo.org\/769845\nPackage-Manager: Portage-3.0.13, Repoman-3.0.2\nSigned-off-by: Alfredo Tupone ","commitid":"5aff1bfa73f6a17a8f9d6952315f80b2f84e9667","committime":"2021-02-10T17:25:02","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: fix dep"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"3d2bd759012f2e7b108376f08b838e77a006eeba","committime":"2021-02-09T19:47:26","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Package-Manager: Portage-3.0.13, Repoman-3.0.2\nSigned-off-by: Alfredo Tupone ","commitid":"fb6c36404e813f6160eddede1e188cf643546e4c","committime":"2021-02-09T17:49:37","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: version bump to 2020"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"dcdec439559bd3dbf583382cda731faf9ae1e54e","committime":"2021-01-20T13:33:04","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"jakov.smolic@sartura.hr","authorname":"Jakov Smolic","body":"Signed-off-by: Jakov Smolic \nSigned-off-by: David Seifert ","commitid":"74b466e0ec087724918ad1c781ac8cf4fc71a367","committime":"2021-01-20T10:15:57","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: Remove old"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"4257aab25df136dbec985d65c42e775bbc84d4d9","committime":"2021-01-17T05:03:05","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"sam@gentoo.org","authorname":"Sam James","body":"* We need := for OCaml deps to ensure we're rebuilt\n when they update for consistency, to prevent\n strange issues.\n\n* Use ocamlopt= rather than ocamlopt? in the\n dev-lang\/ocaml dependency to ensure ocamlopt\n is consistently on\/off throughout the system.\n\nPackage-Manager: Portage-3.0.12.0.2-prefix, Repoman-3.0.2\nSigned-off-by: Sam James ","commitid":"13795972d83aa1591561d7e60c220c623538b5e2","committime":"2021-01-17T04:03:17","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: update OCaml deps"},{"authoremail":"sam@gentoo.org","authorname":"Sam James","body":"See: https:\/\/gitlab.inria.fr\/why3\/why3\/-\/blob\/master\/CHANGES.md#version-121-october-28-2019\nPackage-Manager: Portage-3.0.12.0.2-prefix, Repoman-3.0.2\nSigned-off-by: Sam James ","commitid":"8095292e91a60900fb257d373295d0052f883f46","committime":"2021-01-17T03:59:40","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: supports both lablgtk:2, :3 for most versions"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"cb588c6334190de381a73aa6452783a6ceb361dd","committime":"2020-06-15T17:35:41","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Closes: https:\/\/bugs.gentoo.org\/728334\nPackage-Manager: Portage-2.3.99, Repoman-2.3.22\nSigned-off-by: Alfredo Tupone ","commitid":"0959f5c012916f832872f2d864fb06552e1d16d5","committime":"2020-06-15T17:19:49","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: fix broken links"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"ebe91b32e911af7d114170ff35e7994325982d6b","committime":"2020-06-14T12:35:09","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Closes: https:\/\/bugs.gentoo.org\/728176\nPackage-Manager: Portage-2.3.99, Repoman-2.3.22\nSigned-off-by: Alfredo Tupone ","commitid":"74292be3bc80e701d8edc741daf55e7053583ced","committime":"2020-06-14T11:49:16","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: fix broken symlink"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"6edcc727643f4038732ff701cbb3035cd875e506","committime":"2020-06-12T21:35:22","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Closes: https:\/\/bugs.gentoo.org\/728032\nCloses: https:\/\/bugs.gentoo.org\/728050\nPackage-Manager: Portage-2.3.99, Repoman-2.3.22\nSigned-off-by: Alfredo Tupone ","commitid":"ea162b812cb64c737eba031c8fcb8bbef7a2084a","committime":"2020-06-12T21:24:23","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: fix flags and compression"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"361f073d6c320f3ce2a724782a6c2f35ff70cbbf","committime":"2020-01-17T11:05:47","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Package-Manager: Portage-2.3.79, Repoman-2.3.16\nSigned-off-by: Alfredo Tupone ","commitid":"15f19de474ea4871f4284684f26b152ed2eff792","committime":"2020-01-17T10:41:07","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: profiling is not more supported by newer ocaml"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"713fe9b68673e5dc52aeca13399a12a503532690","committime":"2020-01-16T10:45:44","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Package-Manager: Portage-2.3.79, Repoman-2.3.16\nSigned-off-by: Alfredo Tupone ","commitid":"47cce5e3baa22474f4e67467d0a320adee35c8ad","committime":"2020-01-16T10:09:16","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: depend on a newer dev-ml\/lablgtk"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"fba9821ae128c88e0afeb48896c87f465ec42646","committime":"2020-01-15T08:48:27","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Package-Manager: Portage-2.3.79, Repoman-2.3.16\nSigned-off-by: Alfredo Tupone ","commitid":"9e87df67d81653262595c6e816aea5326ec015e6","committime":"2020-01-15T08:18:52","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: Needs a newer coq version"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"c69cdee8fc00edd44f90c2fcf9b0c66fb3447700","committime":"2020-01-14T08:05:46","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Closes: https:\/\/bugs.gentoo.org\/705072\nPackage-Manager: Portage-2.3.79, Repoman-2.3.16\nSigned-off-by: Alfredo Tupone ","commitid":"d53b71f85b0a0eac777c476cb523c7bc30d3e5da","committime":"2020-01-14T07:51:42","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: use ocaml-4.09"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"c68d23c2e114ea3bceffffbb128b5eecb2a930b7","committime":"2019-12-20T23:05:33","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"ulm@gentoo.org","authorname":"Ulrich Müller","body":"The virtual is deprecated, depend on app-editors\/emacs instead.\n\nPackage-Manager: Portage-2.3.82, Repoman-2.3.20\nSigned-off-by: Ulrich Müller ","commitid":"6c532ec926058d96e6d584075b63a32e4fb2c300","committime":"2019-12-20T16:31:12","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: Update virtual\/emacs dependency."},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"8637697cc1040750595751770fc912a190e06819","committime":"2019-10-11T07:50:12","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Package-Manager: Portage-2.3.69, Repoman-2.3.16\nSigned-off-by: Alfredo Tupone ","commitid":"7db15954ce77fbeacba298e6a9b01fad1f37798a","committime":"2019-10-11T07:28:10","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: version bump to 2019"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"7cb9977af7514bd91d51de22f3aff13885e7410b","committime":"2019-03-15T07:43:52","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Closes: https:\/\/bugs.gentoo.org\/680312\nSigned-off-by: Alfredo Tupone \nPackage-Manager: Portage-2.3.51, Repoman-2.3.11","commitid":"f0437170eb42e30839073788456e18d5e695665b","committime":"2019-03-15T07:24:05","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: use virtual\/emacs on dependency"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"3c3c72e67b8d202e0837d301e69d187c22468fc1","committime":"2018-12-16T08:43:55","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Signed-off-by: Alfredo Tupone \nPackage-Manager: Portage-2.3.51, Repoman-2.3.11","commitid":"05ca892773aa24c6dd3b8b0fa28d5aa261ffe4f0","committime":"2018-12-16T08:36:37","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: Stable"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"160bed501a7d408535d0c0a6aacb76dbc7dd7aa8","committime":"2018-07-13T07:04:15","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Package-Manager: Portage-2.3.40, Repoman-2.3.9","commitid":"a30437c0c5fb08780562baccb5ff3eeb511bb6ad","committime":"2018-07-13T06:49:22","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: Version bump to 2018"},{"authoremail":"repo-qa-checks@gentoo.org","authorname":"Repository QA checks","commitid":"f323c98189a8f173838be964264bec34ae4a7643","committime":"2018-03-27T07:09:03","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Package-Manager: Portage-2.3.24, Repoman-2.3.6","commitid":"414f51e061f8082d6be5f1e342924bc8cf24ed3b","committime":"2018-03-27T06:05:35","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: Fix STRIP_MASK usage. Bug #651458"},{"authoremail":"repo-qa-checks@gentoo.org","authorname":"Repository QA checks","commitid":"e7f45e756d26d0e5b79d4d84d7a35c3d20cd78ed","committime":"2017-11-06T21:18:38","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Package-Manager: Portage-2.3.8, Repoman-2.3.3","commitid":"ce9a2c2e5a2c8c7acc61c556147b7385139071a5","committime":"2017-11-06T21:09:20","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: dev-ml\/camlzip-1.06 causes problem."},{"authoremail":"repo-qa-checks@gentoo.org","authorname":"Repository QA checks","commitid":"625838f2e2ab455bc85730f8b49c9d69cb4b7615","committime":"2017-11-04T21:18:20","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Package-Manager: Portage-2.3.8, Repoman-2.3.3","commitid":"8762ce2768ade2f75a3f87f4591bd30a3be88f21","committime":"2017-11-04T20:46:39","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: Add ocamlopt use flag"},{"authoremail":"repo-qa-checks@gentoo.org","authorname":"Repository QA checks","commitid":"bbc2bf5a63a5fe511d93c833b8d4a4256e619c3b","committime":"2017-11-04T19:17:36","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Package-Manager: Portage-2.3.8, Repoman-2.3.3","commitid":"9ca01a8eb0c26afe211e01dcea811b54b29f0b28","committime":"2017-11-04T18:28:34","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: Install libraries"},{"authoremail":"repo-qa-checks@gentoo.org","authorname":"Repository QA checks","commitid":"6000fc339352d78841db996c24b15fc6d34107fe","committime":"2017-11-01T20:43:42","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Package-Manager: Portage-2.3.8, Repoman-2.3.3","commitid":"f7767454e6ac2a9eb63c5fc48e3fe8d1fe0ff1dd","committime":"2017-11-01T20:28:03","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: Enable coq tactics"},{"authoremail":"repo-qa-checks@gentoo.org","authorname":"Repository QA checks","commitid":"68ce104bb2f2fa0e3383f091654d805f99db0306","committime":"2017-10-25T17:43:44","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Package-Manager: Portage-2.3.8, Repoman-2.3.3","commitid":"7e278f5c3b1dc15bbce41b0c5574dfae1db6fc51","committime":"2017-10-25T17:28:48","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: remove extra --disable-zip"},{"authoremail":"repo-qa-checks@gentoo.org","authorname":"Repository QA checks","commitid":"42b1906b705e1e60be1ed6e4c651a9c0f6dee58f","committime":"2017-10-24T20:08:56","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Package-Manager: Portage-2.3.8, Repoman-2.3.3","commitid":"06a07ce4bfbcaf034558bb8a95c18e644b3683c6","committime":"2017-10-24T19:58:51","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: Add zip use flags"},{"authoremail":"repo-qa-checks@gentoo.org","authorname":"Repository QA checks","commitid":"c6cf1c2c790b0009e2411a6e3109595a6c46c666","committime":"2017-10-24T18:51:29","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Package-Manager: Portage-2.3.8, Repoman-2.3.3","commitid":"68056447a56bcd1c6d4ff5c342651190889c252a","committime":"2017-10-24T18:32:44","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: Adding examples"},{"authoremail":"repo-qa-checks@gentoo.org","authorname":"Repository QA checks","commitid":"9c8944f7c015b490a6d01e96b65207d67faa651d","committime":"2017-10-23T18:40:41","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Package-Manager: Portage-2.3.8, Repoman-2.3.3","commitid":"b9de4cea63a1f308a54f7fdfbe818a65bf9bcace","committime":"2017-10-23T18:29:37","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: Fix SRC_URI"},{"authoremail":"repo-qa-checks@gentoo.org","authorname":"Repository QA checks","commitid":"c24d322ff13e7b4b47ed09d95e071a9a9e66d37a","committime":"2017-10-19T20:10:44","packageid":68094,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Tupone Alfredo","body":"Package-Manager: Portage-2.3.8, Repoman-2.3.3","commitid":"eb5feee2d87d486910df3c8b3cb505f1eb0e47c3","committime":"2017-10-19T19:43:39","packageid":68094,"repoid":1,"summary":"sci-mathematics\/why3-for-spark: Adding why3 for spark"}],"dependencies":[{"block":false,"categoryid":317,"description":"Coq\/Rocq is a proof assistant written in O'Caml","ebuildids":[853673],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"coq","packageid":42174,"summary":"Developed in the LogiCal project, the Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows: * the definition of functions or predicates, * to state mathematical theorems and software specifications, * to develop interactively formal proofs of these theorems, * to check these proofs by a small certification \"kernel\". Coq is based on a logical framework called \"Calculus of Inductive Constructions\" extended by a modular development system for theories."},{"block":false,"categoryid":314,"description":"OCaml bindings to GTK-3","ebuildids":[853673],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"lablgtk","packageid":43080},{"block":false,"categoryid":395,"description":"The advanced, extensible, customizable, self-documenting editor","ebuildids":[853673],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"gnu-emacs@gentoo.org","maintainername":"Gentoo GNU Emacs project","name":"emacs","packageid":45775,"summary":"GNU Emacs is an extensible, customizable text editor - and more. At its core is an interpreter for Emacs Lisp, a dialect of the Lisp programming language with extensions to support text editing. The features of GNU Emacs include: * Content-sensitive editing modes, including syntax coloring, for a variety of file types including plain text, source code, and HTML. * Complete built-in documentation, including a tutorial for new users. * Full Unicode support for nearly all human languages and their scripts. * Highly customizable, using Emacs Lisp code or a graphical interface. * A large number of extensions that add other functionality, including a project planner, mail and news reader, debugger interface, calendar, and more. Many of these extensions are distributed with GNU Emacs; others are available separately."},{"block":false,"categoryid":314,"description":"Compressed file access ML library (ZIP, GZIP and JAR)","ebuildids":[853673],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"camlzip","packageid":47766},{"block":false,"categoryid":314,"description":"Library for automated conversion of OCaml-values to and from S-expressions","ebuildids":[853673],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"sexplib","packageid":49507},{"block":false,"categoryid":314,"description":"OCaml tool to find\/use non-standard packages","ebuildids":[853673],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"findlib","packageid":51288},{"block":false,"categoryid":377,"description":"HeVeA is a quite complete and fast LaTeX to HTML translator","ebuildids":[853673],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"tex@gentoo.org","maintainername":"Gentoo TeX Project","name":"hevea","packageid":51310},{"block":false,"categoryid":314,"description":"O'Caml Graph library","ebuildids":[853673],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocamlgraph","packageid":52838},{"block":false,"categoryid":314,"description":"LR(1) parser generator for the OCaml language","ebuildids":[853673],"firstseen":"2013-02-08T14:36:53.188287","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"menhir","packageid":60329},{"block":false,"categoryid":314,"description":"JSON parsing and pretty-printing library for OCaml","ebuildids":[853673],"firstseen":"2015-02-15T14:38:09.385452","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"yojson","packageid":63076},{"block":false,"categoryid":314,"description":"Arithmetic and logic operations over arbitrary-precision integers","ebuildids":[853673],"firstseen":"2015-09-20T13:38:44.780852","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"zarith","packageid":64116},{"block":false,"categoryid":314,"description":"Type-driven code generation for OCaml","ebuildids":[853673],"firstseen":"2016-02-06T14:40:36.761342","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ppx_deriving","packageid":64953},{"block":false,"categoryid":314,"description":"Support Library for type-driven code generators","ebuildids":[853673],"firstseen":"2016-02-06T14:40:36.761342","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ppx_sexp_conv","packageid":64965},{"block":false,"categoryid":314,"description":"Library for arbitrary-precision integer and rational arithmetic","ebuildids":[853673],"firstseen":"2020-01-07T21:43:34.584399","name":"num","packageid":70574},{"block":false,"categoryid":314,"description":"Regular expression library for OCaml","ebuildids":[853673],"firstseen":"2020-10-13T14:25:05.132759","name":"re","packageid":72119}],"depending":[{"block":false,"categoryid":450,"description":"Software development for high-reliability applications","ebuildids":[854617,854617],"firstseen":"2017-10-21T19:07:57.494219","name":"spark","packageid":68098,"summary":"SPARK is a software development technology specifically designed for engineering high-reliability applications. It consists of a programming language, a verification toolset and a design method which, taken together, ensure that ultra-low defect software can be deployed in application domains where high-reliability must be assured, for example where safety and security are key requirements."},{"block":true,"categoryid":317,"description":"Platform for deductive program verification","ebuildids":[782878,782878,845202,845202,854230,854230,869907,869907,877153,877153],"firstseen":"2021-12-12T02:08:52.137547","name":"why3","packageid":73747,"summary":"Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs."}],"ebuilds":[{"archs":["amd64","~arm64"],"ebuildid":853673,"firstseen":"2025-02-11T17:32:57.206625","license":"GPL-3","moddate":"2026-03-22T20:20:57","packageid":68094,"repoid":1,"slot":"0","uses":["coq","doc","emacs","gtk","html","hypothesis-selection","ocamlopt","sexp","zarith","zip"],"version":"2023.12.13-r2"}],"masks":[],"package":{"categoryid":317,"description":"SPARK 2014 repository for the Why3 verification platform","firstseen":"2017-10-19T20:17:41.724443","name":"why3-for-spark","packageid":68094,"summary":"Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs."},"rdependencies":[{"block":false,"categoryid":317,"description":"Coq\/Rocq is a proof assistant written in O'Caml","ebuildids":[853673],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"coq","packageid":42174,"summary":"Developed in the LogiCal project, the Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows: * the definition of functions or predicates, * to state mathematical theorems and software specifications, * to develop interactively formal proofs of these theorems, * to check these proofs by a small certification \"kernel\". Coq is based on a logical framework called \"Calculus of Inductive Constructions\" extended by a modular development system for theories."},{"block":false,"categoryid":314,"description":"OCaml bindings to GTK-3","ebuildids":[853673],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"lablgtk","packageid":43080},{"block":false,"categoryid":395,"description":"The advanced, extensible, customizable, self-documenting editor","ebuildids":[853673],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"gnu-emacs@gentoo.org","maintainername":"Gentoo GNU Emacs project","name":"emacs","packageid":45775,"summary":"GNU Emacs is an extensible, customizable text editor - and more. At its core is an interpreter for Emacs Lisp, a dialect of the Lisp programming language with extensions to support text editing. The features of GNU Emacs include: * Content-sensitive editing modes, including syntax coloring, for a variety of file types including plain text, source code, and HTML. * Complete built-in documentation, including a tutorial for new users. * Full Unicode support for nearly all human languages and their scripts. * Highly customizable, using Emacs Lisp code or a graphical interface. * A large number of extensions that add other functionality, including a project planner, mail and news reader, debugger interface, calendar, and more. Many of these extensions are distributed with GNU Emacs; others are available separately."},{"block":false,"categoryid":314,"description":"Compressed file access ML library (ZIP, GZIP and JAR)","ebuildids":[853673],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"camlzip","packageid":47766},{"block":false,"categoryid":314,"description":"Library for automated conversion of OCaml-values to and from S-expressions","ebuildids":[853673],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"sexplib","packageid":49507},{"block":false,"categoryid":450,"description":"Programming language supporting functional, imperative & object-oriented styles","ebuildids":[853673],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocaml","packageid":49590},{"block":false,"categoryid":377,"description":"HeVeA is a quite complete and fast LaTeX to HTML translator","ebuildids":[853673],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"tex@gentoo.org","maintainername":"Gentoo TeX Project","name":"hevea","packageid":51310},{"block":false,"categoryid":314,"description":"O'Caml Graph library","ebuildids":[853673],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocamlgraph","packageid":52838},{"block":false,"categoryid":314,"description":"LR(1) parser generator for the OCaml language","ebuildids":[853673],"firstseen":"2013-02-08T14:36:53.188287","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"menhir","packageid":60329},{"block":false,"categoryid":314,"description":"JSON parsing and pretty-printing library for OCaml","ebuildids":[853673],"firstseen":"2015-02-15T14:38:09.385452","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"yojson","packageid":63076},{"block":false,"categoryid":314,"description":"Arithmetic and logic operations over arbitrary-precision integers","ebuildids":[853673],"firstseen":"2015-09-20T13:38:44.780852","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"zarith","packageid":64116},{"block":false,"categoryid":314,"description":"Type-driven code generation for OCaml","ebuildids":[853673],"firstseen":"2016-02-06T14:40:36.761342","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ppx_deriving","packageid":64953},{"block":false,"categoryid":314,"description":"Support Library for type-driven code generators","ebuildids":[853673],"firstseen":"2016-02-06T14:40:36.761342","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ppx_sexp_conv","packageid":64965},{"block":false,"categoryid":314,"description":"Library for arbitrary-precision integer and rational arithmetic","ebuildids":[853673],"firstseen":"2020-01-07T21:43:34.584399","name":"num","packageid":70574},{"block":false,"categoryid":314,"description":"Regular expression library for OCaml","ebuildids":[853673],"firstseen":"2020-10-13T14:25:05.132759","name":"re","packageid":72119}],"repos":[{"branch":"master","lastcommit":"b0dd603654956bad345abbff616070880b281179","name":"gentoo","path":"\/usr\/portage","repoid":1,"upstream":"origin"}],"tracked":false,"urls":["https:\/\/github.com\/AdaCore\/why3","https:\/\/www.why3.org\/"],"uses":[{"description":"Add sci-mathematics\/coq support","isdefault":false,"packageid":68094,"use":"coq"},{"description":"Add extra documentation (API, Javadoc, etc). It is recommended to enable per package instead of globally","isdefault":false,"use":"doc"},{"description":"Add support for GNU Emacs","isdefault":false,"use":"emacs"},{"description":"Add support for x11-libs\/gtk+ (The GIMP Toolkit)","isdefault":false,"use":"gtk"},{"description":"Build HTML documentation","isdefault":false,"packageid":68094,"use":"html"},{"description":"Enable hypothesis selection","isdefault":false,"packageid":68094,"use":"hypothesis-selection"},{"defaultflag":true,"description":"Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable\/enable it at a global scale)","isdefault":true,"use":"ocamlopt"},{"description":"Add support for outputting S-expressions with dev-ml\/ppx_sexp_conv","isdefault":false,"packageid":68094,"use":"sexp"},{"description":"Use Zarith (dev-ml\/zarith) instead of Nums (dev-ml\/num) for computations","isdefault":false,"packageid":68094,"use":"zarith"},{"description":"Enable compression of session files","isdefault":false,"packageid":68094,"use":"zip"}]}