{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":3518380,"defaultBranch":"develop","name":"tamarin-prover","ownerLogin":"tamarin-prover","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2012-02-22T20:03:23.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/1788989?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1695291456.0","currentOid":""},"activityList":{"items":[{"before":"d694dff6bd63465005b3c5f7261ecccbc8025bc7","after":"0e1aa8f32a9cb214ff16e2a8a58fbdc5f815fa45","ref":"refs/heads/develop","pushedAt":"2024-04-03T13:25:59.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rsasse","name":"Ralf Sasse","path":"/rsasse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2189451?s=80&v=4"},"commit":{"message":"Display 'None' when there are no injective fact instances (#612)","shortMessageHtmlLink":"Display 'None' when there are no injective fact instances (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2033019351\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/612\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/612/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/612\">#612</a>)"}},{"before":"b3e18f61e45d701d42d794bc91ccbb4c0e3834ec","after":"d694dff6bd63465005b3c5f7261ecccbc8025bc7","ref":"refs/heads/develop","pushedAt":"2024-02-27T09:29:17.000Z","pushType":"pr_merge","commitsCount":8,"pusher":{"login":"cascremers","name":"Cas Cremers","path":"/cascremers","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1481528?s=80&v=4"},"commit":{"message":"Merge pull request #446 from yavivanov/pr-plainOpenGoals-fix\n\nSolving the second issue of PR#394 without plainOpenGoals","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1052013698\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/446\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/446/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/446\">#446</a> from yavivanov/pr-plainOpenGoals-fix"}},{"before":"662a8575478892d80f92fd69f52ebdee8149ccc9","after":"b3e18f61e45d701d42d794bc91ccbb4c0e3834ec","ref":"refs/heads/develop","pushedAt":"2024-02-26T09:04:48.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jdreier","name":null,"path":"/jdreier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7261779?s=80&v=4"},"commit":{"message":"Update to GHC 9.6 (#618)\n\nRemoving Control.Monad.List","shortMessageHtmlLink":"Update to GHC 9.6 (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2149515393\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/618\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/618/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/618\">#618</a>)"}},{"before":"fbf19d9a78f8ee37cc3e6718ef6de50c04139a73","after":"662a8575478892d80f92fd69f52ebdee8149ccc9","ref":"refs/heads/develop","pushedAt":"2024-02-09T19:13:46.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rkunnema","name":null,"path":"/rkunnema","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2065833?s=80&v=4"},"commit":{"message":"Configuration blocks in spthy files and a new default oraclename (#512)\n\n* support for config blocks + new default oraclename\r\n\r\nCo-authored-by: Nick Moore <nicholas.moore@cs.ox.ac.uk>\r\n\r\n* set backup default oracle to ./oracle\r\n\r\n- adapted heuristic code to the tactic code\r\n- added backup default oracle code\r\n- improved the default oraclename code\r\n- adapted the terminal and Web client outputs\r\n- fixed bugs w.r.t. oracle name workdir and printed output\r\n\r\n* added configblock comparison to regressionTests.py\r\n\r\n* fixed errors resulting from the merge\r\n\r\n---------\r\n\r\nCo-authored-by: Nick Moore <nicholas.moore@cs.ox.ac.uk>\r\nCo-authored-by: rkunnema <robert.kuennemann@cispa.de>","shortMessageHtmlLink":"Configuration blocks in spthy files and a new default oraclename (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1463666183\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/512\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/512/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/512\">#512</a>)"}},{"before":"2a52f1280d430b28c785e57baa50205443c98aa6","after":"fbf19d9a78f8ee37cc3e6718ef6de50c04139a73","ref":"refs/heads/develop","pushedAt":"2024-01-09T15:52:42.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jdreier","name":null,"path":"/jdreier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7261779?s=80&v=4"},"commit":{"message":"Add Esorics'23 Bluetooth examples (#605)\n\nCo-authored-by: tcl <tristan.claverie@ssi.gouv.fr>","shortMessageHtmlLink":"Add Esorics'23 Bluetooth examples (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1955959377\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/605\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/605/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/605\">#605</a>)"}},{"before":"e6a90bf46c82af969733203d6111b12f50908d39","after":"2a52f1280d430b28c785e57baa50205443c98aa6","ref":"refs/heads/develop","pushedAt":"2023-12-08T10:35:27.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jdreier","name":null,"path":"/jdreier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7261779?s=80&v=4"},"commit":{"message":"Adaptation clanDot python3 (#611)\n\n* cleanDotPython3Adaptation\r\n\r\n* Documentation Adaptation for cleanDot\r\n\r\n---------\r\n\r\nCo-authored-by: Marco Calipari <marco.calipari.ext@siemens.com>","shortMessageHtmlLink":"Adaptation clanDot python3 (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2010704208\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/611\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/611/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/611\">#611</a>)"}},{"before":"4e67cd089dc6a43895becfca94b4b6058e122176","after":"e6a90bf46c82af969733203d6111b12f50908d39","ref":"refs/heads/develop","pushedAt":"2023-12-05T15:29:24.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rkunnema","name":null,"path":"/rkunnema","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2065833?s=80&v=4"},"commit":{"message":"Fix accountability examples (#607)\n\n* Adapted some accountability examples to new SAPIC syntax.\r\n\r\n* Adapt another accountability example to updated SAPIC semantic\r\n\r\n* Add oracle heuristic to accountability examples\r\n\r\n* Adapt accountability examples from Master's thesis to new SAPiC semantic\r\n\r\n* Update README\r\n\r\n* Add README\r\n\r\n* Change to monospace\r\n\r\n* Add accountability case studies to regression tests\r\n\r\n* Revert failing case study to upstream version\r\n\r\n* Fix unintentional restore of failing case study\r\n\r\n---------\r\n\r\nCo-authored-by: Robert Künnemann <robert.kuennemann@cispa.saarland>\r\nCo-authored-by: rkunnema <robert.kuennemann@cispa.de>","shortMessageHtmlLink":"Fix accountability examples (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1997437580\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/607\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/607/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/607\">#607</a>)"}},{"before":"1a7df257f43c37ce08adbbb6a950908b6db3c1ca","after":"4e67cd089dc6a43895becfca94b4b6058e122176","ref":"refs/heads/develop","pushedAt":"2023-12-05T11:00:56.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rkunnema","name":null,"path":"/rkunnema","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2065833?s=80&v=4"},"commit":{"message":"Archive case studies of CI run as artifact (#608)\n\n* Archive case studies as artifact in action\r\n\r\n* Run archive action when case studies fail\r\n\r\n* Add verbose output to regression tests\r\n\r\n* Remove case-studies-regression from artifact\r\n\r\n* Change name of archive action","shortMessageHtmlLink":"Archive case studies of CI run as artifact (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1999622057\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/608\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/608/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/608\">#608</a>)"}},{"before":"86014ad1844247b4faac36bc15f83befde30dcd7","after":"1a7df257f43c37ce08adbbb6a950908b6db3c1ca","ref":"refs/heads/develop","pushedAt":"2023-12-05T10:22:53.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rkunnema","name":null,"path":"/rkunnema","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2065833?s=80&v=4"},"commit":{"message":"Update failing case study (#610)","shortMessageHtmlLink":"Update failing case study (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2010110618\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/610\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/610/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/610\">#610</a>)"}},{"before":"b8e274fe9be3568e9cbb3fcd8e579d686247e665","after":"86014ad1844247b4faac36bc15f83befde30dcd7","ref":"refs/heads/develop","pushedAt":"2023-10-27T05:47:40.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rkunnema","name":null,"path":"/rkunnema","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2065833?s=80&v=4"},"commit":{"message":"Run wellformedness checks in parse-only mode and on export (#595)\n\n* Run wellformedness checks in parse-only mode and on export\r\n\r\nWellformedness checks are now also executed in parse-only mode and when\r\nexporting to other formats. Warnings and the version string are included\r\nas comments in tho output.\r\n\r\n* Revise theory loading and translation based on output module\r\n\r\n* Update regression case studies","shortMessageHtmlLink":"Run wellformedness checks in parse-only mode and on export (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1915034001\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/595\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/595/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/595\">#595</a>)"}},{"before":"50e2965292e25ce8ce9794ade5e0e4e235e7924a","after":"b8e274fe9be3568e9cbb3fcd8e579d686247e665","ref":"refs/heads/develop","pushedAt":"2023-10-19T11:11:06.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rkunnema","name":null,"path":"/rkunnema","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2065833?s=80&v=4"},"commit":{"message":"Allow arbitrary public, fresh, and nat names (#594)\n\nPrevious to this change, public, fresh, and nat names were parsed as\r\nidentifiers which artificially limited the set of expressible names in a\r\ntheory.\r\n\r\nNow arbitrary strings without single quotes and newlines are allowed. This\r\nallows including protocol constants verbatim, which could not be parsed\r\nas identifiers.\r\n\r\nCo-authored-by: Yavor Ivanov <s8yaivan@stud.uni-saarland.de>","shortMessageHtmlLink":"Allow arbitrary public, fresh, and nat names (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1911690927\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/594\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/594/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/594\">#594</a>)"}},{"before":"c838686f5a3d41b6a355eafd32cc2104ca41809c","after":"50e2965292e25ce8ce9794ade5e0e4e235e7924a","ref":"refs/heads/develop","pushedAt":"2023-10-19T08:08:21.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jdreier","name":null,"path":"/jdreier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7261779?s=80&v=4"},"commit":{"message":"Small fixes (#602)\n\n* fix keyboard shurtcut order\r\n\r\n* fix bounded auto-prover argument\r\n\r\n* always show adversary deduction edges","shortMessageHtmlLink":"Small fixes (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1935126274\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/602\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/602/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/602\">#602</a>)"}},{"before":"72efe2d78bad60a850e9c3bad89678c907dbef97","after":"c838686f5a3d41b6a355eafd32cc2104ca41809c","ref":"refs/heads/develop","pushedAt":"2023-10-05T19:57:37.000Z","pushType":"pr_merge","commitsCount":5,"pusher":{"login":"cascremers","name":"Cas Cremers","path":"/cascremers","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1481528?s=80&v=4"},"commit":{"message":"Merge pull request #599 from cascremers/remove-obsolete-maintainers\n\nRemove obsolete maintainers","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1928545538\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/599\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/599/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/599\">#599</a> from cascremers/remove-obsolete-maintainers"}},{"before":"6e1f81c1f92a84ef4760fbb6edd7c3a68fee506b","after":"72efe2d78bad60a850e9c3bad89678c907dbef97","ref":"refs/heads/develop","pushedAt":"2023-10-02T07:36:13.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"cascremers","name":"Cas Cremers","path":"/cascremers","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1481528?s=80&v=4"},"commit":{"message":"Merge pull request #598 from cascremers/copyright-simplification\n\nCopyright simplification","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1920629872\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/598\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/598/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/598\">#598</a> from cascremers/copyright-simplification"}},{"before":"42178e49b45bab7acb5677cdc45a22eb28e970fc","after":"6e1f81c1f92a84ef4760fbb6edd7c3a68fee506b","ref":"refs/heads/develop","pushedAt":"2023-10-01T19:25:44.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jdreier","name":null,"path":"/jdreier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7261779?s=80&v=4"},"commit":{"message":"Better status messages when loading a theory (#585)\n\n* Better status messages when loading a theory\r\n\r\n* print Maude & Dot checks to stderr instead of stdout\r\n\r\n* do not show saturing sources during derivchecks","shortMessageHtmlLink":"Better status messages when loading a theory (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1873461873\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/585\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/585/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/585\">#585</a>)"}},{"before":"f95c9d38bffbd9f26d850181eb9222b15de92d49","after":"42178e49b45bab7acb5677cdc45a22eb28e970fc","ref":"refs/heads/develop","pushedAt":"2023-10-01T19:24:57.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jdreier","name":null,"path":"/jdreier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7261779?s=80&v=4"},"commit":{"message":"added shortcut -d for derivcheck-timeout, added rule attribute no_derivcheck (#593)","shortMessageHtmlLink":"added shortcut -d for derivcheck-timeout, added rule attribute no_der…"}},{"before":"9dcd33a4995f40bfff93d96bcb481155e2185435","after":"f95c9d38bffbd9f26d850181eb9222b15de92d49","ref":"refs/heads/develop","pushedAt":"2023-10-01T07:39:29.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"cascremers","name":"Cas Cremers","path":"/cascremers","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1481528?s=80&v=4"},"commit":{"message":"Merge pull request #591 from cascremers/improve-attribution\n\nRemoving obsolete reference to ETH Zurich.","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1904911766\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/591\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/591/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/591\">#591</a> from cascremers/improve-attribution"}},{"before":null,"after":"2023bf45660993c250f71bea8f123d870bfb3e82","ref":"refs/heads/yavivanov-pr-plainOpenGoals-fix","pushedAt":"2023-09-21T10:17:36.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"rkunnema","name":null,"path":"/rkunnema","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2065833?s=80&v=4"},"commit":{"message":"Fix compile error.","shortMessageHtmlLink":"Fix compile error."}},{"before":"b170ec70369fe18f372cb54100e69c430f5127d9","after":"9dcd33a4995f40bfff93d96bcb481155e2185435","ref":"refs/heads/develop","pushedAt":"2023-09-08T06:59:32.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jdreier","name":null,"path":"/jdreier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7261779?s=80&v=4"},"commit":{"message":"Add back asum import to fix compilation (#590)\n\nFixes the following build failure on Arch:\r\n\r\n```\r\n [16 of 24] Compiling Extension.Prelude ( src/Extension/Prelude.hs, dist/build/Extension/Prelude.dyn_o )\r\n\r\n src/Extension/Prelude.hs:231:13: error:\r\n     • Variable not in scope: asum :: [f0 a] -> f a\r\n     • Perhaps you meant one of these:\r\n         ‘sum’ (imported from Prelude),\r\n         ‘msum’ (imported from Control.Basics)\r\n     |\r\n 231 | oneOfList = asum . map pure\r\n     |             ^^^^\r\n```","shortMessageHtmlLink":"Add back asum import to fix compilation (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1886269831\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/590\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/590/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/590\">#590</a>)"}},{"before":"57e619fef32033293e4a83c0be67cc6e296bf166","after":"b170ec70369fe18f372cb54100e69c430f5127d9","ref":"refs/heads/develop","pushedAt":"2023-09-07T11:06:36.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rkunnema","name":null,"path":"/rkunnema","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2065833?s=80&v=4"},"commit":{"message":"Never redefine in the proverif export the nat type (#588)\n\nIn some cases, the sapic typing and priority of parsing makes it so\r\nthat the export redefines the nat type of Proverif, which leads to\r\nfailure. We simply never redefine the nat type to avoid any possible\r\nclashes.","shortMessageHtmlLink":"Never redefine in the proverif export the nat type (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1881579693\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/588\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/588/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/588\">#588</a>)"}},{"before":"5658a12a3e046c5b0a5dbb69282afbacb5884d6e","after":"57e619fef32033293e4a83c0be67cc6e296bf166","ref":"refs/heads/develop","pushedAt":"2023-08-30T11:55:57.000Z","pushType":"push","commitsCount":5,"pusher":{"login":"rsasse","name":"Ralf Sasse","path":"/rsasse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2189451?s=80&v=4"},"commit":{"message":"merge master changes back in, increase develop version number to 1.9.0","shortMessageHtmlLink":"merge master changes back in, increase develop version number to 1.9.0"}},{"before":"160d381d4c464d5e972523245f95d27d42cd6e22","after":"f172d7f00b1485446a1e7a42dc14623c2189cc42","ref":"refs/heads/master","pushedAt":"2023-08-30T11:36:43.000Z","pushType":"push","commitsCount":762,"pusher":{"login":"rsasse","name":"Ralf Sasse","path":"/rsasse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2189451?s=80&v=4"},"commit":{"message":"Regression timing and version number update","shortMessageHtmlLink":"Regression timing and version number update"}},{"before":"e9d6f5471dd891fa17d71ffb1b5f94a6d85f439c","after":"5658a12a3e046c5b0a5dbb69282afbacb5884d6e","ref":"refs/heads/develop","pushedAt":"2023-08-29T12:45:43.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jdreier","name":null,"path":"/jdreier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7261779?s=80&v=4"},"commit":{"message":"Make Sapic compatible with new nat type (#584)\n\n* Make Sapic compatible with new nat type\r\n\r\n* Improve Error reporting for exports","shortMessageHtmlLink":"Make Sapic compatible with new nat type (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1863498015\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/584\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/584/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/584\">#584</a>)"}},{"before":"74123494aed8f7b7d318662073f8850466a3e13b","after":"e9d6f5471dd891fa17d71ffb1b5f94a6d85f439c","ref":"refs/heads/develop","pushedAt":"2023-08-22T11:48:37.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jdreier","name":null,"path":"/jdreier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7261779?s=80&v=4"},"commit":{"message":"Update lts (#583)\n\n* more refactoring of wellformedness checks\r\n\r\n* update LTS, fix unused import","shortMessageHtmlLink":"Update lts (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1861081400\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/583\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/583/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/583\">#583</a>)"}},{"before":"47ea332675a8fee7f2484fe142edfa9b541c52f8","after":"74123494aed8f7b7d318662073f8850466a3e13b","ref":"refs/heads/develop","pushedAt":"2023-08-22T08:39:57.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jdreier","name":null,"path":"/jdreier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7261779?s=80&v=4"},"commit":{"message":"more refactoring of wellformedness checks (#581)","shortMessageHtmlLink":"more refactoring of wellformedness checks (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1859663975\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/581\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/581/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/581\">#581</a>)"}},{"before":"3b83477fe93d08c5dbe4a21209b00520a80d53f8","after":"47ea332675a8fee7f2484fe142edfa9b541c52f8","ref":"refs/heads/develop","pushedAt":"2023-08-15T13:01:02.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"cascremers","name":"Cas Cremers","path":"/cascremers","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1481528?s=80&v=4"},"commit":{"message":"Merge pull request #580 from cascremers/improve-attribution\n\nUpdating development attribution and copyrights.","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1851366111\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/580\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/580/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/580\">#580</a> from cascremers/improve-attribution"}},{"before":"240e5a1f0e73e6a5e8ab2e98a0acf7ff4d7f9066","after":"3b83477fe93d08c5dbe4a21209b00520a80d53f8","ref":"refs/heads/develop","pushedAt":"2023-08-13T19:20:04.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jdreier","name":null,"path":"/jdreier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7261779?s=80&v=4"},"commit":{"message":"Fix spurios wellformedness warnings when using macros (#576)\n\n* fix spurious wellformedness warning when using macros\r\n\r\n* fix another spurious wellformedness warning when using macros","shortMessageHtmlLink":"Fix spurios wellformedness warnings when using macros (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1845811361\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/576\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/576/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/576\">#576</a>)"}},{"before":"28dab343c9a9a2848f328dc5efb445b581dc06b9","after":"240e5a1f0e73e6a5e8ab2e98a0acf7ff4d7f9066","ref":"refs/heads/develop","pushedAt":"2023-08-09T19:18:00.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jdreier","name":null,"path":"/jdreier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7261779?s=80&v=4"},"commit":{"message":"fixes book links (#573)","shortMessageHtmlLink":"fixes book links (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1837431770\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/573\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/573/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/573\">#573</a>)"}},{"before":"c704b61665c8232d8bd5220210a65823e09f310f","after":"28dab343c9a9a2848f328dc5efb445b581dc06b9","ref":"refs/heads/develop","pushedAt":"2023-08-09T19:17:32.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jdreier","name":null,"path":"/jdreier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7261779?s=80&v=4"},"commit":{"message":"Refactor Derivation Checks (#575)\n\n* fix compile warnings + hlint\r\n\r\n* you don't need to close the diff theory just to get the final rules","shortMessageHtmlLink":"Refactor Derivation Checks (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1837939824\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/575\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/575/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/575\">#575</a>)"}},{"before":"a35488c91ecf3f927a9ff3756f086ff6e5c0b293","after":"c704b61665c8232d8bd5220210a65823e09f310f","ref":"refs/heads/develop","pushedAt":"2023-07-31T11:44:39.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rsasse","name":"Ralf Sasse","path":"/rsasse","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2189451?s=80&v=4"},"commit":{"message":"Subterms and Natural Numbers (#507)\n\n* adapt gitignore for Intellij\r\n\r\n* remove old unused files\r\n\r\n* Fixed Haddock errors\r\n\r\nneeded for the Haskell Intellij-plugin\r\n\r\n* fix haddock errors\r\n\r\nnecessary for Intelliij Haskell plugin\r\n\r\n* different way of fixing haddock\r\n\r\n* Revert \"Fixed Haddock errors\"\r\n\r\nThis reverts commit 71d30f40f448b8fe33cb851481d8ecf327ed101a.\r\n\r\n* whole subterms squashed\r\n\r\n* Contradictions.hs\r\n\r\n* Goals.hs (void insertFormula)\r\n\r\n* Guarded.hs\r\n\r\n* LTerm.hs\r\n\r\n* Pretty.hs\r\n\r\n* Reduction.hs (insertFormula stuff)\r\n\r\n* Signature.hs (unsure what stFunSyms is...)\r\n\r\n* Simplify.hs (without freshOrdering)\r\n\r\n* System.hs (hasSubtermCycle)\r\n\r\n* Term.hs (elemNotBelowReducible)\r\n\r\n* Token.hs (opSubterm << ⊏)\r\n\r\n* Wellformedness.hs\r\n\r\n* towards a compiling version\r\n\r\n* reverting insertFormula change\r\n\r\n* a compiling version!\r\n\r\n* first subtermStore stuff\r\n\r\n* partially integrated subtermStore\r\n\r\n* add SubtermG\r\n\r\n* solve SubtermGoal\r\n\r\n* simpSubterms in Simplify.hs\r\n\r\n* reducibleFormula\r\n\r\n* somewhat finished\r\nleft todo's are:\r\n- show a \"trace found\" (e.g. in SubtermTests --> WrongSplitSubterms)\r\n- show a message \"no further proof possible\" if reducible operators are left\r\n\r\n* removed todo\r\n\r\n* replace plainOpenGoals by openGoals\r\nand add minimal test file\r\n\r\n* little fix regarding duplicate goals (one solved and one unsolved)\r\n\r\n* advanced freshOrdering (using subterms)\r\n\r\n* little fix\r\n\r\n* Natural Number Cherry Picking\r\n\r\n* Natural Number compiling version\r\n\r\n* minor adaptions\r\n\r\n* Term Parser: moving from \"Parser (Term l)\" to \"Parser LNTerm\"\r\n\r\n* small tidy-up\r\n\r\n* re-enabled NatSubtermD in splitSubterm\r\n\r\n* proper usage of splitting subterms\r\n\r\n* heuristics adapted\r\n\r\n* implemented nat-cycle algorithm\r\n\r\n* little parser fix\r\n\r\n* Parser don't know fix\r\n\r\n* maude parser fix\r\n\r\n* removed debugging\r\n\r\n* fixed sort of tone\r\n\r\n* debugging output kills performance (400%)\r\n\r\n* removing already false negative subterms\r\n\r\n* fix such that non-splits do not appear in the goals\r\n\r\n* arityOneDeduction\r\n\r\n* enhanced freshOrdering rule   ##careful!!! this will impact the regression tests!!!\r\n\r\n* fixed forgotten persistent fact exclusion\r\n\r\n* fixed serious bug in the enhanced freshOrdering\r\n\r\n* advanced partialAtomValuation for subterms\r\n\r\n* Fix parser merge\r\n\r\n* partial evaluation of CR-rule S_neg\r\n\r\n* deduce KU(%nat) automatically like done with KU($pub)\r\n\r\n* Better detection of injective facts\r\n\r\n* detection of non-changing and monotonic positions\r\n\r\n* monotonic injective facts!\r\n(pairs are a todo)\r\n\r\n* s vs t bugfix\r\n\r\n* (decreasing, strict vs non-strict) rework of the injective fact monotonicity\r\nTODO: properly test it\r\n\r\n* uncomment non-increasing stuff as models diverge with it\r\n\r\n* bugfix concerning detection of monotonicity with pairs\r\n\r\n* fixed looping bug for non-strictly increasing stuff\r\n\r\n**and: now, no subterms are introduced by monotonicity**\r\n\r\n* sanity kill whenever right side of a subterm has reducible operator on top [just for the paper]\r\n\r\n* Regression updates\r\n\r\n* Parse proofs with subterm\r\n\r\n* Move addition of less relation from injective fact as looping simplifier\r\n\r\n* Docker fixes\r\n\r\n* fix compiler error\r\n\r\n* fixing parser errors but creating other ones\r\n\r\n* parser sorting checks\r\n\r\n* porting natCheck to diff\r\n\r\n* fix maude merging error\r\n\r\n* removing freshOrdering if it's a sapic file because that makes it slower\r\nsee opc_ua_secure_conversation.spthy\r\n\r\n* Removing nat intruder rules as it is constructed directly in NatConstrRule\r\n\r\n* fix download proof and reimport error and diff quantifier sort error\r\n\r\n* change advanced fresh order to only insert `<` and never a disjunction (and check that the equalities are impossible)\r\n\r\n* `System>safePartialAtomValuation` now uses `SubtermStore>isTrueFalse` as well\r\n\r\n* comment changes\r\n\r\n* removing outdated TODO's\r\n\r\n* apply addNonInjectiveFactInstances non-looping\r\n\r\n* updating the regression tests to be the ones from develop\r\n\r\n* some variable renaming that killed the regression test performance\r\n\r\n* re-enabled freshOrdering for sapic - including actions in detection\r\n\r\n* added missing regression test to case-studies-regression which was produced by the makefile\r\n\r\n* fixing bug in freshOrder\r\n\r\n* added natural numbers to regression tests\r\n\r\n* fixing heavy observational equivalence bug\r\n\r\n* Yellow Color!\r\n\r\n* yellow diff fixes\r\n\r\n* update regression tests\r\n\r\n* updated regression tests for merged changes from develop\r\n\r\n* Remove remnant debug trace from Message Derivation checks.\r\n\r\n* Remove unnecessary Debug.Trace include\r\n\r\n* remove unnecessary Debug.Trace import.\r\n\r\n* expand comment on DiffUnfinishable in code\r\n\r\n* adding small tests for subterms and numbers\r\n\r\n* make fst/snd by default Constructor again, instead of Destructor.\r\n\r\n* minor cleanup changes, as discussed in PR\r\n\r\n* remove unnecessary (commented) imports, typo fixes\r\n\r\n* fixed runtime issue in diff mode\r\n\r\n* trying to fix issue with nat vars\r\n\r\n* fixing timeout for derivation checks\r\n\r\n* Better messages for derivation checks\r\n\r\n* fix timeout, again...\r\n\r\n* fix output: don't show empty warning\r\n\r\n* fix warnings\r\n\r\n* fix more warnings\r\n\r\n* missing regression test file\r\n\r\n* Fixed Makefile to include xor-diff target.\r\n\r\n* Update ALL regression targets.\r\n\r\n---------\r\n\r\nCo-authored-by: Charlie Jacomme <jacomme@crans.org>\r\nCo-authored-by: Philip Lukert <c01phlu@colossus06.cispa.saarland>\r\nCo-authored-by: Ralf Sasse <ralf.sasse@gmail.com>\r\nCo-authored-by: Jannik Dreier <jannik.dreier@loria.fr>","shortMessageHtmlLink":"Subterms and Natural Numbers (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1447907928\" data-permission-text=\"Title is private\" data-url=\"https://github.com/tamarin-prover/tamarin-prover/issues/507\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/tamarin-prover/tamarin-prover/pull/507/hovercard\" href=\"https://github.com/tamarin-prover/tamarin-prover/pull/507\">#507</a>)"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEJrDjMAA","startCursor":null,"endCursor":null}},"title":"Activity · tamarin-prover/tamarin-prover"}