Circle CI Pro license tracker

[alexpatel]

• met with Wendy@CircleCI on Friday, she will try and flip the image caching flag and also to get us started on a Pro CircleCI license to try out.
• meeting with her again on Tuesday or Wednesday to get the Pro license turned on

I'll update when we find a time here - please feel free to join me for that conversation if you'd like to hear their official PRINCESS "sales pitch" :) (and chime in on the e-mail chain I CC'ed to the group mailing list if the time we choose doesn't work for you).

[mwookawa]

Let's find a time to chat before talking to her again. Is this pro license a permanent donation or a trial?

Also, i want to make it clear to them that we are not going to attempt to use circleci as a model checker. They are competing with a local jenkins install, not an RC spin batch job. On Mon, Jul 31, 2017 at 8:06 AM Alex Patel notifications@github.com wrote:

• met with Wendy@CircleCI on Friday, she will try and flip the image caching flag and also to get us started on a Pro CircleCI license to try out.
• meeting with her again on Tuesday or Wednesday to get the Pro license turned on

I'll update when we find a time here - please feel free to join me for that conversation if you'd like to hear their official PRINCESS "sales pitch" :) (and chime in on the e-mail chain I CC'ed to the group mailing list if the time we choose doesn't work for you).

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/Harvard-PRINCESS/Guppy/issues/95, or mute the thread https://github.com/notifications/unsubscribe-auth/ABceTMyv935UJuYrSOddcTL9OejMeWb_ks5sTcNJgaJpZM4OoSXI .

[alexpatel]

Let's find a time to chat before talking to her again. Is this pro license a permanent donation or a trial?

It was a little ambiguous when I spoke with her, but I definitely made it clear that we were not looking to pay for a professional license because of funding constraints. Hopefully, they will take this into consideration for the plan they put together

Also, i want to make it clear to them that we are not going to attempt

touse circleci as a model checker. They are competing with a local jenkins install, not an RC spin batch job..

Okay, cool, so we would just want it purely to run tests against our manual code (e.g. Alewife development), and not the synthesized OSes we create?

Can you elaborate on what is an RC spin batch job?

Alex

On Mon, Jul 31, 2017 at 8:12 AM, Ming Kawaguchi notifications@github.com wrote:

Let's find a time to chat before talking to her again. Is this pro license a permanent donation or a trial?

Also, i want to make it clear to them that we are not going to attempt to use circleci as a model checker. They are competing with a local jenkins install, not an RC spin batch job. On Mon, Jul 31, 2017 at 8:06 AM Alex Patel notifications@github.com wrote:

• met with Wendy@CircleCI on Friday, she will try and flip the image caching flag and also to get us started on a Pro CircleCI license to try out.
• meeting with her again on Tuesday or Wednesday to get the Pro license turned on

I'll update when we find a time here - please feel free to join me for that conversation if you'd like to hear their official PRINCESS "sales pitch" :) (and chime in on the e-mail chain I CC'ed to the group mailing list if the time we choose doesn't work for you).

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/Harvard-PRINCESS/Guppy/issues/95, or mute the thread https://github.com/notifications/unsubscribe-auth/ ABceTMyv935UJuYrSOddcTL9OejMeWb_ks5sTcNJgaJpZM4OoSXI .

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/Harvard-PRINCESS/Guppy/issues/95#issuecomment-319049678, or mute the thread https://github.com/notifications/unsubscribe-auth/AEqvaLeHK8CBo1nb9bRBXOlFD08_XVuHks5sTcSZgaJpZM4OoSXI .

-- Alexander H. Patel Harvard College, Class of 2017 alexanderpatel@college.harvard.edu (720) 320-1185

[mwookawa]

http://spinroot.com/spin/whatispin.html

In a sketching model, a candidate is certified by a bounded model checker. Spin is the grandaddy of all model checkers and highly parallelizable. For this sketching experiment, it is much more appropriate to figure out how to offload high compute onto the research cluster than to beg a startup for a huge amount of compute that isn't in their wheelhouse at all.

Note: i am still going to beg the startup for free services. It is kind of what i do ;) On Mon, Jul 31, 2017 at 8:17 AM Alex Patel notifications@github.com wrote:

Let's find a time to chat before talking to her again. Is this pro license a permanent donation or a trial?

It was a little ambiguous when I spoke with her, but I definitely made it clear that we were not looking to pay for a professional license because of funding constraints. Hopefully, they will take this into consideration for the plan they put together

Also, i want to make it clear to them that we are not going to attempt

touse circleci as a model checker. They are competing with a local jenkins install, not an RC spin batch job..

Okay, cool, so we would just want it purely to run tests against our manual code (e.g. Alewife development), and not the synthesized OSes we create?

Can you elaborate on what is an RC spin batch job?

Alex

On Mon, Jul 31, 2017 at 8:12 AM, Ming Kawaguchi notifications@github.com wrote:

Let's find a time to chat before talking to her again. Is this pro license a permanent donation or a trial?

Also, i want to make it clear to them that we are not going to attempt to use circleci as a model checker. They are competing with a local jenkins install, not an RC spin batch job. On Mon, Jul 31, 2017 at 8:06 AM Alex Patel notifications@github.com wrote:

• met with Wendy@CircleCI on Friday, she will try and flip the image caching flag and also to get us started on a Pro CircleCI license to try out.
• meeting with her again on Tuesday or Wednesday to get the Pro license turned on

I'll update when we find a time here - please feel free to join me for that conversation if you'd like to hear their official PRINCESS "sales pitch" :) (and chime in on the e-mail chain I CC'ed to the group mailing list if the time we choose doesn't work for you).

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/Harvard-PRINCESS/Guppy/issues/95, or mute the thread https://github.com/notifications/unsubscribe-auth/ ABceTMyv935UJuYrSOddcTL9OejMeWb_ks5sTcNJgaJpZM4OoSXI .

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub < https://github.com/Harvard-PRINCESS/Guppy/issues/95#issuecomment-319049678 , or mute the thread < https://github.com/notifications/unsubscribe-auth/AEqvaLeHK8CBo1nb9bRBXOlFD08_XVuHks5sTcSZgaJpZM4OoSXI

.

-- Alexander H. Patel Harvard College, Class of 2017 alexanderpatel@college.harvard.edu (720) 320-1185

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/Harvard-PRINCESS/Guppy/issues/95#issuecomment-319050736, or mute the thread https://github.com/notifications/unsubscribe-auth/ABceTAH0qA8cOu32ddL5sAsE0x7bx2bQks5sTcXPgaJpZM4OoSXI .

[alexpatel]

Okay, sounds good.

On Mon, Jul 31, 2017 at 8:25 AM, Ming Kawaguchi notifications@github.com wrote:

http://spinroot.com/spin/whatispin.html

In a sketching model, a candidate is certified by a bounded model checker. Spin is the grandaddy of all model checkers and highly parallelizable. For this sketching experiment, it is much more appropriate to figure out how to offload high compute onto the research cluster than to beg a startup for a huge amount of compute that isn't in their wheelhouse at all.

Note: i am still going to beg the startup for free services. It is kind of what i do ;)

On Mon, Jul 31, 2017 at 8:17 AM Alex Patel notifications@github.com wrote:

Let's find a time to chat before talking to her again. Is this pro license a permanent donation or a trial?

It was a little ambiguous when I spoke with her, but I definitely made it clear that we were not looking to pay for a professional license because of funding constraints. Hopefully, they will take this into consideration for the plan they put together

Also, i want to make it clear to them that we are not going to attempt

touse circleci as a model checker. They are competing with a local jenkins install, not an RC spin batch job..

Okay, cool, so we would just want it purely to run tests against our manual code (e.g. Alewife development), and not the synthesized OSes we create?

Can you elaborate on what is an RC spin batch job?

Alex

On Mon, Jul 31, 2017 at 8:12 AM, Ming Kawaguchi < notifications@github.com> wrote:

Let's find a time to chat before talking to her again. Is this pro license a permanent donation or a trial?

Also, i want to make it clear to them that we are not going to attempt to use circleci as a model checker. They are competing with a local jenkins install, not an RC spin batch job. On Mon, Jul 31, 2017 at 8:06 AM Alex Patel notifications@github.com wrote:

• met with Wendy@CircleCI on Friday, she will try and flip the image caching flag and also to get us started on a Pro CircleCI license to try out.
• meeting with her again on Tuesday or Wednesday to get the Pro license turned on

I'll update when we find a time here - please feel free to join me for that conversation if you'd like to hear their official PRINCESS "sales pitch" :) (and chime in on the e-mail chain I CC'ed to the group mailing list if the time we choose doesn't work for you).

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/Harvard-PRINCESS/Guppy/issues/95, or mute the thread https://github.com/notifications/unsubscribe-auth/ ABceTMyv935UJuYrSOddcTL9OejMeWb_ks5sTcNJgaJpZM4OoSXI .

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub < https://github.com/Harvard-PRINCESS/Guppy/issues/95# issuecomment-319049678 , or mute the thread < https://github.com/notifications/unsubscribe-auth/ AEqvaLeHK8CBo1nb9bRBXOlFD08_XVuHks5sTcSZgaJpZM4OoSXI

.

-- Alexander H. Patel Harvard College, Class of 2017 alexanderpatel@college.harvard.edu (720) 320-1185

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/Harvard-PRINCESS/Guppy/issues/95# issuecomment-319050736, or mute the thread https://github.com/notifications/unsubscribe-auth/ ABceTAH0qA8cOu32ddL5sAsE0x7bx2bQks5sTcXPgaJpZM4OoSXI

.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/Harvard-PRINCESS/Guppy/issues/95#issuecomment-319052377, or mute the thread https://github.com/notifications/unsubscribe-auth/AEqvaA_oyZG0T2Xlk_ICCxkyWX9SHTWEks5sTcergaJpZM4OoSXI .

-- Alexander H. Patel Harvard College, Class of 2017 alexanderpatel@college.harvard.edu (720) 320-1185

[ghost]

Also, i want to make it clear to them that we are not going to attempt to use circleci as a model checker. They are competing with a local jenkins install, not an RC spin batch job.

Also if we try to push every candidate synthesis to github on its own branch it will probably not explode github but will almost certainly explode the UI.

[alexpatel]

Yes - it may even explode github - I'll drop them a line in the morning asking about any limits they have on branches for OSS projects.

[ghost]

Each such branch would presumably be shortlived, so probably not; but we don't really want to do it anyway.

I suspect if we really want to have git involved in the synthesis pipeline we should keep it at least partially separate and host it ourselves. (E.g. we have a VM somewhere that we push candidates to and that the test/modelchecker VMs pull from.) I think there are probably better ways to do this than git though; maybe phabricator if it weren't written in PHP... version control systems aren't really meant to handle candidate changes, only finished ones.

Also, there's a tradeoff. If your synthesis pipeline is something that you run locally, then you can build and run it anywhere, including on a thousand AWS images. If it depends directly on a bunch of one-off cloud infrastructure, though, then you can only use it where and when that infrastructure is available; this is both potentially a scaling limit, a barrier to adoption of the tools by additional users, and a liability for the long-term lifespan of the tools. I have no idea to what extent we care about the latter two points.

[mwookawa]

so the good news is that it's not going to explode github. branches are just pointers in the git CAM. for example, the a difference between branch/HEAD, tags and branches is in interpretation by the git client software. the representation in-repo is just as an alias for a hash.

but, if i understand correctly, the only reason they are being pushed into public github as branches is so that circleci.com will be automatically triggered to pull them and run them, and not because we want them to be branches in our public github. in the very short term, would there be any disadvantage to deleting the branches after circleci runs and then using the hash that circleci pulled down to identify the code being tested rather than a branch name?

deleting the branches will also allow for us to use aggressive github garbage collection to prune the variants. if the branch names are never garbage collected, the commit hashes can't be garbage collected.

that said, for now can we fork guppy locally (ie, within harvard-princess) and run the guppypy experiments on harvard-princess/guppypy-fork ? then none of this is of particular concern, as we can just wipe the fork to garbage collect in one step.

On Mon, Jul 31, 2017 at 7:53 PM dh6713 notifications@github.com wrote:

Each such branch would presumably be shortlived, so probably not; but we don't really want to do it anyway.

I suspect if we really want to have git involved in the synthesis pipeline we should keep it at least partially separate and host it ourselves. (E.g. we have a VM somewhere that we push candidates to and that the test/modelchecker VMs pull from.) I think there are probably better ways to do this than git though; maybe phabricator if it weren't written in PHP... version control systems aren't really meant to handle candidate changes, only finished ones.

Also, there's a tradeoff. If your synthesis pipeline is something that you run locally, then you can build and run it anywhere, including on a thousand AWS images. If it depends directly on a bunch of one-off cloud infrastructure, though, then you can only use it where and when that infrastructure is available; this is both potentially a scaling limit, a barrier to adoption of the tools by additional users, and a liability for the long-term lifespan of the tools. I have no idea to what extent we care about the latter two points.

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/Harvard-PRINCESS/Guppy/issues/95#issuecomment-319228648, or mute the thread https://github.com/notifications/unsubscribe-auth/ABceTKrU4nHXMoqYlnfZywn0ufxWfX_Oks5sTmj5gaJpZM4OoSXI .

[alexpatel]

but, if i understand correctly, the only reason they are being pushed into public github as branches is so that circleci.com will be automatically triggered to pull them and run them, and not because we want them to be branches in our public github. in the very short term, would there be any disadvantage to deleting the branches after circleci runs and then using the hash that circleci pulled down to identify the code being tested rather than a branch name?

Great point - i didn't realize beforehand how annoying branch spamming would be. I just updated guppypy to delete the branches after circleci picks them up, @penlu if the ones you pushed were just tests can you push : them.

that said, for now can we fork guppy locally (ie, within harvard-princess) and run the guppypy experiments on harvard-princess/guppypy-fork ? then none of this is of particular concern, as we can just wipe the fork to garbage collect in one step.

Yes, I agree with this strategy.

[alexpatel]

re: @dh6713

I suspect if we really want to have git involved in the synthesis pipeline we should keep it at least partially separate and host it ourselves. (E.g. we have a VM somewhere that we push candidates to and that the test/modelchecker VMs pull from.) I think there are probably better ways to do this than git though; maybe phabricator if it weren't written in PHP... version control systems aren't really meant to handle candidate changes, only finished ones

AWS CodeDeploy would do the job (AWS ECS could then be triggered run the BarrelfishOS tests using Docker). I agree with Ming that git/github won't break.

Also, there's a tradeoff. If your synthesis pipeline is something that you run locally, then you can build and run it anywhere, including on a thousand AWS images. If it depends directly on a bunch of one-off cloud infrastructure, though, then you can only use it where and when that infrastructure is available; this is both potentially a scaling limit, a barrier to adoption of the tools by additional users, and a liability for the long-term lifespan of the tools. I have no idea to what extent we care about the latter two points.

AWS guarantees a 99.95% uptime on EC2 instances (down 4 hours a year). Isn't the scaling limit hit the minute you run out of sockets in MD121; user adoption lowered when in order to run your code you have to SSH into MD and work solely in your terminal; and long-term infrastructure liability limited when the on-premise infrastructure needs to be updated?

I would claim: given that the interesting part is the automating programming, not the infrastructure, why wouldn't we try to minimize to 0 (with the cloud) the physical computers that we have to bring up and take care of?

These two tradeoff points seem to me to be worded as conjectures - have these incidents happened a lot to you recently? This is one of those things that I would propose we just prototype and try before going out and manually configuring a bunch of machines. In my 16 months of AWS experience, I think I lost an EC2 once (only to have it replaced in minutes by the Auto-scaling group).

[alexpatel]

^ this is tongue in cheek, but I would ultimately claim that the cloud could be really valuable for a project like this

[mwookawa]

can we gup this over to the documents repo?

[ghost]

Where in the documents repo?

Anyway, I think you're missing the point. The two alternatives I'm describing are:

1. Implement the thing so it runs on one machine, or one machine that uses AWS control interfaces to fork itself as needed. It doesn't depend on other infrastructure, so anyone with an AWS (or similar) account can run it and if AWS goes glub it only needs porting to some other similar platform.
2. Implement the thing so that it depends on external resources, like git servers and a separate bank of test machines. Now it only works for us, and it will stop working for us when those other external resources get shut down or bitrot.

I'm not sure how "sockets in MD121" factor into this.

[alexpatel]

Cool @dh6713 thanks - I think I maybe don't fully understand the design of these alternatives or have the wrong mental image of them - when I next see you if you have time would love to chat more.