{"push_id":2807474244,"size":584,"distinct_size":2,"ref":"refs/heads/cf-div","head":"360a5929382809854e12d2142a9c8dda71daf17e","before":"a660edc1fa32b58a3668ac93502b947482f709c8","commits":[{"sha":"2b1a222a4783d88b526451150411121a81691fe1","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Experiment on not duplicate type checking in semantics\n\nStart by removing the checks from modSem. Everything seems to work,\nexcept for a lemma about constructor exhuastiveness information.","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/2b1a222a4783d88b526451150411121a81691fe1"},{"sha":"85f2545442c3fd7d8e330062b105e60e56b6bfd8","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Merge remote-tracking branch 'origin/master' into dup_typenames","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/85f2545442c3fd7d8e330062b105e60e56b6bfd8"},{"sha":"b2c7e865acba9fc3f8e48c5c79ba258d8b8abe65","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Merge remote-tracking branch 'origin/master' into dup_typenames","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/b2c7e865acba9fc3f8e48c5c79ba258d8b8abe65"},{"sha":"5c45355935c81527bfe957fe0d590dab40c069ba","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Add a flag to modSem to enforce exhaustive patterns\n\nIn preparation to remove exhLang and make exhaustiveness checking (and\ncompletion) a modLang to modLang pass. This will remove an awkward\ntop-level mapping (which recorded which constructors each type had) that\nmod-to-con used to build to communicate with dec-to-exh, once the type\ndeclarations were removed from the program.","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/5c45355935c81527bfe957fe0d590dab40c069ba"},{"sha":"82d0d6d89bf6f6b8e3eaae60cb71946119b077b4","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Merge remote-tracking branch 'origin/master' into exh_move","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/82d0d6d89bf6f6b8e3eaae60cb71946119b077b4"},{"sha":"e3877f2dc2290b5c9e865de390bf0ba56ee8280f","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Update the opsem to generate stamps for typedefs","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/e3877f2dc2290b5c9e865de390bf0ba56ee8280f"},{"sha":"dbbaba9c2d2fb57a2586768fa060b4b864d926c4","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"WIP on updating for non-unique type names","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/dbbaba9c2d2fb57a2586768fa060b4b864d926c4"},{"sha":"4f67080c873ab8dd46d22c90af8928d2060ad032","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Merge remote-tracking branch 'origin/master' into type-stamps","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/4f67080c873ab8dd46d22c90af8928d2060ad032"},{"sha":"afdbb219c5e1e58b4f59d8998196c610f6813954","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"First pass throught the semantics for nested modules\n\nAnd more work on stamp based type identities","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/afdbb219c5e1e58b4f59d8998196c610f6813954"},{"sha":"a0e58c9531bb3ffc2d3ba3762f85dda8624b1d49","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Comment out cmlPtreeConversionScript\n\nIt doesn't build for mysterious reasons.","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/a0e58c9531bb3ffc2d3ba3762f85dda8624b1d49"},{"sha":"93bc2da42b9989f6df3104df1a8fbfe9a870b70f","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Update top-level semantics\n\nComment out parsing stuff pending cmlPtreeConversion fixes","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/93bc2da42b9989f6df3104df1a8fbfe9a870b70f"},{"sha":"6c403b2e9ec7fa315210605986a9c0a21ade4b63","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Fix termination proof","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/6c403b2e9ec7fa315210605986a9c0a21ade4b63"},{"sha":"a68869af4042732d910e13d490e369f0f7b419e4","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Update type soundness invariants","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/a68869af4042732d910e13d490e369f0f7b419e4"},{"sha":"32ba8bb180bc3a32a902060bde31aaefbe87d5f8","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Fix type system and proofs up through weakening","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/32ba8bb180bc3a32a902060bde31aaefbe87d5f8"},{"sha":"d3cbd477487253a2832abe2868ad88601012a0d6","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Work on type soundness proof","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/d3cbd477487253a2832abe2868ad88601012a0d6"},{"sha":"d9d14e01d53a024823cac6666d2702ba1df72f3e","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Rework the canonical values theorem\n\nNow that the details of constructors and theor stamps/types are\ndifferent. Not finished with the proof yet.","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/d9d14e01d53a024823cac6666d2702ba1df72f3e"},{"sha":"f2afd4f123e78b201659808068d94d6dd1bf78f5","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Prove type soundess for primitive ops\n\nReworked the proof to simplify a bit by strengthening the canonical\nvalues lemmas","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/f2afd4f123e78b201659808068d94d6dd1bf78f5"},{"sha":"fae810c340f97d33f6e272eed056f00d14d750d4","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Merge remote-tracking branch 'origin/master' into type+module-update","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/fae810c340f97d33f6e272eed056f00d14d750d4"},{"sha":"4a727aa0bd3a5f5767219cd582dd2b0e3f41e951","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Tweak","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/4a727aa0bd3a5f5767219cd582dd2b0e3f41e951"},{"sha":"8d6f6290ea5f8e455c41e06be404be9fe85e169e","author":{"name":"Scott Owens","email":"28ee6d13aeff9b83dad27063b8ac6102494e7457@kent.ac.uk"},"message":"Fix expression type soundness\n\nPattern matchint type soundness cheated for now","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/8d6f6290ea5f8e455c41e06be404be9fe85e169e"}]}
{"actor":{"display_login":"fogity"}}