The Population Cycle of Lemmas

You don't "cover" for me; you manage expectations.

--Donald Draper

Previously, I mentioned that I was solving a trillion instances.  That was the original plan.  One thousand instances in a modified cnf file, one thousand files in a folder, one thousand folders in a zip file, and one thousand zip files.  Somewhere along the line, maybe precisely when I realized that individual uncompressed folders exceeded 500 mb in size and I couldn't even fit a thousand of them on disk, I switched the thousand folders per zip file to 1 folder per zip file, and promptly forgot the effect it would have on the order of magnitude of the size of my data set.  So, I'll be generating 1.001 billion instances to test with, as opposed to 1.001 trillion.  Yes, I could simply generate a million zip files and stick them on a giant hard drive, unfortunately, I've also recently discovered that with the resources at my disposal it would take years to accomplish that.

I could generate 1 trillion, if there were exactly 1000 clones of me (thanks to the .001 its one thousand and not 999 clones) but I think I'm going to settle for the billions instead.  Either sum is pathetic compared to the size of the search space (number of atoms in the universe?  please) so what does it matter?  The only danger is if there was an elusive, super-hard worst case instance that was only going to appear if I generated a trillion.

I need to begin work on the proof anyway.  Why do I need to begin this?  Because I just hit the limit for the number of cores I am allowed to rent from Windows Azure.  Fun fact:  if you need to do CPU intensive work, you may find it far cheaper to rent 8 extra-small shared-CPU instances than to rent a single 8-core server.

The next technical difficulty other than maxing out my Azure subscription (a point in Amazon EC2's favor) is getting the data off the hard drives before they fill up.  Given that I can apparently only use the most basic libraries with mono, and given that I want to move the files and not just sync them, the best option was to use FTP.  You know, that old ass file moving protocol on port 21.  Well, guess what.  FTP is actually not a simple file moving protocol that does everything through port 21.  Port 21 is just the beginning.  If you have to manually open ports to a box in order for it to work, you are going to learn a lot about passive mode, and active mode, and port 20, and ranges of ports in both the client and server, and bugs in various popular FTP clients.  I'm sure the cludgy-ass design made sense back when harddrives only held 30 MB, but holy shit it is awful now.  And it transmits the password in clear text!  If I was going to design a protocol to be a headache of a security risk, I would write FTP.  I got an active-mode FTP client that can punch through the Azure firewall.  Unfortunately it does not work from inside the Azure firewall.  Go figure.  I would like to formally protest all network protocols that can still have connection failures after you've established a connection.


In light of this, the least amount of work is probably going to be to manually log into the servers and clean the files out myself.  Oh, I forgot to mention I implemented a simple workflow engine in mysql and php.  That was fucking awesome.  Anyway.

Azure has its own version of S3, but you can't directly upload files larger than 64 MB do it--you have to break it up into blocks, and the libraries provided probably won't run in mono.  In the choice between [not using mono, and therefore .NET on windows, which means] having to log in to my servers with some graphical bullshit, verses having to manually move files, the latter seems way more fun.

I want to say that I don't understand why you still can't just ssh into windows (powershell doesnt count) but I actually know why;  I just want it to complain about it.

My next strategy with the proof aspect is I'm going to try and see what small things I can prove about my algorithm (if condition X, can I always succeed at clause finding?) and then see if I can build a proof out of those smaller statements.  I believe these are called lemmas, and then the axioms are the ones that are obvious/self evident.

Knowing that girls in the future could read what I write today is making temporal mechanics a real problem for my writing.  For now, I haven't written anything but math shit, yet my readership is growing.  I wish blogger would let me ban Seattle IP addresses.  In this town all of the attractive girls that know how to set up a proxy to get around regional restrictions always turn out to be guys in real life anyway, which is {tolerance affirmation}.