Using Twelf on Windows

[noncom]

Setting up a development environment for Twelf on Windows

1. Instal Git Bash and GNU Make

Git bash provides some basic Linux commands like date, which, hostname and cat. These are needed for automatically filling the buildid info in a further step. Make sure they are available in PATH.

Make sure that make is also available in PATH.

2. Install SML/NJ

SML/NJ is an implementation of SML that works well on Windows and should be easy to install.

NOTE: MLton, another well-known implementation, might work too, as it recently started providing a Windows build, but I haven't found an easy way to use it because the main launch script is still written in bash, and having to work with it through something like Git Bash complicates the process, making it hard to organize interop with other programs in Windows. Also, MLton doesn't provide a REPL like SML/NJ does, so it would be not so interactive. Poly/ML is yet another implementation that supports Windows, but I haven't worked with it much yet. So this instruction concentrates on SML/NJ currently.

After installing SML/NJ make sure that sml is avilable in PATH.

NOTE: To quit the SML/NJ interpreter, send the end-of-file character, which means Ctrl+Z on Windows (or Ctrl+D on Linux). See https://www.cs.cornell.edu/courses/cs312/2008sp/handouts/faq.htm.

3. Clone Twelf

Clone Twelf and make sure the bin folder of the cloned repo is in the PATH.

For building Twelf we'll be closely following the smlnj target from the Makefile, but performing the steps manually since some scripts of the original target are written for a Linux shell. There are not many steps though. If you want, you can create something like a smlnj-win target, and formalize them later.

4. Create buildid

In the cloned Twelf repository run

make buildid

This should generate the <twelf-repo>/src/frontend/buildid.sml file.
NOTE: You will probably see an error that svnversion command wasn't found, but that's not a problem.

Open the generated buildid.sml file, and if the revision field is empty, add something there for a good measure, like a random number or the current commit hash or whatever.

5. Build the server

This is an adaptation of the twelf-server-smlnj target in the Makefile.

In the cloned Twelf repository run

sml build/twelf-server-smlnj.sml

This step should run for a while, generating a lot output in the console, for everything that's getting compiled. The result should be the compiled server file, something like <twelf-repo>/bin/.heap/twelf-server.x86-win32. The suffix of the filename might differ depending on the toolchain. If you're using a 32bit SML/NJ interpreter, the generated build is also going to be 32bit.

Next run

sml @SMLload="<twelf-repo>/bin/.heap/twelf-server"

NOTE: This is a Windows adaptation of <twelf-repo>/bin/.mkexec, and I'm skipping specifying @SMLdebug, since I'm not sure what would be a good Windows setting for it.

This should print something like

Twelf 1.7.1+ (r1, built 01/17/25 at 19:29:52 on DESKTOP-G7CH5LH)
%% OK %%

Which would mean that the build was successful.

6. Preparing a server bat file for the VSCode extension

Next prepare a bat file for launching the server. There's an existing <twelf-repo>/bin/.twelf-server.bat file, but it looks a bit Linux-y on the inside. So to create a proper Windows adaptation of it, create a file named twelf-server.bat beside it, and copy the following content into it:

@echo off
sml @SMLload=%TWELFDIR%/bin/.heap/twelf-server.x86-win32

Where %TWELFDIR% is a system variable that points to the cloned Twelf repository.

NOTE: For me %TWELFFIR% variable didn't work for some reason, either I did something wrong, or SML/NJ doesn't expand the path. So in the end I had to simply hard-code the full path instead of using the variable.

7. The VSCode extension

Install the Twelf Extension Pack extension by IvanMazzon. Unfortunately the way it works with the path to Twelf would only work on Linux, and I found no repository for the extension to propose fixing that, so it would have to be modified a little to work on Windows.

• Go to C:\Users\<user>\.vscode\extensions\ivan-m.twelf-extension-pack-1.0.1\src and open extension.js.
• Find the startMainTerminalIfNecessary() function and find this code fragment:

if (serverPath == null) {
    vscode.window.showErrorMessage("Error: folder twelf/bin not added to PATH.");
    return false;
}

• Replace it with:

if (serverPath == null) {
    serverPath = "<twelf-repo>/bin/twelf-server.bat";
    //vscode.window.showErrorMessage("Error: folder twelf/bin not added to PATH.");
    //return false;
}

where replace <twelf-repo> with your actual path to the cloned repository.

• Restart the exension or VSCode.

8. Test

• Open a workspace folder
• Create a test.elf file
• Paste some Twelf code into it, for example:

nat : type.
z   : nat.
s   : nat -> nat.

even   : nat -> type.
even-z : even z.
even-s : even (s (s N))
  <- even N.

plus   : nat -> nat -> nat -> type.
plus-z : plus z N2 N2.
plus-s : plus (s N1) N2 (s N3)
  <- plus N1 N2 N3.

• Run the Twelf: Start server command
• You should see the Twelf Server terminal open (*), with the same info/status printout as in step 5
• Run the Twelf: Run current file command.
• You should see some checks running with some status, hopefully %% OK %% at the end.

(*) -- For some reason I couldn't make this happen on one of the machines, the terminal simply won't show. Not sure why, probably the extension was unable to find or run Twelf even with the changes, even though Twelf worked ok when running it from the command line. I haven't yet found the reason why.

9. Success!

Profit!