Stupid Compiler

I’ve always been interested in computer assisted proof systems. Over the last year (or 2), I’ve been reading more and more on proving interesting properties of programs. I began with the very recent papers on security and safety properties of micro kernels (Gerwin Klein and Michael Norrish). From the NICTA work, I ended up working through much of the Isabelle proof system tutorials. The syntax of Isabelle felt very natural. Next, I read some of the French work (Xavier Leroy et al.) on formally verifying compilers. This led me to Coq and Benjamin Pierce’s exercises he has posted on his website. I’ve worked through a good 67% of those. Coq feels very pragmatic and the bundled environment is great to get started quick. Then, I took a few months break to look at a bunch of security stuff (static analysis work from Dawson Engler and the rest).

When I came back to it, I started reading the book Robert Harper is working on “Practical Foundations for Programming Languages”. This is dense (for me at least) and I’ve found myself having a hard time making too much progress. I think it would help to have an instructor, but in absence of that I have been taking large breaks in between chapters to decompress and let it marinate in my brain. My problem is remembering the vocabulary and notation each time, but after a day or two it comes back to me.

In any case, I came back to the work surrounding POPLMark and this led me to Twelf. I’ve been accumulating resources and wanted to put them all together for my own benefit. Maybe it will help someone else, but I think the Twelf wiki has a better selection — I’m just trying to keep track of what I have found and worked through.

• University of Oregon Summer School on Logic and Theorem Proving in Programming Languages
• Hints on Proving Theorems in Twelf
• Mechanizing Metatheory in Twelf
• Using Twelf to Prove Type Theorems

Today, I spent a few hours trying to figure out why my SMLNJ install kept failing. For the benefit of others who may have run into this problem, I’m going to record my solution (which I haven’t seen anywhere).

Issue 1:
I had a native Win32 install of SMLNJ at some point and my first failure looks like:

$ ./config/install.sh
...
//fs01/Home/dblazakis/projects/smlnj/bin/.link-sml: line 45: c:smlnj/bin/.arch-n-opsys: No such file or directory
...

Notice the native windows path — once I saw that I remembered I had SMLNJ_HOME set. So, from bash, ‘unset SMLNJ_HOME’.

Issue 2:
With that out of the way, I figured I was golden… but I was wrong. The next error:

$ ./config/install.sh
...
./config/install.sh: CM metadata directory name is ".cm"
exception raised during init phase: SysErr: No such file or directory [noent]
//fs01/Home/dblazakis/projects/smlnj/bin/.run/run.x86-cygwin: Fatal error -- Uncaught exception SysErr with <unknown> raised at <stat.c>
./config/install.sh !!! Boot code failed, no heap image (sml.x86-cygwin).

This one is more troublesome. First thought is that it is a path issue, so I add a few echos to the install script and everything looks correct to me. Next, I add a strace to the call in the install script which is failing (a call to generate the initial heap image containing the preloaded modules). This generates a ton of output even after masking to output only syscalls. Sifting through it, it appears the first open or stat call after reading the PIDMAP uses a single ‘/’ instead of the usual double ‘/’ to denote a network share.

...
340 27275136 [main] run.x86-cygwin 2956 normalize_posix_path: src /fs01/Home/dblazakis/projects/smlnj/sml.boot.x86-unix/smlnj/init
...

Poor cygwin — it tries so hard. This appears to be a bug in the SMLNJ SrcPath module (cm/paths/srcpath.sml), but this is the first time I’ve waded through the SMLNJ code.

Long story short, I decided to move my build to a local directory (instead of a network share) and it worked on the first try.