{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":37164878,"defaultBranch":"master","name":"copilot","ownerLogin":"Copilot-Language","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2015-06-09T23:48:41.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/12819929?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1715154358.0","currentOid":""},"activityList":{"items":[{"before":"2fc1cbde7072a6ce881981e60054665a46b509fb","after":"9e4b1cbf8ec250ccc53e96e93339efd2b4d474b5","ref":"refs/heads/master","pushedAt":"2024-05-08T07:45:50.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Merge branch 'release-3.19.1'. Close #512.\n\n**Description**\n\nVersion 3.19.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\nENV DEBIAN_FRONTEND=noninteractive\n\nRUN apt-get update\n\nRUN apt-get install --yes libz-dev pkg-config\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.19.1\" \\\n --constraint=\"copilot-c99==3.19.1\" \\\n --constraint=\"copilot-core==3.19.1\" \\\n --constraint=\"copilot-prettyprinter==3.19.1\" \\\n --constraint=\"copilot-interpreter==3.19.1\" \\\n --constraint=\"copilot-language==3.19.1\" \\\n --constraint=\"copilot-libraries==3.19.1\" \\\n --constraint=\"copilot-theorem==3.19.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=\" -it copilot-verify-512\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.19.1'. Close #512."}},{"before":"1991df820e9c5da524f61b0924a1f4e541e360fe","after":"2fc1cbde7072a6ce881981e60054665a46b509fb","ref":"refs/heads/master","pushedAt":"2024-05-08T06:03:17.000Z","pushType":"push","commitsCount":13,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Merge remote-tracking branch 'fdedden/develop-fix-nonexisting-readme'. Close #452.\n\n**Description**\n\n`copilot-theorem`'s README mentions a file `Driver.hs` that is not part\nof the library:\n```\nAs an example, the following prover is used in Driver.hs:\n```\nand later\n```\nSome examples are in the examples folder. The Driver.hs contains the\nmain function to run any example.\n```\n\nIt also says that there are two provers: one based on `Kind2`, and one\ncalled `lightProver`. The latter no longer exists, but we do have a\n`What4` module now.\n\nThese mentions should be adjusted or removed.\n\n**Type**\n\n- Bug: incorrect documentation.\n\n**Additional context**\n\nNone.\n\n**Requester**\n\n- Max Fan (NASA)\n\n**Method to check presence of bug**\n\nRunning a search through the tree brings up several mentions:\n```\n$ grep -nIHre 'Driver.hs'\ncopilot-theorem/README.md:205:As an example, the following prover is used in `Driver.hs`:\ncopilot-theorem/README.md:254:Some examples are in the *examples* folder. The `Driver.hs` contains the `main`\ncopilot-theorem/README.md:257:by changing one *import* directive in `Driver.hs`.\n```\n\n```\n$ grep -nIHre 'lightProver'\ncopilot-theorem/README.md:79:prove (lightProver def) (check \"gt0\") spec\ncopilot-theorem/README.md:82:where `lightProver def` stands for the *light prover* with default\ncopilot-theorem/README.md:150:`lightProver :: Options -> Prover` function which builds a prover from a record\ncopilot-theorem/README.md:209: lightProver def {onlyBmc = True, kTimeout = 5}\n```\n\n```\n$ grep -nIHre '\\' | grep -ve 'XML'\ncopilot-theorem/README.md:71: the `Copilot.Theorem.Light` and `Copilot.Theorem.Kind2` module.\ncopilot-theorem/README.md:123:Two provers are provided by default: `Light` and `Kind2`.\ncopilot-theorem/README.md:149:The *light prover* is defined in `Copilot.Theorem.Light`. This module exports the\ncopilot-theorem/README.md:399:#### The Light prover\ncopilot-theorem/README.md:402:basic *k-induction* algorithm [1]. The `Light` directory contains three files:\n```\n\n**Expected result**\n\nThe output of the above `grep` commands is empty, indicating that that\ninexisting file/modules/functions are not mentioned.\n\n**Solution implemented**\n\nThe README has been adjusted to match the current interface.\nSpecifically, the references above have been fixed, and any code\nexamples updated to use currently supported APIs.\n\n**Further notes**\n\nNone.","shortMessageHtmlLink":"Merge remote-tracking branch 'fdedden/develop-fix-nonexisting-readme'. …"}},{"before":"f8239019b9c83315a78e2a92221b862945aa3b7c","after":"1991df820e9c5da524f61b0924a1f4e541e360fe","ref":"refs/heads/master","pushedAt":"2024-05-07T14:15:53.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Merge remote-tracking branch 'galois/develop-issue495-kind2Prover-falsifiable'. Close #495.\n\n**Description**\n\n`copilot-theorem` crashes when trying to disprove a property that is\nfalse using `kind2Prover`.\n\n`kind2Prover` expects the word used in kind2's XML output to be\n`invalid`, but the keyword used is `falsifiable`, leading to a parse\nerror.\n\n**Type**\n\n- Bug: crash when passing valid input to function.\n\n**Additional context**\n\nNone.\n\n**Requester**\n\n- Ryan Scott (Galois)\n\n**Method to check presence of bug**\n\nAttempting to run the following spec with kind2-0.7.2:\n\n```haskell\nmodule Main (main) where\n\nimport Data.Functor\n\nimport Copilot.Theorem.Kind2\nimport Copilot.Theorem.Prove\nimport Language.Copilot\n\nspec :: Spec\nspec =\n void $ theorem \"false\" (forAll false) (check (kind2Prover def))\n\nmain :: IO ()\nmain = void $ reify spec\n```\n\nleads to a crash due to a parse error:\n\n```\nSpec.hs: Parse error while reading the Kind2 XML output :\nUnrecognized status : falsifiable\n\n\n\nkind2 v0.7.2\n\n 0.122\n 1\n falsifiable\n \n\n\n\n\nCallStack (from HasCallStack):\n error, called at src/Copilot/Theorem/Misc/Error.hs:32:9 in copilot-theorem-3.19-CUYLKPoYpZX7ZyknpdGomd:Copilot.Theorem.Misc.Error\n```\n\nThe following Dockerfile checks that running the above Spec completes\nsuccessfully, in which case it prints the message \"Success\":\n\n```\n--- Dockerfile\nFROM ubuntu:focal\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 \\\n ghc-8.6.5 cabal-install-2.4 \\\n libtool-bin libz-dev libzmq5 opam z3\n\n # Install Kind2's OCaml dependencies\nRUN opam init --auto-setup --yes --bare --disable-sandboxing \\\n && opam switch create default 4.01.0 \\\n && opam install -y -j \"$(nproc)\" camlp4 menhir \\\n && opam clean -a -c -s --logs\n\n # Install Kind2-0.7.2\nENV KIND2_VER=\"0.7.2\"\nRUN wget https://github.com/kind2-mc/kind2/archive/refs/tags/v${KIND2_VER}.zip \\\n && unzip v${KIND2_VER}.zip\nWORKDIR kind2-${KIND2_VER}\nRUN sed -i.bak -e 's/-pedantic -Werror -Wall/-pedantic -Wall/' ocamlczmq/czmq/configure.ac\nRUN eval $(opam env) \\\n && ./autogen.sh \\\n && ./build.sh \\\n && make install\nWORKDIR /\n\n # Install GHC and Cabal\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 | grep \"false: proof failed\") \\\n && echo \"Success\"\n\n--- Spec.hs\nmodule Main (main) where\n\nimport Data.Functor\n\nimport Copilot.Theorem.Kind2\nimport Copilot.Theorem.Prove\nimport Language.Copilot\n\nspec :: Spec\nspec =\n void $ theorem \"false\" (forAll false) (check (kind2Prover def))\n\nmain :: IO ()\nmain = void $ reify spec\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=\" -it copilot-verify-495\n```\n\n**Expected result**\n\nRunning the Dockerfile above prints the message \"Success\", indicating\nthat the spec was proven falsifiable using kind2, and that the output\nfrom Copilot contained the text \"false: proof failed\" (as expected).\n\n**Solution implemented**\n\nModify `copilot-theorem:Copilot.Theorem.Kind2.Output.parseOutput` to\nexpect the word `falsifiable`, rather than `invalid`.\n\n**Further notes**\n\nNone.","shortMessageHtmlLink":"Merge remote-tracking branch 'galois/develop-issue495-kind2Prover-fal…"}},{"before":"58809726f6c38f0f0aab04c8d1be133c7036d4d4","after":null,"ref":"refs/heads/release-3.19","pushedAt":"2024-03-08T09:13:11.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"}},{"before":"3725ca21ada9fa2912b6f95414be57cafe49701f","after":"f8239019b9c83315a78e2a92221b862945aa3b7c","ref":"refs/heads/master","pushedAt":"2024-03-08T09:10:26.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Merge branch 'release-3.19'. Close #504.\n\n**Description**\n\nVersion 3.19 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\nENV DEBIAN_FRONTEND=noninteractive\n\nRUN apt-get update\n\nRUN apt-get install --yes libz-dev pkg-config\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.19\" \\\n --constraint=\"copilot-c99==3.19\" \\\n --constraint=\"copilot-core==3.19\" \\\n --constraint=\"copilot-prettyprinter==3.19\" \\\n --constraint=\"copilot-interpreter==3.19\" \\\n --constraint=\"copilot-language==3.19\" \\\n --constraint=\"copilot-libraries==3.19\" \\\n --constraint=\"copilot-theorem==3.19\" \\\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=\" -it copilot-verify-504\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.19'. Close #504."}},{"before":null,"after":"58809726f6c38f0f0aab04c8d1be133c7036d4d4","ref":"refs/heads/release-3.19","pushedAt":"2024-03-08T08:07:00.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Document changes in CHANGELOG. Refs #504.","shortMessageHtmlLink":"Document changes in CHANGELOG. Refs #504."}},{"before":"fbe9d596f709395c99dd31d8218d2b03ee02f08f","after":"3725ca21ada9fa2912b6f95414be57cafe49701f","ref":"refs/heads/master","pushedAt":"2024-03-08T08:00:05.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Merge branch 'develop-core-tests-coverage'. Close #502.\n\n**Description**\n\nThe test coverage of `copilot-core` is currently reported at 25% by\nHackage. This is very low.\n\nAlthough there are exceptions to what we can test (record fields of\nexistential types) or should tests (proxies, automatically generated\nconstructors and accessor functions), the coverage of our tests should\nbe higher and anything that is not tested should be documented.\n\n**Type**\n\n- Maintenance: Increase coverage of tests.\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\nAll top-level functions that are not automatically generated by the\ncompiler are tested, except where testing them is not possible or for\ncode that is automatically generated (constructors, record accessor\nfunctions). Anything not tested is documented.\n\n**Solution implemented**\n\nAdd tests for all definitions in `Copilot.Core.Type` and\n`Copilot.Core.Type.Array`, except record accessor functions.\n\nRunning tests with coverage enabled achieves coverage of 97% for\ntop-level definitions (37 out of 38 definitions). The one not tested is\nuTypeType, which cannot be tested due to being part of an existential\ntype (it's necessity is being discussed in issue 484). The modules\nCopilot.Core.Operators and Copilot.Core.Spec and Copilot.Core.Expr only\ncontain datatype definitions, so they do not need to be tested.\n\n**Further notes**\n\nNone.","shortMessageHtmlLink":"Merge branch 'develop-core-tests-coverage'. Close #502."}},{"before":"9c121baae0528dca32a4a0bb1790d4f7604eb72e","after":null,"ref":"refs/heads/develop-core-tests-coverage","pushedAt":"2024-03-08T07:23:41.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"}},{"before":null,"after":"9c121baae0528dca32a4a0bb1790d4f7604eb72e","ref":"refs/heads/develop-core-tests-coverage","pushedAt":"2024-03-08T06:56:29.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"copilot-core: Document changes in CHANGELOG. Refs #502.","shortMessageHtmlLink":"copilot-core: Document changes in CHANGELOG. Refs #502."}},{"before":"835deafa4727c60741337a84cf7b8dce705f6e41","after":"fbe9d596f709395c99dd31d8218d2b03ee02f08f","ref":"refs/heads/master","pushedAt":"2024-03-08T03:14:39.000Z","pushType":"push","commitsCount":8,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Merge branch 'develop-remove-deprecatedType'. Close #500.\n\n**Description**\n\nThe functions `Copilot.Core.Type.typename`,\n`Copilot.Core.Type.tylength`, `Copilot.Core.Type.tysize`,\n`Copilot.Core.Type.fieldname`, `Copilot.Core.Type.accessorname` and\n`Copilot.Core.Type.Array.arrayelems` are not being used by any other\npart of Copilot.\n\nThey were replaced by functions with similar names in lowerCamelCase\nformat. The original functions were deprecated in Copilot 3.17 and no\nmessages have been received requesting that they be kept in this\nlibrary.\n\nAs per our internal policy of waiting 3 versions from deprecation until\na public interface declaration can be removed, these functions can now\nbe removed.\n\n**Type**\n\n- Bug: unused code included in the implementation.\n\n**Additional context**\n\n- Issue #457, addressed in Copilot 3.17, deprecated the functions.\n\n**Requester**\n\n- Ivan Perez\n\n**Method to check presence of bug**\n\nThere is no easy, forward-compatible, automated way of detecting that\nthe functions are present and also deprecated. Manual inspection is\nrecommended. At present, they are the only deprecated functions in\n`copilot-core`, so their presence can be found with:\n\n```sh\n$ grep -nHre 'DEPRECATED' src/\nsrc/Copilot/Core/Type.hs:58:-- {-# DEPRECATED typename \"Use typeName instead.\" #-}\nsrc/Copilot/Core/Type.hs:85:-- {-# DEPRECATED fieldname \"Use fieldName instead.\" #-}\nsrc/Copilot/Core/Type.hs:96:-- {-# DEPRECATED accessorname \"Use accessorName instead.\" #-}\nsrc/Copilot/Core/Type.hs:139:-- {-# DEPRECATED tylength \"Use typeLength instead.\" #-}\nsrc/Copilot/Core/Type.hs:149:-- {-# DEPRECATED tysize \"Use typeSize instead.\" #-}\nsrc/Copilot/Core/Type/Array.hs:47:{-# DEPRECATED arrayelems \"Use ArrayElems instead.\" #-}\n```\n\n**Expected result**\n\nThe strings returned by the command above should be empty (nothing is\ndeprecated).\n\n**Solution implemented**\n\nRemove the deprecated functions from `Copilot.Core.Type` and\n`Copilot.Core.Type.Array`.\n\n**Further notes**\n\nNone.","shortMessageHtmlLink":"Merge branch 'develop-remove-deprecatedType'. Close #500."}},{"before":"266a2d3bf41381669ac32bb6a8d889b175ec2359","after":"835deafa4727c60741337a84cf7b8dce705f6e41","ref":"refs/heads/master","pushedAt":"2024-01-08T09:43:41.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?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=\" -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'. Close #493."}},{"before":"a53f5320842276019fa2fe1c1dce863f6ff8b6e4","after":"266a2d3bf41381669ac32bb6a8d889b175ec2359","ref":"refs/heads/master","pushedAt":"2024-01-08T08:55:21.000Z","pushType":"push","commitsCount":6,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Merge branch 'develop-ghc-9.6.3'. Close #491.\n\n**Description**\n\n`copilot-theorem` is failing to compile with GHC 9.6.3. This is because\nthe module `Control.Monad.State` no longer re-exports `Control.Monad`,\nso the functions `ap`, `forM`, `when`, `liftM` and `liftM2` are not in\nscope. Another issue is that `System.Directory` can no longer be\nimported safely. These errors are causing the build to fail on hackage,\nwhich uses GHC 9.6.3.\n\n**Type**\n\n- Bug: Failure to compile with version of dependency.\n\n**Additional context**\n\n- https://github.com/haskell/directory/issues/147\n\n**Requester**\n\n- Ivan Perez\n\n**Method to check presence of bug**\n\nThe following Dockerfile checks whether Copilot can be installed with\nGHC 9.6, in which case it prints the message Success:\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\n\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 && 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=\" -it copilot-verify-491\n```\n\n**Expected result**\n\nCompiling with GHC 9.6 succeeds. Running the above image prints the\nmessage Success, indicating that Copilot can be compile with GHC 9.6.3.\n\n**Solution implemented**\n\nModify `copilot-theorem` to import `Control.Monad` explicitly, instead of via\nre-exports from other modules.\n\nModify the module that imports `System.Directory` so that it is marked\nas trustworthy instead of Safe.\n\n**Further notes**\n\nNone.","shortMessageHtmlLink":"Merge branch 'develop-ghc-9.6.3'. Close #491."}},{"before":"6d742f2e3503ebc91eab02be514ee6b920eff6f2","after":"a53f5320842276019fa2fe1c1dce863f6ff8b6e4","ref":"refs/heads/master","pushedAt":"2024-01-08T00:26:20.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Merge branch 'release-3.18'. Close #487.\n\n**Description**\n\nVersion 3.18 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.18\" \\\n --constraint=\"copilot-c99==3.18\" \\\n --constraint=\"copilot-core==3.18\" \\\n --constraint=\"copilot-prettyprinter==3.18\" \\\n --constraint=\"copilot-interpreter==3.18\" \\\n --constraint=\"copilot-language==3.18\" \\\n --constraint=\"copilot-libraries==3.18\" \\\n --constraint=\"copilot-theorem==3.18\" \\\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=\" -it copilot-verify-487\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'. Close #487."}},{"before":"ca738f7a57c3b8c5a08b4dae1baf2df343e57882","after":"6d742f2e3503ebc91eab02be514ee6b920eff6f2","ref":"refs/heads/master","pushedAt":"2024-01-07T23:22:54.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Merge branch 'develop-optparse-applicative-versions'. Close #488.\n\n**Description**\n\n`optparse-applicative` has seen a new release 0.18.1.0, but `copilot`\nneeds versions strictly lower than 1.8. This could prevent `copilot`\nfrom being installed in certain systems or with certain LTSs.\n\n**Type**\n\n- Management: update versions of dependencies.\n\n**Additional context**\n\nNone.\n\n**Requester**\n\n- Ivan Perez\n\n**Method to check presence of bug**\n\nThe following Dockerfile checks Copilot can be installed with\noptparse-applicative>=0.18, in which case it prints the message Success:\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.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.8\nRUN ghcup set ghc 9.4.8\nRUN cabal update\n\nCMD git clone $REPO \\\n && cd $NAME \\\n && git checkout $COMMIT \\\n && cabal install --lib copilot**/ \\\n --constraint=\"optparse-applicative>=0.18\" \\\n && echo Success\n```\n\nCommand (substitute variables based on new path after merge):\n```sh\n$ docker run -e \"REPO=https://github.com/copilot-language/copilot\" -e \"NAME=copilot\" -e \"COMMIT=\" copilot-verify-488\n```\n\n**Expected result**\n\nCopilot can be installed with `optparse-applicative>=0.18`.\n\n**Proposed solution**\n\nModify `copilot`'s cabal file to accept `optparse-applicative` versions\n`>= 0.18` and `<0.19`.\n\n**Further notes**\n\nNone.","shortMessageHtmlLink":"Merge branch 'develop-optparse-applicative-versions'. Close #488."}},{"before":"5ee005e223f6ea8a1eadcdbc9b1795da70ba8bdc","after":"ca738f7a57c3b8c5a08b4dae1baf2df343e57882","ref":"refs/heads/master","pushedAt":"2024-01-07T13:18:41.000Z","pushType":"push","commitsCount":7,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?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'. Close #472."}},{"before":"b9df52d964048a549d597926af8431a5f182aa6b","after":null,"ref":"refs/heads/develop-misra-2012","pushedAt":"2024-01-04T05:06:35.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"}},{"before":"437b647609d3d3665c1d5d3fa3bf407d38c9bcec","after":"5ee005e223f6ea8a1eadcdbc9b1795da70ba8bdc","ref":"refs/heads/master","pushedAt":"2023-12-29T11:55:56.000Z","pushType":"push","commitsCount":9,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?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=\" -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'. Close #470."}},{"before":"fbfbbd39d3795d861fe4df8f612faf19aca533b0","after":"437b647609d3d3665c1d5d3fa3bf407d38c9bcec","ref":"refs/heads/master","pushedAt":"2023-12-25T05:56:44.000Z","pushType":"push","commitsCount":5,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Merge branch 'develop-test-libraries'. Close #475.\n\n**Description**\n\nAs part of the requirements for Class D (NPR7150.2C), we need unit tests\nfor all of copilot.\n\nA natural next step is to introduce the testing infrastructure for\n`copilot-libraries`.\n\n**Type**\n\n- Management: conformance with new requirement.\n\n**Additional context**\n\nNone.\n\n**Requester**\n\n- Ivan Perez\n\n**Method to check presence of bug**\n\nThe following Dockerfile checks that copilot-libraries's tests can be\nexecuted, in which case it prints the message Success:\n\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 make libgmp3-dev g++\n\nSHELL [\"/bin/bash\", \"-c\"]\n\nRUN ghcup install ghc 9.4.7\nRUN ghcup install cabal 3.8\nRUN ghcup set ghc 9.4.7\nRUN cabal update\n\nRUN apt-get install --yes z3\n\nCMD git clone $REPO && \\\n cd $NAME && \\\n git checkout $COMMIT && \\\n cd copilot-libraries && \\\n cabal test copilot-libraries:unit-tests && \\\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=\" -it copilot-verify-475\n```\n\n**Expected result**\n\nThe library `copilot-libraries` includes tests for some of the existing\nmodules. Introducing (some classes of) errors in the implementation of\n`copilot-libraries` makes the tests detect those errors.\n\nRunning the docker file above prints the message success, indicating\nthat copilot-libraries now declares a unit-tests component.\n\n**Solution implemented**\n\nAdd tests for `copilot-libraries` that test a basic property in the\nmodule Copilot.Libraries.PTLTL. The property is tested using both\ncopilot-theorem and copilot-interpreter, showing how both interfaces can\nbe used.\n\n**Further notes**\n\nDue to the magnitude of this change, we decide to simplify the issue by\nmerely introducing the infrastructure. We leave it to a future issue to\ninclude a more comprehensive list of properties that covers all modules.","shortMessageHtmlLink":"Merge branch 'develop-test-libraries'. Close #475."}},{"before":"f0da035462065d19d7fff2e39dff8fcaefff009c","after":null,"ref":"refs/heads/develop-test-libraries","pushedAt":"2023-12-25T03:25:27.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"}},{"before":null,"after":"f0da035462065d19d7fff2e39dff8fcaefff009c","ref":"refs/heads/develop-test-libraries","pushedAt":"2023-12-25T03:24:21.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"copilot: Document changes in CHANGELOG. Refs #475.","shortMessageHtmlLink":"copilot: Document changes in CHANGELOG. Refs #475."}},{"before":"4620006d384decb417444f6f34470254b73b335f","after":"fbfbbd39d3795d861fe4df8f612faf19aca533b0","ref":"refs/heads/master","pushedAt":"2023-12-20T11:07:10.000Z","pushType":"push","commitsCount":5,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Merge branch 'develop-test-what4'. Close #474.\n\n**Description**\n\nAs part of the requirements for Class D (NPR7150.2C), we need unit tests\nfor all of copilot.\n\nA natural next step is to introduce the testing infrastructure for\n`copilot-theorem`.\n\n**Type**\n\n- Management: conformance with new requirement.\n\n**Additional context**\n\nNone.\n\n**Requester**\n\n- Ivan Perez\n\n**Method to check presence of bug**\n\nThe following Dockerfile checks that copilot-theorem's tests can be\nexecuted, in which case it prints 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 make libgmp3-dev g++\n\nSHELL [\"/bin/bash\", \"-c\"]\n\nRUN ghcup install ghc 9.4.7\nRUN ghcup install cabal 3.8\nRUN ghcup set ghc 9.4.7\nRUN cabal update\n\nRUN apt-get install --yes z3\n\nCMD git clone $REPO && \\\n cd $NAME && \\\n git checkout $COMMIT && \\\n cd copilot-theorem && \\\n cabal test copilot-theorem:unit-tests && \\\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=\" -it copilot-verify-474\n```\n\n**Expected result**\n\nThe library `copilot-theorem` includes tests for `what4`. Introducing\n(some classes of) errors in the implementation of `copilot-theorem`\nmakes the tests detect those errors.\n\nRunning the docker file above prints the message success, indicating\nthat copilot-theorem now declares a unit-tests component.\n\n**Proposed solution**\n\nAdd tests for `copilot-theorem` that test basic properties whose result\nis known with one of the existing solver.\n\nThe tests focus on What4, the Z3 solver, and only 3 properties. The goal\nis to introduce enough infrastructure that testing the What4 connection\nmore thoroughly should be reduced to adding more properties to the\nnow-existing test module.\n\n**Further notes**\n\nDue to the magnitude of this change, we decide to simplify the issue in\nthree ways:\n- Focus only on `what4`, which is likely going to replace other ways of\n connecting to SMT solvers provided by `copilot-theorem`.\n- Focus only on one of the SMT solvers.\n- Focus only on the core of the infrastructure, leaving it to a future\n issue to have a more comprehensive list of properties.","shortMessageHtmlLink":"Merge branch 'develop-test-what4'. Close #474."}},{"before":"907d5bbfcdfbda63da1cbc0631c5e927a706d719","after":"4620006d384decb417444f6f34470254b73b335f","ref":"refs/heads/master","pushedAt":"2023-12-20T04:10:11.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Merge branch 'develop-fix-trigger-arg-arrays'. Close #431.\n\n**Description**\n\nCopilot's C99 backend generates incorrect code. In the generated code,\nthe functions that generate values passed as arguments to trigger\nfunctions may return pointers to stack-allocated arrays, so the memory\nmay be used for something else (or freed).\n\nInstead, the structure of the implementation should guarantee that the\narrays are always allocated.\n\n**Type**\n\n- Bug: generated C code may be incorrect.\n\n**Additional context**\n\n- Bug #386 was initially opened for the same reason, but only addressed\n the `_gen` functions generated by Copilot. Other functions generated\n by Copilot also return pointers to arrays and can fail for the same\n reason.\n\n**Requester**\n\n- Ryan Scott (Galois)\n\n**Method to check presence of bug**\n\nThe following Dockerfile, and accompanying Copilot and C code, check\nthat passing a stream of arrays as an argument to a trigger, when\ncompiled with and without optimizations, produces the same results, in\nwhich case it prints the message Success. The docker image produces a\ndiff of the two outputs if not:\n\n```\n--- Dockerfile-verify-431\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 cabal v1-install alex happy\nRUN apt-get install --yes git\n\nADD Array.hs /tmp/Array.hs\nADD array_driver.c /tmp/array_driver.c\n\nSHELL [\"/bin/bash\", \"-c\"]\nCMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \\\n && cabal v1-install $NAME/copilot**/ \\\n && cabal v1-exec -- runhaskell /tmp/Array.hs \\\n && gcc -O0 /tmp/array_driver.c array.c -I. -o main-no-op && ./main-no-op > no-optimizations \\\n && gcc -O /tmp/array_driver.c array.c -I. -o main-op && ./main-op > with-optimizations \\\n && diff no-optimizations with-optimizations \\\n && echo \"Success\"\n\n--- Array.hs\n{-# LANGUAGE DataKinds #-}\nmodule Main where\n\nimport Copilot.Compile.C99\nimport Language.Copilot\nimport qualified Prelude as P\n\nspec :: Spec\nspec = trigger \"f\" true [arg stream]\n where\n stream :: Stream (Array 2 Int16)\n stream = constant (array [3,4])\n\nmain :: IO ()\nmain = reify spec >>= compile \"array\"\n\n--- array_driver.c\n#include \n#include \n\n#include \"array_types.h\"\n#include \"array.h\"\n\nvoid f (int16_t f_arg0[(2)]) {\n printf(\"([%d,%d])\\n\", f_arg0[0], f_arg0[1]);\n}\n\nint main(void) {\n int i = 0;\n\n printf(\"f:\\n\");\n\n for (i=0; i<5; i++) {\n step();\n }\n return 0;\n}\n```\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=\" -it copilot-verify-431\n```\n\n**Expected result**\n\nRunning the docker image above prints the message success, indicating\nthat the output structs produced with and without optimizations enabled\nare the same.\n\n**Solution implemented**\n\nModify generated C99 backend so that the output array in a function\nproducing values passed to triggers as arguments, as well as any they\ncall that also produces arrays, take the returned array as input. That\nway, all memory is preallocated and there's no need for mallocs either\n(which we want to avoid).\n\nIdentify factorization opportunity for different functions that call\ngenerators and pattern match based on the type of the expression being\ngenerated.\n\n**Further notes**\n\nNone.","shortMessageHtmlLink":"Merge branch 'develop-fix-trigger-arg-arrays'. Close #431."}},{"before":"60c44849980b881e84c2313c855954bccf8f10e9","after":"907d5bbfcdfbda63da1cbc0631c5e927a706d719","ref":"refs/heads/master","pushedAt":"2023-12-19T05:33:27.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Merge branch 'develop-test-integerSizes'. Close #471.\n\n**Description**\n\nThe code generated by `copilot-c99` during tests produces warnings\nduring compilation. The reason is that some constants included in the\ncode are too big and the compiler is making assumptions about their\nnecessary types. If those constants are annotated, their intention will\nbe made clearer.\n\n**Type**\n\n- Bug: test produce warnings during compilation.\n\n**Additional context**\n\nNone.\n\n**Requester**\n\n- Scott Talbert (Debian Developer & Debian Haskell Group)\n\n**Method to check presence of bug**\n\nCompiling `copilot-c99`'s tests can produce warnings:\n\n```\nmain.c:9:23: warning: integer constant is so large that it is unsigned\n 9 | uint64_t input_s[] = {10613134964919841005};\n | ^~~~~~~~~~~~~~~~~~~~\n```\n\n**Expected result**\n\nThe above tests should compile without warnings.\n\n**Solution implemented**\n\nModify the [`CShow` instances for different\ntypes](https://github.com/Copilot-Language/copilot/blob/cfc565bcf52dd359eb7ee768549459402c1785df/copilot-c99/tests/Test/Copilot/Compile/C99.hs#L884-L916)\nso that constants are printed with the necessary annotations.\n\nInstead of hard-coding the suffixes, which produces code that might not\nbe portable, we use macros defined in stdint.h to wrap the values. This\ncustomizes the suffixes for the architecture for which the C code\nproduced is being compiled.\n\n**Further notes**\n\n- Tests are randomly generated, so there's no guarantee that code with\n such warnings will be produced by a specific run. This issue is\ntherefore not always replicable unless we fix the number generator seed.\n\n- We have confirmed that the solution implemented works by asking the\n original user to check on their side that compilation now completes\n without those warnings.","shortMessageHtmlLink":"Merge branch 'develop-test-integerSizes'. Close #471."}},{"before":"7cb9a4e8c4cc74eb0cb4164885bd63b16284ea3d","after":"60c44849980b881e84c2313c855954bccf8f10e9","ref":"refs/heads/master","pushedAt":"2023-12-17T19:18:01.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Merge branch 'develop-language-test-typeError'. Close #469.\n\n**Description**\n\n`copilot-language`'s tests fail to compile with GHC 9.4. Prior versions\nsometimes made arbitrary decisions during type inference, whereas the\nnew type checker will simply reject such programs.\n\nFor example, compiling `copilot-language`'s tests with GHC 9.4.7 results\nin the following error message:\n\n```\nBuild profile: -w ghc-9.4.7 -O1\nIn order, the following will be built (use -v for more details):\n - copilot-language-3.17 (test:unit-tests) (first run)\nPreprocessing test suite 'unit-tests' for copilot-language-3.17..\nBuilding test suite 'unit-tests' for copilot-language-3.17..\n[2 of 3] Compiling Test.Copilot.Language.Reify ( tests/Test/Copilot/Language/Reify.hs, /root/copilot/dist-newstyle/build/x86_64-linux/ghc-9.4.7/copilot-language-3.17/t/unit-tests/build/unit-tests/unit-tests-tmp/Test/Copilot/Language/Reify.o )\n\ntests/Test/Copilot/Language/Reify.hs:737:16: error:\n * Could not deduce (Copilot.Core.Type.Struct t)\n arising from a superclass required to satisfy `Typed t',\n arising from a use of `observer'\n from the context: (Read t, Eq t, Typed t, Arbitrary t)\n bound by a pattern with constructor:\n SemanticsP :: forall t.\n (Typeable t, Read t, Eq t, Show t, Typed t, Arbitrary t) =>\n ((Typeable t, Read t, Eq t, Show t, Typed t, Arbitrary t) =>\n (Stream t, [t]))\n -> SemanticsP,\n in an equation for `checkSemanticsP'\n at tests/Test/Copilot/Language/Reify.hs:734:33-59\n Possible fix:\n add (Copilot.Core.Type.Struct t) to the context of\n the data constructor `SemanticsP'\n * In the expression: observer testObserverName expr\n In an equation for `spec': spec = observer testObserverName expr\n In the expression:\n do let spec = observer testObserverName expr\n llSpec <- reify spec\n let trace = eval Haskell steps llSpec\n let expectation = take steps exprList\n ....\n |\n737 | spec = observer testObserverName expr\n```\n\n**Type**\n\n- Bug: test fails to compile.\n\n**Additional context**\n\nNone.\n\n**Requester**\n\n- Scott Talbert (Debian Developer & Debian Haskell Group)\n\n**Method to check presence of bug**\n\nThe following Dockerfile checks that copilot-language compiles with GHC\n9.4, in which case it prints the message Success:\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.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 make libgmp3-dev g++\n\nSHELL [\"/bin/bash\", \"-c\"]\n\nRUN ghcup install ghc 9.4.7\nRUN ghcup install cabal 3.8\nRUN ghcup set ghc 9.4.7\nRUN cabal update\n\nCMD git clone $REPO && \\\n cd $NAME && \\\n git checkout $COMMIT && \\\n cd copilot-language && \\\n cabal test . && \\\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=\" -it copilot-verify-469\n```\n\n**Expected result**\n\nRunning the above docker image should print the message success,\nindicating that the tests can be compiled without errors (the image\nalso checks that they run successfully, although for this case we\nonly really care about the fact that it compiles).\n\n**Proposed solution**\n\nAdd type annotation to `spec` in `checkSemanticsP`, to help GHC's type\ninference engine.\n\nComment the change to make sure that future changes do not remove the\nsignature.\n\n**Further notes**\n\nNone.","shortMessageHtmlLink":"Merge branch 'develop-language-test-typeError'. Close #469."}},{"before":"cfc565bcf52dd359eb7ee768549459402c1785df","after":"7cb9a4e8c4cc74eb0cb4164885bd63b16284ea3d","ref":"refs/heads/master","pushedAt":"2023-12-17T16:36:42.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Merge branch 'develop-c99-testsMainType'. Close #468.\n\n**Description**\n\n`copilot-c99`'s tests fail on non-Intel architectures. The issue is that\nthe return code of the programs being generated (and executed) during\ntests are not zero, which the test interprets as a failure. More\nspecifically, the return type of the `main` function included in the\ngenerated C code is `void`, but should be `int`. By making it `int` and\nreturning `0`, the testing system will not interpret the test as a\nfailure.\n\n**Type**\n\n- Bug: test fails to run.\n\n**Additional context**\n\nNone.\n\n**Requester**\n\n- Scott Talbert (Debian Developer & Debian Haskell Group)\n\n**Method to check presence of bug**\n\nRunning `copilot-c99`' tests can lead to failures depending on the\narchitecture and compiler used, producing errors such as:\n\n```\nCopilot.Compile.C99:\n Compile specification: [OK, passed 1 tests]\n Compile specification in custom dir: [OK, passed 1 tests]\n Run specification: [Failed]\n*** Failed! Exception: 'callProcess: ./main (exit 64): failed' (after 1 test):\n```\n\nThis error manifests on non-Intel architectures, making it very hard to\nreproduce.\n\nFor what is worth, searching for void main in the search tree now brings\nup no results, while searching for int main brings up several results:\n\n```\n$ grep -nIHre 'void main'\n$ grep -nIHre 'int main'\ncopilot-c99/tests/Test/Copilot/Compile/C99.hs:160: , \"int main () {\"\ncopilot-c99/tests/Test/Copilot/Compile/C99.hs:696: , \"int main () {\"\n```\n\nThat, however, is a fairly weak check, since splitting the type and the\nfunction name would make the search pattern not succeed (which is common\nfor example with other coding standards like GNU's).\n\n**Expected result**\n\nThe above test should run without errors.\n\n**Solution implemented**\n\nModify the tests for `copilot-c99` so that the `main` has type `int`.\nChanging its type is enough to make it return `0` when reaching the end\nof the function.\n\n**Further notes**\n\nThe decision of what value to return upon program termination is\ndependent on the C standard, the compiler and architecture.\n\nISO C Standard (ISO/IEC 9899:1999) states in section \"5.1.2.2.3 Program\ntermination\":\n\n> If the return type of the main function is a type compatible with int\n> [...] reaching the } that terminates the main function returns a value\n> of 0. If the return type is not compatible with int, the termination\n> status returned to the host environment is unspecified.","shortMessageHtmlLink":"Merge branch 'develop-c99-testsMainType'. Close #468."}},{"before":null,"after":"aea0ae2ca6313789eddb7f6d81f576c5144ec12f","ref":"refs/heads/develop-ltl","pushedAt":"2023-12-07T22:00:55.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Future time LTL.\n\n[ci skip]","shortMessageHtmlLink":"Future time LTL."}},{"before":"11c2169ef95f49eac7daea5cc60e9bff271caeaa","after":null,"ref":"refs/heads/develop-demo","pushedAt":"2023-11-14T20:23:27.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"}},{"before":null,"after":"11c2169ef95f49eac7daea5cc60e9bff271caeaa","ref":"refs/heads/develop-demo","pushedAt":"2023-11-14T20:22:33.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"},"commit":{"message":"Array\n\n[ci skip]","shortMessageHtmlLink":"Array"}},{"before":"2839f73d85c87696cb1ef24ad41e65d7febd4567","after":null,"ref":"refs/heads/develop-demo","pushedAt":"2023-11-09T05:06:45.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?s=80&v=4"}},{"before":"e0a86dd2c70f124bb26005087a792c0153270b6b","after":"cfc565bcf52dd359eb7ee768549459402c1785df","ref":"refs/heads/master","pushedAt":"2023-11-08T00:28:25.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"ivanperez-keera","name":"Ivan Perez, PhD","path":"/ivanperez-keera","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1162320?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=\" -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'. Close #466."}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAERFkTLwA","startCursor":null,"endCursor":null}},"title":"Activity · Copilot-Language/copilot"}