### Some useful and free Mac apps

Here are several really useful free Mac apps that I’ve come across recently:

• Macfusion (free). Lets you mount remote filesystems over SSH or FTP, and access them through Finder. Far nicer than using the ssh command in Terminal, or a third-party FTP client. Depends on OSXFUSE. Notes:
• Finder does already provide FTP access (via “Connect to server…”), but it’s read-only.
• In order to have write access over SSH, you’ll need to do the trick described here to map your local username to the username of your SSH account.
• I find it convenient to place a link to Macfusion.app in Finder’s toolbar.
• BetterTouchTool (free). Brings to Mac the excellent ‘aero-snap’ feature of Windows 7 (plus a few other nice features).
• Spark (free). Lets you assign custom keyboard shortcuts. Really stable and powerful. Doesn’t look to have been updated for a couple of years, but still works fine on Snow Leopard.
• VirtualBox (free). Run Windows or Linux on your Mac – and no need to dual boot. I’m staggered by how well this works.
• BibDesk (free). I use this to manage my PDF library. Very powerful and customisable.
• PDFNut (free). A PDF viewer with Chrome-style tabs. I only started using it yesterday, and I love it already.

### The Isabelle logo as end-of-proof symbol

In a recent research paper, I formalised some of my theorems in the proof assistant Isabelle, but left some of them as just proved ‘by hand’. I found it helpful to use a different ‘QED’ symbol depending on which method I had used.

Below is an enlarged version of the ‘three cubes’ symbol in the snippet above, together with the original Isabelle logo for comparison. The new symbol is designed to be suitable for black-and-white printing at a small size, and can be generated by the LaTeX code given below.

\usepackage{tikz}
\newcommand{\isabelleqed}{%
\begin{tikzpicture}[x=0.8mm, y=0.8mm,
baseline=-0.3mm, line join=round]
\begin{scope}[yslant=-0.5]
\draw (0,0) rectangle +(1,1);
\draw (2,1) rectangle +(1,1);
\draw (1,2) rectangle +(1,1);
\end{scope}
\begin{scope}[yslant=0.5]
\filldraw (1,-1) rectangle +(1,1);
\filldraw (3,-2) rectangle +(1,1);
\filldraw (2,0) rectangle +(1,1);
\end{scope}
\begin{scope}[yslant=0.5,xslant=-1]
\draw (1,0) rectangle +(1,1);
\draw (2,-1) rectangle +(1,1);
\draw (3,1) rectangle +(1,1);
\end{scope}
\end{tikzpicture}%
}

One could even go a step further, and extend this idea into a potential new logo for Isabelle.

The picture above is generated by the following LaTeX code.

\begin{tikzpicture}[x=4mm, y=4mm, baseline=6mm,
line join=round, draw=black]
\begin{scope}[every node/.append style={yslant=-0.5}, yslant=-0.5]
\filldraw[fill=blue!25] (0,0) rectangle +(1,1);
\node at (0.5,0.5) {$\lambda$};
\filldraw[fill=blue!25] (2,1) rectangle +(1,1);
\node at (2.5,1.5) {$=$};
\filldraw[fill=yellow!25] (1,2) rectangle +(1,1);
\node at (1.5,2.5) {$\vdash$};
\filldraw[fill=red!25] (4,2) rectangle +(1,1);
\node at (4.5,2.5) {$\alpha$};
\filldraw[fill=red!25] (3,3) rectangle +(1,1);
\node at (3.5,3.5) {$\rightarrow$};
\filldraw[fill=yellow!25] (2,4) rectangle +(1,1);
\node at (2.5,4.5) {$\forall$};
\end{scope}
\begin{scope}[yslant=0.5]
\filldraw[fill=black!25!blue] (1,-1) rectangle +(1,1);
\filldraw[fill=black!25!blue] (3,-2) rectangle +(1,1);
\filldraw[fill=black!25!yellow] (2,0) rectangle +(1,1);
\filldraw[fill=black!25!yellow] (3,1) rectangle +(1,1);
\filldraw[fill=black!25!red] (4,-1) rectangle +(1,1);
\filldraw[fill=black!25!red] (5,-3) rectangle +(1,1);
\end{scope}
\begin{scope}[yslant=0.5,xslant=-1]
\filldraw[fill=blue] (1,0) rectangle +(1,1);
\filldraw[fill=blue] (2,-1) rectangle +(1,1);
\filldraw[fill=yellow] (3,1) rectangle +(1,1);
\filldraw[fill=yellow] (5,2) rectangle +(1,1);
\filldraw[fill=red] (4,0) rectangle +(1,1);
\filldraw[fill=red] (3,-2) rectangle +(1,1);
\end{scope}
\end{tikzpicture}\hspace{4mm}{\Huge\bf Isabelle}

### Why apostrophes are important…

He has feet the size of rabbits.
He has feet the size of rabbits’.

### Trivia+cryptic crossword

Here is a crossword. Some clues are cryptic, and some are general knowledge. Good luck!

ACROSS

5. Tunnel built by friend following vehicle? (6)

8. Whose tombstone in Vienna reads S = k log W? (6,9)

9. Pneumatic tool for RAF practice? (3,5)

11. Plant of the year? (6)

12. The heart, in Hebrew, is found in Jewish ale vessel (5)

13. Their work is provided by the devil (4,5)

18. Which Minnesotan city might appeal to a Czech? (3,6)

22. Which fabric originates from the French city of Nîmes? (5)

23. Which Renault engineer is famous for his curves? (6)

24. … (2,6)

25. Which former colony (flag pictured) boasts the world’s most livable city (according to The Economist) (7,8)?

26. Path taken by falling satellite (6)

27. Which institution, founded in 1458, has won University Challenge a record four times? (8)

DOWN

1. Which British PM’s term as a transport minister saw the introduction of zebra crossings? (9)

2. By which computing phenomenon can x − y  > x be true for positive y? (9)

3. Largest French waterway avoids European capital to expose tributary? (4,5)

4. Loops around reel? (5)

5. Industrial building? (7)

6. Which country was represented by the first “perfect 10.0” Olympic gymnast? (7)

7. Objectivist philosopher, and yarn spinner? (3,4)

10. Prone to deceiving? (5)

14. German lies in gladioli (e.g. tristis) (5)

15. Investment in shrubbery? (5,4)

16. The solution is not to use any words (3-6)

17. As above (4,5)

19. Contemplate steep descent? (3,4)

20. Rope artist? (7)

21. What did chemical engineer Erik Rotheim invent in 1926 to help wax his skis? (7)

24. What is the website of the world’s oldest continuously-published encyclopedia? (2.3)

### How the HSBC SecureKey works

Update: I now know the description below to be inaccurate. See the comments section below.

Here is my guess at how the new HSBC SecureKey device works…

Each device has its own method for generating a long sequence of 6-digit numbers (example: divide the previous number by 13, add 5, and swap the second and fourth digits around). That method is known only to the device itself, and HSBC’s central database. That database stores, for each device serial number, (1) how that device’s sequence is generated, and (2) where the device is currently at in the sequence. When you press the green button after entering your PIN, the next 6-digit number in the sequence is generated and shown. When you type that number into the HSBC login page, HSBC updates its database to advance to the next number in the sequence, and checks that it matches the number you entered.

This process will eventually, after several years, exhaust the sequence of 6-digit numbers. Thereupon, the sequence will begin all over again.

A slight refinement is necessary. I can make my device get ‘out of sync’ with the HSBC database by repeatedly pressing the green button, but not trying to log in using the numbers it generates. To address this situation, the HSBC login page must accept not merely the very next number in the sequence, but any of the next, say, hundred numbers, and update its database accordingly.

### How to fix a Roland HP 136 Digital Piano

I wanted to investigate a dodgy key on my Roland HP 136 Digital Piano, and found the web to be surprisingly unable to advise me on how to go about this. This post presents some information that I had hoped to find. (Follow this advice at your own risk, I merely claim that this worked for me.)

### Opening the case

1. Remove two screws from the underside of the piano …
2. … then three screws from the back of the piano…
3. … and then lift the lid. Result:

### Removing a key

1. Unhook the spring at the back of the key.
2. Push a screwdriver into the slot (as shown in the photo below) and prise the key out.
3. I found that in order to free the key completely, I had to slide the whole rack of keys backwards a little. This required removing several more bolts from the piano’s underside.

It turned out that the dodgy key was caused by a snapped hammer. I superglued it back together and it has been playing fine ever since.

I found it a little long-winded to import PDFs from the web into my BibDesk library. My old workflow was as follows:

1. Open the PDF in my browser.
2. Choose “Save Page as…” from the menu bar, and save the PDF to my desktop.
3. Open BibDesk.
4. Drag the PDF from my desktop into my BibDesk library.
5. Edit the title/author etc. of the new publication.
6. Hit shift-cmd-k to ‘auto file’ the downloaded PDF into my Papers folder.

Below is an AppleScript I wrote to automate this procedure. Now my workflow is:

1. Copy the URL of the PDF file.
2. Launch the AppleScript below (a keyboard shortcut can be configured for this).
3. Paste the URL.
4. Edit the title/author etc. of the new publication.

Much nicer!

-- Get URL of a pdf file
tell application "Finder"
set returneditems to (display dialog ¬
"Enter PDF URL:" buttons {"Add", "Cancel"} ¬
default answer "" default button 1)
set buttonpressed to button returned of returneditems
set theURL to text returned of returneditems
end tell

if buttonpressed = "Cancel" then
return
end if

-- Make sure all existing publications are auto-filed
(* This is necessary because the last pdf added by
this script will currently be stored at
tell application "BibDesk"
activate
open "/Users/johnwickerson/Documents/Papers/John.bib"
set theDoc to get first document
tell theDoc
repeat with thePub in publications
tell thePub to auto file
end repeat
end tell
end tell

set localfile to ¬
tell application "URL Access Scripting"
end tell

-- add new publication to database
tell application "BibDesk"
activate
open "/Users/johnwickerson/Documents/Papers/John.bib"
set theDoc to get first document
tell theDoc
set newPub to make new publication ¬
at the beginning of publications
tell newPub
add (POSIX file localfile) to ¬
end tell