{"push_id":1323404191,"size":465,"distinct_size":465,"ref":"refs/heads/master","head":"c6c399da56d6f31f4cab8cf33cef123c1d2eec32","before":"6cbfdd32de26166262c7537137d61551cb40a4ef","commits":[{"sha":"8b152bbbb798ebea319614772f6ada9e7d460a41","author":{"name":"Jan de Muijnck-Hughes","email":"b12f6d4f6f80d7d34658089661e60ffcdb5bab59@st-andrews.ac.uk"},"message":"Updated formatting for Directives.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/8b152bbbb798ebea319614772f6ada9e7d460a41"},{"sha":"c2b01ccf5d8e4070000fe665200e7b7d902970a4","author":{"name":"Edwin Brady","email":"c928bc23af0546b9627da03f5800c450bd33bde7@st-andrews.ac.uk"},"message":"mkUniqueName fix\n\nMake user's names unique earlier (to save difficulty in alternative\nresolution, which is postponed). Also need to ensure names get added to\nthe map in the right order for when resolving ambiguous names in\nalternatives.\n\nFixes #3116","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/c2b01ccf5d8e4070000fe665200e7b7d902970a4"},{"sha":"c56d5cf2934e94e18ace3a2f90d707c0b0c0b710","author":{"name":"Jan de Muijnck-Hughes","email":"b12f6d4f6f80d7d34658089661e60ffcdb5bab59@st-andrews.ac.uk"},"message":"Addition of a Fragile directive.\n\nWhen building packages new features may be added for testing. The\n`fragile` directive provides support for marking such fragile\nconstructs and providing compilation warnings.\n\nThis commit also adds a directives test to check the operation of the\ndeprecate and fragile directives.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/c56d5cf2934e94e18ace3a2f90d707c0b0c0b710"},{"sha":"6b64e74d663c4561942869524a962c078d2a092d","author":{"name":"Jan de Muijnck-Hughes","email":"b12f6d4f6f80d7d34658089661e60ffcdb5bab59@st-andrews.ac.uk"},"message":"Fixed formatting of directives adt.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/6b64e74d663c4561942869524a962c078d2a092d"},{"sha":"59942da82a660d8d1abe5c859f4a89076cb4f7ed","author":{"name":"Edwin Brady","email":"c928bc23af0546b9627da03f5800c450bd33bde7@st-andrews.ac.uk"},"message":"Look deeper in pruneByType\n\nOtherwise, we might commit to something where it's clear from looking\ndeeper that the alternative can't possible work.\n\nFixes #2830","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/59942da82a660d8d1abe5c859f4a89076cb4f7ed"},{"sha":"951b631681cca4c2c7f22b0441a003c79fed03fa","author":{"name":"Edwin Brady","email":"c928bc23af0546b9627da03f5800c450bd33bde7@st-andrews.ac.uk"},"message":"Constraint insertion on implicits\n\nNo need to treat implicits specially, because deciding the ordering can\nbe tricky - let the elaborator do its job instead!\n\nFixes #2505","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/951b631681cca4c2c7f22b0441a003c79fed03fa"},{"sha":"1df4d970902c8aa338461a714db22f59d79385df","author":{"name":"Edwin Brady","email":"c928bc23af0546b9627da03f5800c450bd33bde7@st-andrews.ac.uk"},"message":"Tweak alternative pruning\n\nDon't remove overloadings where there's a blocked function name in the\ntype, because further information may reveal it's a valid overloading.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/1df4d970902c8aa338461a714db22f59d79385df"},{"sha":"7688c8d4747066017cf76d41f588c6582c0b910c","author":{"name":"Edwin Brady","email":"c928bc23af0546b9627da03f5800c450bd33bde7@st-andrews.ac.uk"},"message":"Better DecEq implementations on primitives\n\nMake sure they block completely hen inputs are unknown, otherwise the\nproofs which get generated are not going to typecheck if they turn up\nunder some evaluation","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/7688c8d4747066017cf76d41f588c6582c0b910c"},{"sha":"d662e2652dfad40f59bae603499a56ea4382d627","author":{"name":"Edwin Brady","email":"c928bc23af0546b9627da03f5800c450bd33bde7@st-andrews.ac.uk"},"message":"Lazy elaboration tweaks\n\nFirstly, never add a Delay to a pattern variable on the lhs, since\nevaluation isn't forced until it is deconstructed.\nSecondly, \"try\" is supposed to return the first error if there's a\nfailure, but this wasn't happening in some cases. In particular, this\ncan make errors from Lazy elaboration surprising, so this is fixed.\n\nFixes #3105","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/d662e2652dfad40f59bae603499a56ea4382d627"},{"sha":"7e7d0eb19b03b05cd80cf9df31f7f176611d87ed","author":{"name":"Edwin Brady","email":"c928bc23af0546b9627da03f5800c450bd33bde7@st-andrews.ac.uk"},"message":"Elaboration of local applications\n\nExpand application of local variables to all of their arguments in one\ngo, where their type is known. This is better for type-directed\ndisambiguation, and for reporting errors more accurately.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/7e7d0eb19b03b05cd80cf9df31f7f176611d87ed"},{"sha":"ed171dbde70afef5b80c15bccec8e362eb4bc15b","author":{"name":"Niklas Larsson","email":"407b5ecd7b3f53bb1cca7f5fca9c7d6c46ab5b13@mm.st"},"message":"Fix alignment on 32 bits\n\nQwords and doubles are 8 byte aligned and not 4.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/ed171dbde70afef5b80c15bccec8e362eb4bc15b"},{"sha":"cf0b54e268681115aca1389ff18e73196193ff37","author":{"name":"Niklas Larsson","email":"f00ad0a60710e0eb5b699b4c9fdbf02e147c6c43@gmail.com"},"message":"Merge pull request #3121 from melted/align_32bit\n\nFix alignment on 32 bits","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/cf0b54e268681115aca1389ff18e73196193ff37"},{"sha":"5984b2ff0e16c2779d334dffe786b3da91f4c994","author":{"name":"Edwin Brady","email":"c928bc23af0546b9627da03f5800c450bd33bde7@st-andrews.ac.uk"},"message":"Don't use top level elab for resolveTC\n\nOtherwise it'll attempt to resolve ambiguities and the elaborator could\nthink there's an interface resolution failure, when actually it's just\nan ambiguity that hasn't been resolved yet.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/5984b2ff0e16c2779d334dffe786b3da91f4c994"},{"sha":"3ce13cbf430d1a6ad792d22a69c6533e8b9efba9","author":{"name":"Leif Warner","email":"9684e5f07603b76ee20d9e1bb79de586e05b998e@gmail.com"},"message":"Cleanup main warnings (#3123)\n\n* Cleanup all -Wall warnings on Main\r\n\r\n(mostly unused imports)\r\n\r\n* Collapse two BSD ifdefs into one.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/3ce13cbf430d1a6ad792d22a69c6533e8b9efba9"},{"sha":"0dec4a1a99ccf2a6770995a444dfbf731e21d686","author":{"name":"Edwin Brady","email":"c928bc23af0546b9627da03f5800c450bd33bde7@st-andrews.ac.uk"},"message":"Fix name substitution in with functions\n\nThis didn't pay proper attention to shadowing (because it was\nsubstituting things one at a time, instead of all at once) so it's quite\nsurprising nobody has noticed before...","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/0dec4a1a99ccf2a6770995a444dfbf731e21d686"},{"sha":"b57da9db3c61c81fcd8a6244734e1d416c75b7d6","author":{"name":"Edwin Brady","email":"c928bc23af0546b9627da03f5800c450bd33bde7@st-andrews.ac.uk"},"message":"Pattern matching lambda fix\n\nIt's only a pattern matching lambda if it binds a constructor name. We\ndon't want to introduce 'case' unnecessarily since it is restricted in\nthe type inference it can do, so only do that if it really is binding a\nconstructor name.\n\nFixes #2150","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/b57da9db3c61c81fcd8a6244734e1d416c75b7d6"},{"sha":"c931e38419f67dd4134f6b7d69ff30274b790660","author":{"name":"Edwin Brady","email":"c928bc23af0546b9627da03f5800c450bd33bde7@st-andrews.ac.uk"},"message":"Use exact lookup in size-change checking\n\nWe should always use exact name lookup after ambiguities are resolved.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/c931e38419f67dd4134f6b7d69ff30274b790660"},{"sha":"1d0e33c8738fdf551491c1495161003c64bfa6ca","author":{"name":"Edwin Brady","email":"c928bc23af0546b9627da03f5800c450bd33bde7@st-andrews.ac.uk"},"message":"Remove a \"can't happen\" error\n\nThis one can happen if there's been an error previously, but we still\nwant to make a bit of progress on coverage checking.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/1d0e33c8738fdf551491c1495161003c64bfa6ca"},{"sha":"7c5819b55de9233039d9f3fdba7ebf0631a64236","author":{"name":"Edwin Brady","email":"c928bc23af0546b9627da03f5800c450bd33bde7@st-andrews.ac.uk"},"message":"Add Data.Vect.Views\n\nWith SnocVect, Split and SplitRec, also added to views001 test","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/7c5819b55de9233039d9f3fdba7ebf0631a64236"},{"sha":"ea0966e72ae1d0c82e81b719afb03a286fecd69b","author":{"name":"Saurabh Rawat","email":"44611cea0f7fbc21b32759c87a96ca861732ec35@users.noreply.github.com"},"message":"Fix string to positive number conversion (#3129)\n\nCurrently \"-123\" is being parsed as Just 0 for Nats, which is wrong. It should return Nothing for non numbers and negative numbers.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/ea0966e72ae1d0c82e81b719afb03a286fecd69b"}]}
{"actor":{"display_login":"justjoheinz"}}