{"action":"created","issue":{"url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/447","repository_url":"https://api.github.com/repos/mit-plv/fiat-crypto","labels_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/447/labels{/name}","comments_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/447/comments","events_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/447/events","html_url":"https://github.com/mit-plv/fiat-crypto/issues/447","id":366914525,"node_id":"MDU6SXNzdWUzNjY5MTQ1MjU=","number":447,"title":"merge-test-replace script to use instead of continuous integration","user":{"login":"andres-erbsen","id":918403,"node_id":"MDQ6VXNlcjkxODQwMw==","avatar_url":"https://avatars0.githubusercontent.com/u/918403?v=4","gravatar_id":"","url":"https://api.github.com/users/andres-erbsen","html_url":"https://github.com/andres-erbsen","followers_url":"https://api.github.com/users/andres-erbsen/followers","following_url":"https://api.github.com/users/andres-erbsen/following{/other_user}","gists_url":"https://api.github.com/users/andres-erbsen/gists{/gist_id}","starred_url":"https://api.github.com/users/andres-erbsen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andres-erbsen/subscriptions","organizations_url":"https://api.github.com/users/andres-erbsen/orgs","repos_url":"https://api.github.com/users/andres-erbsen/repos","events_url":"https://api.github.com/users/andres-erbsen/events{/privacy}","received_events_url":"https://api.github.com/users/andres-erbsen/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":{"login":"JasonGross","id":396076,"node_id":"MDQ6VXNlcjM5NjA3Ng==","avatar_url":"https://avatars0.githubusercontent.com/u/396076?v=4","gravatar_id":"","url":"https://api.github.com/users/JasonGross","html_url":"https://github.com/JasonGross","followers_url":"https://api.github.com/users/JasonGross/followers","following_url":"https://api.github.com/users/JasonGross/following{/other_user}","gists_url":"https://api.github.com/users/JasonGross/gists{/gist_id}","starred_url":"https://api.github.com/users/JasonGross/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JasonGross/subscriptions","organizations_url":"https://api.github.com/users/JasonGross/orgs","repos_url":"https://api.github.com/users/JasonGross/repos","events_url":"https://api.github.com/users/JasonGross/events{/privacy}","received_events_url":"https://api.github.com/users/JasonGross/received_events","type":"User","site_admin":false},"assignees":[{"login":"JasonGross","id":396076,"node_id":"MDQ6VXNlcjM5NjA3Ng==","avatar_url":"https://avatars0.githubusercontent.com/u/396076?v=4","gravatar_id":"","url":"https://api.github.com/users/JasonGross","html_url":"https://github.com/JasonGross","followers_url":"https://api.github.com/users/JasonGross/followers","following_url":"https://api.github.com/users/JasonGross/following{/other_user}","gists_url":"https://api.github.com/users/JasonGross/gists{/gist_id}","starred_url":"https://api.github.com/users/JasonGross/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JasonGross/subscriptions","organizations_url":"https://api.github.com/users/JasonGross/orgs","repos_url":"https://api.github.com/users/JasonGross/repos","events_url":"https://api.github.com/users/JasonGross/events{/privacy}","received_events_url":"https://api.github.com/users/JasonGross/received_events","type":"User","site_admin":false}],"milestone":null,"comments":3,"created_at":"2018-10-04T18:27:31Z","updated_at":"2018-10-11T20:51:21Z","closed_at":null,"author_association":"CONTRIBUTOR","body":"I think the flow should be roughly as follows:\r\n\r\n- [ ] script to make sure master is up to date, check out a new copy of master, merge a new branch into the copy of master\r\n- [x] remote async test runner: the script I wrote for running tests on CSAIL SLURM works for me: https://gist.github.com/andres-erbsen/9b0e79eb49acf382ecda479023abcd41\r\nIn particular, it survives network partitions, even in the case when tests finish during a network partition, and builds all of fiat-crypto with coq master, 8.9, and 8.8.\r\n- [ ] script to commit the merge, move put the merge commit on top of master, and push to github. Ideally it would always leave local master and remote master in a consistent state. **What should it do in case somebody else has updated master in the meantime?** As we currently test before merging, the most similar thing to do would be to just rebase/merge that commit if it can be done automatically. Of course this doesn't guarantee that master always builds.\r\n- [ ] glue these three scripts together\r\n\r\n- ( ) fix or drop build with coq 8.7 (coqdep being slow?)\r\n- ( ) local multi-version test runner: we should also probably make a local version of this script for those without access to MIT SLURM. The current script relies on SLURM infrastructure for limiting concurrency, so this is not totally trivial.\r\n- ( ) out-of-source build (nice-to-have): build with multiple coq versions without copying the source directory?\r\nCurrently 8"},"comment":{"url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/comments/429114028","html_url":"https://github.com/mit-plv/fiat-crypto/issues/447#issuecomment-429114028","issue_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/447","id":429114028,"node_id":"MDEyOklzc3VlQ29tbWVudDQyOTExNDAyOA==","user":{"login":"JasonGross","id":396076,"node_id":"MDQ6VXNlcjM5NjA3Ng==","avatar_url":"https://avatars0.githubusercontent.com/u/396076?v=4","gravatar_id":"","url":"https://api.github.com/users/JasonGross","html_url":"https://github.com/JasonGross","followers_url":"https://api.github.com/users/JasonGross/followers","following_url":"https://api.github.com/users/JasonGross/following{/other_user}","gists_url":"https://api.github.com/users/JasonGross/gists{/gist_id}","starred_url":"https://api.github.com/users/JasonGross/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JasonGross/subscriptions","organizations_url":"https://api.github.com/users/JasonGross/orgs","repos_url":"https://api.github.com/users/JasonGross/repos","events_url":"https://api.github.com/users/JasonGross/events{/privacy}","received_events_url":"https://api.github.com/users/JasonGross/received_events","type":"User","site_admin":false},"created_at":"2018-10-11T20:51:21Z","updated_at":"2018-10-11T20:51:21Z","author_association":"MEMBER","body":"My first sense: for each commit/branch that we do timing for, we pick a single version of Coq and a single machine (slurm?), and store in the merge commit the timing of the master build we're merging into, and the timing of the merged branch.  If we want, we can also store the table of the diff.  These files will basically be entirely rewritten on every merge commit created by this script."}}
{"actor":{"display_login":"JasonGross"}}