{"push_id":745392759,"size":24,"distinct_size":4,"ref":"refs/heads/extraction2","head":"1c6a3d62c081fdc88122afa35b1375d118e7e267","before":"1e8bbe83fbc2b8ae3613d097b1458fd846fe935f","commits":[{"sha":"8abf8894675e0e5654518858e73535b0361d7da1","author":{"email":"b82eecdfce19ef6c0125840b498d3afc6226dd31@cs.uni-saarland.de","name":"Niklas Grimm"},"message":"proving some relational properties for the spdz framework","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/8abf8894675e0e5654518858e73535b0361d7da1"},{"sha":"dddbdbcc1fe34d1860be2fc16a53a854cd1c7f25","author":{"email":"b82eecdfce19ef6c0125840b498d3afc6226dd31@cs.uni-saarland.de","name":"Niklas Grimm"},"message":"Code for #290","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/dddbdbcc1fe34d1860be2fc16a53a854cd1c7f25"},{"sha":"c43e495c5e23f1318e6a23b5d38b75d75147366f","author":{"email":"d4406ad8ea8c39bb970f4926611869ef609e7113@users.noreply.github.com","name":"Nikhil Swamy"},"message":"Merge branch 'extraction2'","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/c43e495c5e23f1318e6a23b5d38b75d75147366f"},{"sha":"4e4162f736195b2031ba221b1f354216218cd397","author":{"email":"d4406ad8ea8c39bb970f4926611869ef609e7113@users.noreply.github.com","name":"Nikhil Swamy"},"message":"removing old generated files","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/4e4162f736195b2031ba221b1f354216218cd397"},{"sha":"9e272b96d806183fc45f21b0add516e1dac2db3d","author":{"email":"b82eecdfce19ef6c0125840b498d3afc6226dd31@cs.uni-saarland.de","name":"Niklas Grimm"},"message":"Code for #291","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/9e272b96d806183fc45f21b0add516e1dac2db3d"},{"sha":"95ed9018d8a138add05de29a4ff591c92d327210","author":{"email":"0749e5dd25babf08d5bfafc2069ecdd31e4f5458@gmail.com","name":"jkz"},"message":"fixed bugs in bigint code","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/95ed9018d8a138add05de29a4ff591c92d327210"},{"sha":"72b83f8567f4987e113bcf9541ac26a39520e086","author":{"email":"3623de16a2d847203d0b13f4c029365b5cd13403@microsoft.com","name":"Abhishek Anand (on VAIO laptop)"},"message":"Merge branch 'extraction2'","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/72b83f8567f4987e113bcf9541ac26a39520e086"},{"sha":"b6e81c1f5426da77e318dfc040a2277a80d43fbd","author":{"email":"ac6a81074837c53f281f322691d9a34fc7b68e28@cs.umd.edu","name":"Michael Hicks"},"message":"Added support for stack-allocated references. Marked them as possible\nroots, conservatively.","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/b6e81c1f5426da77e318dfc040a2277a80d43fbd"},{"sha":"4f1753e6eaa2c158a84364dd86b6965404bdcc34","author":{"email":"ac6a81074837c53f281f322691d9a34fc7b68e28@cs.umd.edu","name":"Michael Hicks"},"message":"Merge branch 'master' of github.com:FStarLang/FStar","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/4f1753e6eaa2c158a84364dd86b6965404bdcc34"},{"sha":"fe51c824e1c450037f1c63a1904206f704b151ac","author":{"email":"3623de16a2d847203d0b13f4c029365b5cd13403@microsoft.com","name":"Abhishek Anand (@ MSR desktop)"},"message":"removed ticks when tyVars are retained in ML as termVars.\n\nThis change seems to preserve passing all tests, and hence can be merged to master:\n\nError: 35 errors were reported (see above)\nSuccess: 35 failures were expected\nmake[2]: Leaving directory '/home/t-aban/FStar/examples/unit-tests'\nmake[1]: Leaving directory '/home/t-aban/FStar/examples'","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/fe51c824e1c450037f1c63a1904206f704b151ac"},{"sha":"e22ce6063db1dcb31c9aa029d0713b0621734477","author":{"email":"3623de16a2d847203d0b13f4c029365b5cd13403@microsoft.com","name":"Abhishek Anand (@ MSR desktop)"},"message":"added the extract of sstCombinators.fst.\nThere are 2 unnecessary magics, possibly due to the same issue, perhaps related to extraction of metas.\nWill manually remove those magics.","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/e22ce6063db1dcb31c9aa029d0713b0621734477"},{"sha":"1c131935f52ad5daad01ff7dfa796b0da17d0a37","author":{"email":"3623de16a2d847203d0b13f4c029365b5cd13403@microsoft.com","name":"Abhishek Anand (@ MSR desktop)"},"message":"added the extract of SST and factorial.\nThere are some unnececcary magics in Factorial.ml . Many magics are necessary, because of how the non-OCaml inductive type aref gets extracted.\nUp Next : will try to provide a simple implementation of undefined functions in SST.ml, and try to run the factorial program.","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/1c131935f52ad5daad01ff7dfa796b0da17d0a37"},{"sha":"31401fa02a12a1a3380ebac48d04400206e50acc","author":{"email":"3623de16a2d847203d0b13f4c029365b5cd13403@microsoft.com","name":"Abhishek Anand (@ MSR desktop)"},"message":"simple implementation of SST.\ntried to run factorial (in Test.ml).\nIt fails with a \"not yet implemented\" exception.\nextraction will now include names of the unimplemented lidents in such messages.","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/31401fa02a12a1a3380ebac48d04400206e50acc"},{"sha":"9e3a05108478fda7539167c76b045bfae9c168d2","author":{"email":"3623de16a2d847203d0b13f4c029365b5cd13403@microsoft.com","name":"Abhishek Anand (@ MSR desktop)"},"message":"manually provided an implementation of Heap.emp\nThe factorial program then runs:\n\n./program\n6","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/9e3a05108478fda7539167c76b045bfae9c168d2"},{"sha":"5083b7350ee60720b7c1ce9bff70c3f0810be58d","author":{"email":"3623de16a2d847203d0b13f4c029365b5cd13403@microsoft.com","name":"Abhishek Anand (@ MSR desktop)"},"message":"Merge branch 'master' into extraction2","distinct":true,"url":"https://api.github.com/repos/FStarLang/FStar/commits/5083b7350ee60720b7c1ce9bff70c3f0810be58d"},{"sha":"dc17cf0786fbd73d0f2d2f27cecc9e7c71405f13","author":{"email":"ac6a81074837c53f281f322691d9a34fc7b68e28@cs.umd.edu","name":"Michael Hicks"},"message":"Added support for stack-allocated arrays.","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/dc17cf0786fbd73d0f2d2f27cecc9e7c71405f13"},{"sha":"d755cfdd58388459cf765cd605c0eb210dae129f","author":{"email":"ac6a81074837c53f281f322691d9a34fc7b68e28@cs.umd.edu","name":"Michael Hicks"},"message":"Missing file.","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/d755cfdd58388459cf765cd605c0eb210dae129f"},{"sha":"8c61f665475dd39a388d717f873b40d0f5ab6b01","author":{"email":"3623de16a2d847203d0b13f4c029365b5cd13403@microsoft.com","name":"Abhishek Anand (@ MSR desktop)"},"message":"added ghost.fst to all build configs.\nadded test cases for ghostness","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/8c61f665475dd39a388d717f873b40d0f5ab6b01"},{"sha":"d77dd6aced8f12ffb9f10e04954ffe5a211b0af6","author":{"email":"3623de16a2d847203d0b13f4c029365b5cd13403@microsoft.com","name":"Abhishek Anand (@ MSR desktop)"},"message":"checked eraseability before inserting magic.\nOtherwise, the change of type caused by erasure caused unnecessary magics.\nUp next : delta unfolding which deciding eraseability","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/d77dd6aced8f12ffb9f10e04954ffe5a211b0af6"},{"sha":"bd48dc77f8e725cf9aa68a2d1722e8e7e928f8f8","author":{"email":"3623de16a2d847203d0b13f4c029365b5cd13403@microsoft.com","name":"Abhishek Anand (@ MSR desktop)"},"message":"delta unfolding in checking erasability","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/bd48dc77f8e725cf9aa68a2d1722e8e7e928f8f8"}]}