{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":395729248,"defaultBranch":"master","name":"copilot-1","ownerLogin":"GaloisInc","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2021-08-13T16:58:10.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/1584774?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1713978680.0","currentOid":""},"activityList":{"items":[{"before":"8cfd52bbc08db443a5b1b392c6aee3848235f12a","after":"b153fbc2231ad33862d2b7a94986f0a90bf501f9","ref":"refs/heads/develop-issue495-kind2Prover-falsifiable","pushedAt":"2024-05-05T21:37:58.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"copilot-theorem: Document changes in CHANGELOG. Refs #495.","shortMessageHtmlLink":"copilot-theorem: Document changes in CHANGELOG. Refs <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2079121923\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Copilot-Language/copilot/issues/495\" data-hovercard-type=\"issue\" data-hovercard-url=\"/Copilot-Language/copilot/issues/495/hovercard\" href=\"https://github.com/Copilot-Language/copilot/issues/495\">Copilot-Language…</a>"}},{"before":null,"after":"8cfd52bbc08db443a5b1b392c6aee3848235f12a","ref":"refs/heads/develop-issue495-kind2Prover-falsifiable","pushedAt":"2024-04-24T17:11:20.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"copilot-theorem: Document changes in CHANGELOG. Refs #495.","shortMessageHtmlLink":"copilot-theorem: Document changes in CHANGELOG. Refs <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2079121923\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Copilot-Language/copilot/issues/495\" data-hovercard-type=\"issue\" data-hovercard-url=\"/Copilot-Language/copilot/issues/495/hovercard\" href=\"https://github.com/Copilot-Language/copilot/issues/495\">Copilot-Language…</a>"}},{"before":null,"after":"b9256d2e1cbeab1da69e645e0a74b495b14fb3a1","ref":"refs/heads/tmp-falsifiable","pushedAt":"2024-04-22T22:22:52.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Draft: s/invalid/falsifiable/\n\n[ci skip]","shortMessageHtmlLink":"Draft: s/invalid/falsifiable/"}},{"before":"78f851ebaddf21a20929ab4914f974670d2384b8","after":"da7dcfd27fe9cc7b13238e1015dd5c92889f8c01","ref":"refs/heads/develop-callstack-support","pushedAt":"2024-02-07T13:29:14.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Add call stacks to unit tests","shortMessageHtmlLink":"Add call stacks to unit tests"}},{"before":"6aeebdb3996d76f47d6dc0a9a0546d73dc20b5bf","after":"3543f0aa9dd8d912fce70fe55c285fe6608eed4b","ref":"refs/heads/develop-bluespec-bsv","pushedAt":"2024-01-28T17:00:08.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Try Bluespec SystemVerilog","shortMessageHtmlLink":"Try Bluespec SystemVerilog"}},{"before":"db755d631e3d2deb8939aba1f171d833d05140b4","after":"6aeebdb3996d76f47d6dc0a9a0546d73dc20b5bf","ref":"refs/heads/develop-bluespec-bsv","pushedAt":"2024-01-28T16:47:43.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Try Bluespec SystemVerilog","shortMessageHtmlLink":"Try Bluespec SystemVerilog"}},{"before":"e819554b476b38ab40c298e2f87ea7f4dff05aa1","after":"44b02a685b42b1688142f3010e65fe79d2371339","ref":"refs/heads/develop-bluespec","pushedAt":"2024-01-17T12:02:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"DESIGN.md: More details on unsupported operations","shortMessageHtmlLink":"DESIGN.md: More details on unsupported operations"}},{"before":"dac050b22531599597137d69254fa0699d2bb286","after":"e819554b476b38ab40c298e2f87ea7f4dff05aa1","ref":"refs/heads/develop-bluespec","pushedAt":"2024-01-16T19:09:11.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"copilot-bluespec unit tests\n\nInspired by the unit test suite in `copilot-c99`.","shortMessageHtmlLink":"copilot-bluespec unit tests"}},{"before":"c39beb43feb06c97630a49efb0ce9ef841ac5ec8","after":"e819554b476b38ab40c298e2f87ea7f4dff05aa1","ref":"refs/heads/develop-bluespec-tests","pushedAt":"2024-01-16T19:06:35.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"copilot-bluespec unit tests\n\nInspired by the unit test suite in `copilot-c99`.","shortMessageHtmlLink":"copilot-bluespec unit tests"}},{"before":"ff34ac0f79cbc4e4c3dca6ddb33ebd6e0c1cbfb1","after":"c39beb43feb06c97630a49efb0ce9ef841ac5ec8","ref":"refs/heads/develop-bluespec-tests","pushedAt":"2024-01-15T22:40:26.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Draft: copilot-bluespec unit tests\n\n[ci skip]","shortMessageHtmlLink":"Draft: copilot-bluespec unit tests"}},{"before":"9b4c098e4b2786168105222fbf3021bb60290123","after":"ff34ac0f79cbc4e4c3dca6ddb33ebd6e0c1cbfb1","ref":"refs/heads/develop-bluespec-tests","pushedAt":"2024-01-14T21:06:43.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Draft: copilot-bluespec unit tests\n\n[ci skip]","shortMessageHtmlLink":"Draft: copilot-bluespec unit tests"}},{"before":null,"after":"9b4c098e4b2786168105222fbf3021bb60290123","ref":"refs/heads/develop-bluespec-tests","pushedAt":"2024-01-14T04:04:46.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Draft: copilot-bluespec unit tests\n\n[ci skip]","shortMessageHtmlLink":"Draft: copilot-bluespec unit tests"}},{"before":"cf9e5b848d7078a1e6b151074390acadd52e7fe0","after":"db755d631e3d2deb8939aba1f171d833d05140b4","ref":"refs/heads/develop-bluespec-bsv","pushedAt":"2024-01-14T01:58:57.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Try Bluespec SystemVerilog","shortMessageHtmlLink":"Try Bluespec SystemVerilog"}},{"before":"8ac2da0bb8d30b3bf1786f92b4da3e58bdc9fd0e","after":"cf9e5b848d7078a1e6b151074390acadd52e7fe0","ref":"refs/heads/develop-bluespec-bsv","pushedAt":"2024-01-14T00:01:17.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Try Bluespec SystemVerilog","shortMessageHtmlLink":"Try Bluespec SystemVerilog"}},{"before":"54704450a6acd12fc971d62c5acec1f4771ebbd0","after":"8ac2da0bb8d30b3bf1786f92b4da3e58bdc9fd0e","ref":"refs/heads/develop-bluespec-bsv","pushedAt":"2024-01-13T23:56:47.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Bump language-bluespec submodule","shortMessageHtmlLink":"Bump language-bluespec submodule"}},{"before":"16f6ebc6bb12893eaff3980fc5b5dfa6a49747a6","after":"54704450a6acd12fc971d62c5acec1f4771ebbd0","ref":"refs/heads/develop-bluespec-bsv","pushedAt":"2024-01-13T23:51:29.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Bump language-bluespec submodule","shortMessageHtmlLink":"Bump language-bluespec submodule"}},{"before":"6a868dc570a4927abf7317c6b33a5a973eefb33a","after":"dac050b22531599597137d69254fa0699d2bb286","ref":"refs/heads/develop-bluespec","pushedAt":"2024-01-13T23:35:58.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Fill in more details in DESIGN document","shortMessageHtmlLink":"Fill in more details in DESIGN document"}},{"before":"ca738f7a57c3b8c5a08b4dae1baf2df343e57882","after":"835deafa4727c60741337a84cf7b8dce705f6e41","ref":"refs/heads/master","pushedAt":"2024-01-08T14:53:03.000Z","pushType":"push","commitsCount":15,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Merge branch 'release-3.18.1'. Close #493.\n\n**Description**\n\nVersion 3.18.1 of Copilot is ready and should be closed and published on\nHackage.\n\n**Type**\n\n- Management: release and publication.\n\n**Additional context**\n\nNone.\n\n**Requester**\n\n- Ivan Perez.\n\n**Method to check presence of bug**\n\nNot applicable (not a bug).\n\n**Expected result**\n\n- Cabal files indicate new version number, constraints are adjusted as\n  needed, commit is tagged with version number, and packages are\n  published on Hackage.\n\n- The following docker image installs copilot enforcing the new version\n  via compiler constraints. It prints the message \"Success\" at the end\n  if all completes correctly, and shows an error message otherwise.\n\n```Dockerfile\nFROM ubuntu:focal\n\nRUN apt-get update\n\nRUN apt-get install --yes libz-dev\nRUN apt-get install --yes git\n\nRUN apt-get install --yes wget\nRUN mkdir -p $HOME/.ghcup/bin\nRUN wget https://downloads.haskell.org/~ghcup/0.1.17.7/x86_64-linux-ghcup-0.1.17.7 -O $HOME/.ghcup/bin/ghcup\n\nRUN chmod a+x $HOME/.ghcup/bin/ghcup\nENV PATH=$PATH:/root/.ghcup/bin/\nENV PATH=$PATH:/root/.cabal/bin/\nRUN apt-get install --yes curl\nRUN apt-get install --yes gcc g++ make libgmp3-dev\nRUN ghcup install ghc 9.6.3\nRUN ghcup install cabal 3.4\nRUN ghcup set ghc 9.6.3\nRUN cabal update\n\nSHELL [\"/bin/bash\", \"-c\"]\nCMD git clone $REPO \\\n    && cd $NAME \\\n    && git checkout $COMMIT \\\n    && cabal install --lib copilot**/ \\\n         --constraint=\"copilot==3.18.1\" \\\n         --constraint=\"copilot-c99==3.18.1\" \\\n         --constraint=\"copilot-core==3.18.1\" \\\n         --constraint=\"copilot-prettyprinter==3.18.1\" \\\n         --constraint=\"copilot-interpreter==3.18.1\" \\\n         --constraint=\"copilot-language==3.18.1\" \\\n         --constraint=\"copilot-libraries==3.18.1\" \\\n         --constraint=\"copilot-theorem==3.18.1\" \\\n    && echo Success\n```\nCommand (substitute variables based on new path after merge):\n```\n$ docker run -e \"REPO=https://github.com/Copilot-Language/copilot\" -e \"NAME=copilot\" -e \"COMMIT=<HASH>\" -it copilot-verify-491\n```\n\n**Solution implemented**\n\n- Cabal files indicate new version number, constraints are adjusted as\n  needed, commit is tagged with version number, and packages are\n  published on Hackage.\n\n**Further notes**\n\nNone.","shortMessageHtmlLink":"Merge branch 'release-3.18.1'. <span class=\"issue-keyword tooltipped tooltipped-se\" aria-label=\"This commit closes issue #493.\">Close</span> <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2069996047\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Copilot-Language/copilot/issues/493\" data-hovercard-type=\"issue\" data-hovercard-url=\"/Copilot-Language/copilot/issues/493/hovercard\" href=\"https://github.com/Copilot-Language/copilot/issues/493\">Copilot-Language#493</a>."}},{"before":"5ee005e223f6ea8a1eadcdbc9b1795da70ba8bdc","after":"ca738f7a57c3b8c5a08b4dae1baf2df343e57882","ref":"refs/heads/master","pushedAt":"2024-01-07T20:30:55.000Z","pushType":"push","commitsCount":7,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Merge branch 'develop-misra-2012'. Close #472.\n\n**Description**\n\nThe code generated by Copilot is not fully compliant with MISRA C. At\npresent, it complies with all but one rules, and all but two directives\nof MISRA C 2012.\n\nDue to the nature of this project and the environment where it is meant\nto be used, we want to have compliance with all MISRA C rules, and if\npossible with all MISRA C directives.\n\nAny deviations should be properly justified and documented.\n\n**Type**\n\n- Feature: Compliance with MISRA C 2012.\n\n**Additional context**\n\nNone.\n\n**Requester**\n\n- Patrick Quach (NASA)\n\n**Method to check presence of bug**\n\nNot applicable (not a bug).\n\n**Expected result**\n\nThe code produced by Copilot complies with all rules in MISRA C 2012.\nAny deviations from any rules or directives are documented and\njustified.\n\n**Solution implemented**\n\nModify `copilot-c99` to add keyword `static` to guards and generator\nfunctions. That requires using language-c99-simple >= 0.3.\n\nModify `copilot-c99` backend to explicitly cast constants to `size_t` in\nmanipulations of the ring buffers.\n\nAdd a tool to the CI process that checks for compliance with the standard.\n\n**Further notes**\n\nThe solution includes a new test in the CI setup that uses cppcheck to\ncheck that a Copilot-generated C file complies with MISRA C. The test is\nbeing executed by the CI setup (see:\nhttps://app.travis-ci.com/github/Copilot-Language/copilot/jobs/615908458#L1976-L1978).\n\nFurthermore, Parasoft has been used to manually check the same example\nfor compliance. Parasoft's tool reports a violation of one advisory\nonly: Directive 4.6. Complying with that recommendation would require\nusing specific types that indicate the size and signedness instead of\nfloat and double. Although we could call those float32_t and float64_t,\nthere is in principle no guarantee that those will be the sizes in all\narchitectures, making such names potentially misleading. Since this is a\nrecommendation, we decide to accept non-compliance with this directive.\n\nThis change does not modify the README, contrary to the solution\noriginally proposed. This is intentional: there is no suitable place to\nindicate information about compliance, or lack thereof, with MISRA C.\nWe decide to defer this change, and suggest extending the README to show\nthe features of Copilot more prominently. That will create the space to\ntalk about MISRA compliance and also list the advisory we do not\ncurrently comply with.","shortMessageHtmlLink":"Merge branch 'develop-misra-2012'. <span class=\"issue-keyword tooltipped tooltipped-se\" aria-label=\"This commit closes issue #472.\">Close</span> <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2033901199\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Copilot-Language/copilot/issues/472\" data-hovercard-type=\"issue\" data-hovercard-url=\"/Copilot-Language/copilot/issues/472/hovercard\" href=\"https://github.com/Copilot-Language/copilot/issues/472\">Copilot-Language#472</a>."}},{"before":"9091ce12d59ff27c327ecfcae661f7d2261d55e0","after":"6a868dc570a4927abf7317c6b33a5a973eefb33a","ref":"refs/heads/develop-bluespec","pushedAt":"2024-01-05T21:00:34.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Fill in more details in DESIGN document","shortMessageHtmlLink":"Fill in more details in DESIGN document"}},{"before":"cb1be17d64903977bfbd668e8c4fd94e84bb19c5","after":"9091ce12d59ff27c327ecfcae661f7d2261d55e0","ref":"refs/heads/develop-bluespec","pushedAt":"2024-01-01T15:21:52.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"DESIGN: Minor fixes","shortMessageHtmlLink":"DESIGN: Minor fixes"}},{"before":"cfc565bcf52dd359eb7ee768549459402c1785df","after":"5ee005e223f6ea8a1eadcdbc9b1795da70ba8bdc","ref":"refs/heads/master","pushedAt":"2023-12-30T14:45:28.000Z","pushType":"push","commitsCount":32,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Merge branch 'develop-forall'. Close #470.\n\n**Description**\n\nThe Copilot API offers the function `Copilot.Language.Spec.forall`,\nwhich future versions of GHC will disallow.\n\nTo ensure that Copilot keeps working with future versions of the\ncompiler, this function should be renamed.\n\n**Type**\n\n- Management: change to keep Copilot working with future versions of the\n  language/compiler.\n\n**Additional context**\n\nThe proposal was filed in\nhttps://github.com/ghc-proposals/ghc-proposals/pull/281, and\nsubsequently accepted in GHC. Details are also available at:\nhttps://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wforall-identifier.\n\n**Requester**\n\n- Ivan Perez\n\n**Method to check presence of bug**\n\nAlthough not a bug, it is possible to detect the presence of this issue\nby compiling with GHC >= 9.4. Using `-Werror=forall-identifier` will\nmake the issue become a compile-time error.\n\nWe cannot yet use a test that will produce a failure (expected) if\nforall is defined (i.e., with -Werror=forall-keyword) because we have to\ndeprecate the function before we remove it.\n\nThe following Dockerfile checks that the function forall has been\ndeprecated and that the alterative forAll is offered, in which case\nprints the message Success:\n```\nFROM ubuntu:focal\n\nRUN apt-get update\n\nRUN apt-get install --yes libz-dev\nRUN apt-get install --yes git\n\nRUN apt-get install --yes wget\nRUN mkdir -p $HOME/.ghcup/bin\nRUN wget https://downloads.haskell.org/~ghcup/0.1.19.2/x86_64-linux-ghcup-0.1.19.2 -O $HOME/.ghcup/bin/ghcup\n\nRUN chmod a+x $HOME/.ghcup/bin/ghcup\nENV PATH=$PATH:/root/.ghcup/bin/\nENV PATH=$PATH:/root/.cabal/bin/\nRUN apt-get install --yes curl\nRUN apt-get install --yes gcc g++ make libgmp3-dev\n\nSHELL [\"/bin/bash\", \"-c\"]\n\nRUN ghcup install ghc 9.4\nRUN ghcup install cabal 3.2\nRUN ghcup set ghc 9.4.8\nRUN cabal update\n\nSHELL [\"/bin/bash\", \"-c\"]\nCMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \\\n  && cabal v1-sandbox init \\\n  && cabal v1-install alex happy \\\n  && cabal v1-install copilot/**/ \\\n  && ! cabal v1-exec -- runhaskell -Werror=deprecations <<< 'import Copilot.Language (true, forall, theorem); spec = theorem \"true\" (forall true); main :: IO (); main = pure ();' \\\n  && cabal v1-exec -- runhaskell -Werror=forall-identifier -Werror=deprecations <<< 'import Copilot.Language (true, forAll, theorem); spec = theorem \"true\" (forAll true); main :: IO (); main = pure ();' \\\n  && echo \"Success\"\n```\n\nCommand (substitute variables based on new path after merge):\n```\n$ docker run -e \"REPO=https://github.com/Copilot-Language/copilot\" -e \"NAME=copilot\" -e \"COMMIT=<HASH>\" -it copilot-verify-470\n```\n\n**Expected result**\n\nRunning the Dockerfile above prints the message \"Success\", indicating\nthat the old forall function is deprecated and a new variant is being\noffered.\n\n**Solution implemented**\n\nIntroduce a new function `forAll` that implements the behavior currently\nimplemented by `forall`.\n\nReplace all references of `forall` to point to `forAll`, including\noccurrences in tests and examples.\n\nDeprecate `forall`.\n\n**Further notes**\n\nNone.","shortMessageHtmlLink":"Merge branch 'develop-forall'. <span class=\"issue-keyword tooltipped tooltipped-se\" aria-label=\"This commit closes issue #470.\">Close</span> <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1992009385\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Copilot-Language/copilot/issues/470\" data-hovercard-type=\"issue\" data-hovercard-url=\"/Copilot-Language/copilot/issues/470/hovercard\" href=\"https://github.com/Copilot-Language/copilot/issues/470\">Copilot-Language#470</a>."}},{"before":"e975b4a0e007241f14e1c1032f46111ec4d69e83","after":null,"ref":"refs/heads/develop-fix-trigger-arg-arrays","pushedAt":"2023-12-20T07:32:50.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"}},{"before":"ef70d5c9141543d1cc0005bcc85916b3a55c36f0","after":"e975b4a0e007241f14e1c1032f46111ec4d69e83","ref":"refs/heads/develop-fix-trigger-arg-arrays","pushedAt":"2023-12-19T19:53:05.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"copilot-c99: Document changes in CHANGELOG. Refs #431.","shortMessageHtmlLink":"copilot-c99: Document changes in CHANGELOG. Refs <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1649623890\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Copilot-Language/copilot/issues/431\" data-hovercard-type=\"issue\" data-hovercard-url=\"/Copilot-Language/copilot/issues/431/hovercard\" href=\"https://github.com/Copilot-Language/copilot/issues/431\">Copilot-Language#431</a>."}},{"before":null,"after":"ef70d5c9141543d1cc0005bcc85916b3a55c36f0","ref":"refs/heads/develop-fix-trigger-arg-arrays","pushedAt":"2023-12-19T19:50:45.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"copilot-c99: Document changes in CHANGELOG. Refs #431.","shortMessageHtmlLink":"copilot-c99: Document changes in CHANGELOG. Refs <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1649623890\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Copilot-Language/copilot/issues/431\" data-hovercard-type=\"issue\" data-hovercard-url=\"/Copilot-Language/copilot/issues/431/hovercard\" href=\"https://github.com/Copilot-Language/copilot/issues/431\">Copilot-Language#431</a>."}},{"before":"82bbd26859e499632268d959fa3181500c7e5f59","after":"f8da7d66bfd97a14a695fea460e625c8aae9ac11","ref":"refs/heads/T431","pushedAt":"2023-12-13T13:05:34.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"copilot-c99: Document changes in CHANGELOG. Refs TODO RGS.","shortMessageHtmlLink":"copilot-c99: Document changes in CHANGELOG. Refs TODO RGS."}},{"before":"eeed69c3c4bff75ce2a2125cd1057eef77c2d556","after":"cfc565bcf52dd359eb7ee768549459402c1785df","ref":"refs/heads/master","pushedAt":"2023-12-09T22:21:55.000Z","pushType":"push","commitsCount":78,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Merge branch 'release-3.17'. Close #466.\n\n**Description**\n\nVersion 3.17 of Copilot is ready and should be closed and published on Hackage.\n\n**Type**\n\n- Management: release and publication.\n\n**Additional context**\n\nNone.\n\n**Requester**\n\n- Ivan Perez.\n\n**Method to check presence of bug**\n\nNot applicable (not a bug).\n\n**Expected result**\n\n- Cabal files indicate new version number, constraints are adjusted as\n  needed, commit is tagged with version number, and packages are\n  published on Hackage.\n\n- The following docker image installs copilot enforcing the new version\n  via compiler constraints. It prints the message \"Success\" at the end\n  if all completes correctly, and shows an error message otherwise.\n\n```Dockerfile\nFROM ubuntu:focal\n\nRUN apt-get update\n\nRUN apt-get install --yes libz-dev\nRUN apt-get install --yes git\n\nRUN apt-get install --yes wget\nRUN mkdir -p $HOME/.ghcup/bin\nRUN wget https://downloads.haskell.org/~ghcup/0.1.17.7/x86_64-linux-ghcup-0.1.17.7 -O $HOME/.ghcup/bin/ghcup\n\nRUN chmod a+x $HOME/.ghcup/bin/ghcup\nRUN chmod a+x $HOME/.ghcup/bin/ghcup\nENV PATH=$PATH:/root/.ghcup/bin/\nENV PATH=$PATH:/root/.cabal/bin/\nRUN apt-get install --yes curl\nRUN apt-get install --yes gcc make libgmp3-dev\nRUN ghcup install ghc 9.0\nRUN ghcup install cabal 3.4\nRUN ghcup set ghc 9.0.2\nRUN cabal update\n\nSHELL [\"/bin/bash\", \"-c\"]\nCMD git clone $REPO \\\n    && cd $NAME \\\n    && git checkout $COMMIT \\\n    && cabal install --lib copilot**/ \\\n         --constraint=\"copilot==3.17\" \\\n         --constraint=\"copilot-c99==3.17\" \\\n         --constraint=\"copilot-core==3.17\" \\\n         --constraint=\"copilot-prettyprinter==3.17\" \\\n         --constraint=\"copilot-interpreter==3.17\" \\\n         --constraint=\"copilot-language==3.17\" \\\n         --constraint=\"copilot-libraries==3.17\" \\\n         --constraint=\"copilot-theorem==3.17\" \\\n    && echo Success\n```\nCommand (substitute variables based on new path after merge):\n```\n$ docker run -e \"REPO=https://github.com/Copilot-Language/copilot\" -e \"NAME=copilot\" -e \"COMMIT=<HASH>\" -it copilot-verify-466\n```\n\n**Solution implemented**\n\n- Cabal files indicate new version number, constraints are adjusted as\n  needed, commit is tagged with version number, and packages are\n  published on Hackage.\n\n**Further notes**\n\nNone.","shortMessageHtmlLink":"Merge branch 'release-3.17'. <span class=\"issue-keyword tooltipped tooltipped-se\" aria-label=\"This commit closes issue #466.\">Close</span> <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1982011419\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Copilot-Language/copilot/issues/466\" data-hovercard-type=\"issue\" data-hovercard-url=\"/Copilot-Language/copilot/issues/466/hovercard\" href=\"https://github.com/Copilot-Language/copilot/issues/466\">Copilot-Language#466</a>."}},{"before":null,"after":"82bbd26859e499632268d959fa3181500c7e5f59","ref":"refs/heads/T431","pushedAt":"2023-12-09T22:13:16.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Draft: T431","shortMessageHtmlLink":"Draft: T431"}},{"before":null,"after":"16f6ebc6bb12893eaff3980fc5b5dfa6a49747a6","ref":"refs/heads/develop-bluespec-bsv","pushedAt":"2023-10-29T20:42:56.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Bump language-bluespec submodule","shortMessageHtmlLink":"Bump language-bluespec submodule"}},{"before":"34b454513d43db86fa1b0b1c648bf05a7b233949","after":"eeed69c3c4bff75ce2a2125cd1057eef77c2d556","ref":"refs/heads/master","pushedAt":"2023-08-16T13:44:08.000Z","pushType":"push","commitsCount":32,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Merge branch 'develop-majority'. Close #408.\n\n**Description**\n\nThe function `Copilot.Library.Voting.majority'`, used to implement majority\nvoting, produces code that may potentially contain unused variables.\n\nIn particular, when the argument list of that function, with signature:\n\n```haskell\nmajority' :: (P.Eq a, Typed a) => [Stream a] -> Stream a -> Stream Word32 -> Stream a\n```\n\nonly has one element, Copilot will generate code with unused local variables.\nThis happens in almost every case, since the function is called recursively\nwith a smaller list at every step.\n\nThe C code generated by Copilot contains unused variables, which trigger\nwarnings when compiled with `-Wall`.\n\n**Type**\n\n- Bug: code generated by Copilot produces warnings.\n\n**Additional context**\n\nNone.\n\n**Requester**\n\n- Ryan Scott (Galois)\n\n**Method to check presence of bug**\n\nThe following Dockerfile checks that the implementation of majority produces\ncode without unused local variables (it checks that it produces code that\ncompiles with no warnings, and the GCC compiler installed by this docker script\nproduces warnings by default for unused local variables). In that case, it\nprints the message Success:\n\n```Dockerfile\n--- Dockerfile\nFROM ubuntu:trusty\n\nRUN apt-get update\n\nRUN apt-get install --yes software-properties-common\nRUN add-apt-repository ppa:hvr/ghc\nRUN apt-get update\n\nRUN apt-get install --yes ghc-8.6.5 cabal-install-2.4\nRUN apt-get install --yes libz-dev\n\nENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH\n\nRUN cabal update\nRUN cabal v1-sandbox init\nRUN apt-get install --yes git\n\nADD Spec.hs /tmp/Spec.hs\n\nSHELL [\"/bin/bash\", \"-c\"]\nCMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \\\n  && cabal v1-install alex happy \\\n  && cabal v1-install $NAME/copilot**/ \\\n  && cabal v1-exec -- runhaskell /tmp/Spec.hs \\\n  && gcc -Werror -Wall maj.c -c -o maj.o \\\n  && echo \"Success\"\n\n--- Spec.hs\nmodule Main where\n\nimport Language.Copilot\nimport Copilot.Compile.C99\nimport qualified Copilot.PrettyPrint as PP\n\nspec :: Spec\nspec = trigger \"maj\" (majority [true, true]) []\n\nmain :: IO ()\nmain =\n  reify spec >>= compile \"maj\"\n```\n\nCommand (substitute variables based on new path after merge):\n```\n$ docker run -e \"REPO=https://github.com/Copilot-Language/copilot\" -e \"NAME=copilot\" -e \"COMMIT=<HASH>\" -it copilot-verify-408.\n```\n\n**Expected result**\n\nThe dockerfile above should print \"Success\", indicating that the code produced\nby the use of the `majority` function compiles without any warnings (including\nany warnings due to unused variables).\n\n**Solution implemented**\n\nModify the implementation of `Copilot.Library.Voting.majority'` to account for\nthe case in which the argument list only has one element, and specialize the\nimplementation of `inCan` to not create a local variable in that case.\n\n**Further notes**\n\nWe could address this also during reification by traversing specs and removing\nunused variables. In this case, the conceptual error exists in the definition\nof `Copilot.Library.Voting.majority'`, so it's good to fix it there.\nNevertheless, the introduction of dead-code elimination in the Copilot compiler\ncould be useful in the future.","shortMessageHtmlLink":"Merge branch 'develop-majority'. <span class=\"issue-keyword tooltipped tooltipped-se\" aria-label=\"This commit closes issue #408.\">Close</span> <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1529810135\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Copilot-Language/copilot/issues/408\" data-hovercard-type=\"issue\" data-hovercard-url=\"/Copilot-Language/copilot/issues/408/hovercard\" href=\"https://github.com/Copilot-Language/copilot/issues/408\">Copilot-Language#408</a>."}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEQgayUQA","startCursor":null,"endCursor":null}},"title":"Activity · GaloisInc/copilot-1"}