Travel, Technology, Thoughts
Recently I found myself in a situation where I wanted to bring in a specific upstream commit into a forked repository. Although these repos share a common history, the two repos had diverged enough that it wasn’t a straight-forward cherry-pick between branches. Instead, with clones of the two repositories I managed to cherry-pick as follows:
git --git-dir=..//.git format-patch -k -1 --stdout | git am -3 -kRead more
I’ve recently hit an interesting issue involving Docker containers and compiled C code crashing code with illegal hardware instruction errors.
In a nutshell the Docker image was built on a server using Jenkins. It has been running fine until the underlying host orchestration software and physical hardware changed.
Read moreI use a lot of open source software in my research and work.
In recent months I’ve been modifying the source code of some of open source repositories to better suit my needs and I’ve contributed a few small changes back to the DeepLearning4J and the Snacktory projects.
This morning I’m starting to work on a further patch for the DeepLearning4J repository and I needed to bring my local repository up to date before committing the change. However, at some point over the past few months the DeepLearning4J repository has been rebased and my fork of it will no longer merge.
Read moreLike any good computer scientist I use git for many research and personal projects. My primary use of git is for code backups rather than collaborating with others. However, in some of my recent work I’ve been sharing repositories with colleagues and students which has caused me to improve my git skills.
The following is some of the functionality I’ve only recently discovered that has been extremely helpful:
git cherry-pick commit-id-numberRead more
I had an interesting discussion this afternoon which highlighted how important it is to understand conditional probability and how code structure can produce unexpected results.
The code contained three lists and a random number generator. The random number generator was meant to randomly chose which list to take something from with equal probability (that is 1/3 chance of selecting from each of the lists). However, somehow one of their lists was being selected far more than the others.
Read moreIt has just taken me around an hour to try and insert some previous and next month navigation links to the blog monthly archives. It seems that WordPress doesn’t have any real native support for this time of navigation which is odd.
The code below is my very hacky version of how to do it. I placed this in my theme’s archive.php file
Read moreRecently I have installed a colorbox plugin onto this blog for image galleries.
This plugin overrides the default behaviour of an image gallery and replaces individual image pages with a simple in-page pop up of the image. It works quite nicely, however, one problem I have had is that it extracts the title attribute from the former page links rather than the caption of the image that it is displaying.
I have spent the last few days trying to figure out a way to get the behaviour I want out of the plugin. However, this has been much more difficult that expected, the code that generates the galleries in WordPress is buried deep in the code and isn’t as straight-forward as replacing title=getTitle with title=getCaption. Trying to edit the behaviour of the jquery on the colorbox plugin isn’t an option either as it is heavily optimised. And updating every database row to replace the title with the caption also isn’t very practical.
Instead the simple hack below will achieve what I want. It isn’t pretty and I am still looking for a better solution, but in the meantime after the page has been rendered the jquery quickly looks for galleries and replaces the titles in any links with the alt text from the image. This means that when an image loads in the colorbox it displays with a caption.
<script type="text/javascript">
jQuery(document).ready(function($) {
$('.gallery img').each(function() {
$(this).parent().attr('title',$(this).attr('alt'));
});
});
</script>