Frequently Asked Questions


Getting and Using Beluga

Getting and Using Emacs



Q: Do I need a SOCS account/username, and if so, how do I get one?

A: No. But ou can get a McGill School of Computer Science (SOCS) account, if it would become necessary. If you are registered for the course (or any other COMP course), you are automatically eligible for a SOCS account.

The default log in screens of the SOCS computers in the Trottier labs (on the 3rd floor of Trottier) display instructions on how to obtain a SOCS account. If you encounter any difficulties during the automated account creation process, please contact the friendly SOCS sytems staff via email at help at cs dot mcgill dot ca, or, better yet, visit them in person in ENGMC 209N.

Q: How do I submit my project and report?

A:You should create a web-site with the material where the instructor can download the report and the .

Q: How do I transfer files from my home machine to my SOCS user account?

A: That depends on what operating system you use. If you use Windows, it's easiest to use a graphical file transfer client, such as the SSH File Transfer Client, which comes with the SSH Secure Shell Client. Other SSH and SFTP clients for Windows are also available, such as WinSCP and PuTTY.

Several graphical SSH and SFTP clients are also available for MacOS, such as Fugu and Fetch. Alternatively, MacOS also comes with implementations of the command-line tools ssh and sftp (see next paragraph).

Most UNIX-like operating systems (Linux, BSD, MacOS, etc.) come with command-line implementations of SSH and SFTP clients. The usage of the command-line SSH client (called ssh) was demonstrated in the answer to the previous question. Using the command-line SFTP client (called sftp) is not much more difficult. To log in to your SOCS account from any UNIX-like machine, run


You may be asked for your SOCS password. Note that since your SOCS account is available on all SOCS machines, you need not necessarily log in to to transfer files to your SOCS account. Any SOCS machine will do. (The hostnames of most lab machines and compute servers in the SOCS domain can be found here and here, respectively.)

Having logged in to your account via sftp, you will be able to navigate the filesystem using a subset of the commands available in most shells (run help when logged in through sftp to see all available commands). To transfer a file from your local filesystem to the remote filesystem, run

put foo.bel

This will locate the file foo.bel in the local filesystem (on your machine), looking in the current directory on your local machine (which will generally be the directory in which you ran sftp, although you can change it from an active sftp session), and will transfer it to the current directory on the remote machine. To go the other way, you can run

get foo.bel

to transfer the file foo.bel from the remote filesystem to your local one.

Rather than using sftp, you can also use a simpler tool called scp. This is exactly like the cp command for copying files, except that for the destination file (and even the source file, optionally), you also specify the hostname of the machine you want to do the copying to. If you're on your home machine, and you want to copy the file foo.bel to your SOCS account's home directory, the following will do.

scp foo.bel

You will probably be asked for your SOCS password again.

There are probably graphical SSH and SFTP clients for UNIX-like operating systems, as well, but if you're a UNIX user, I'm sure you don't need or want to use them. :)

Getting and Using Beluga

Q: What is Beluga?

A: Beluga is a dependently-typed functional programming language. It provides an implementation of the logical framework LF. In addition, it supports implementing dependently-typed recursive programs by pattern matching on LF objects. Beluga is implemented in OCaml.

Q: Where can I download Beluga?

A: At the official Beluga site. This site contains a link to a tar-ball for the most recent version which you have to download. In the tar-ball you can also find installation instructions for Unix-like operating systems, Macs, and Windows.

Q: How do I compile Beluga?

A: Beluga is written in OCaml. It requires at least OCaml 3.10 together with the following packages: omake, ocaml-findlib, libextlib-ocaml-dev, libounit-ocaml-dev ocaml-ulex. Once you have all the required OCaml packages, we recommend you generate native code when compile Beluga. This typically results in a 6x speed up.

omake NATIVE_ENABLED=true 

Q: How do I use the Beluga?

A: Beluga provides a type reconstruction engine and an interpreter/evaluator. The recommended way to develop and compile Beluga code is within Emacs using the beluga-mode. Uou can also compile Beluga perfectly well from a console terminal window (or DOS box under Windows). Here is a sample run whe you compile a Beluga program directly in a shell:

bpientka@boba:~/complogic/beluga$ bin/interpreter examples/arith/arith.bel

## Type Reconstruction: examples/arith/arith.bel ##

rec plus : nat[] -> nat[] -> nat[] = 
fn x => fn y => 
  case x of 
  | ([] z) : ^0 ; ^0  => 
  | {N :: nat[]}
    ([] s N) : ^1 ; ^0  => 
      (case plus ([] N) y of 
       | {N2 :: nat[]}  {N1 :: nat[]}
         ([] N1) :  . N2 = N , ^2 ; ^0  => 
          [] s N1
## Type Reconstruction done: examples/arith/arith.bel  ##

Q: What should I know about Beluga's error messages?

A: Type reconstruction is, in general, undecidable for the logical framework LF and for Beluga's dependently-typed functional language. For LF, our algorithm reports a principal type, a type error, or that the source term needs more type information. For our computation language, we check functions against a given type and either succeed, report a type error, or fail by asking for more type information. It is always possible to make typing unambiguous by adding more annotations.
Beluga is a system under development and its error messages could be improved. Luckily, its line and column numbers are quite precise and with some practice, you can usually figure out why it failed.

Getting and Using Emacs

Q: What is (1) emacs, (2) Beluga-mode?

A: (1) Emacs is a text editor that can do an astounding number of things. It is particularly suitable for writing Beluga (or Twelf or Agda2 or OCaml ) programs because of the existence of beluga-mode (see next point). (2) beluga-mode is an extension to emacs which was written by Stefan Monnier and is part of the Beluga distribution. Once installed, it allows emacs to enter a special mode customized for writing Beluga code. For instance, beluga-mode will allow you to compile and run a Beluga program from within emacs. Effectively, this allows you to write code in one buffer inside emacs, then immediately compile it in another buffer by pressing a single key combination. This saves you time, as otherwise, you would have to switch to a terminal or DOS box, launch Beluga separately.

Q: Can I use Beluga without emacs?

A: Yes, you can compile Beluga perfectly well from a console terminal window (or DOS box under Windows). However, beluga-mode under emacs provides some nifty shortcuts and, with practice, can significantly shorten the time you spend writing code. But is it not necessary to use emacs, and you will not be evaluated on anything related to it. Emacs has a steep learning curve, so it might be better to begin writing code in an editor your familiar with, and migrating later, if you like.

Q: Where can I download emacs?

A: There are two main forks of emacs, GNU Emacs and XEmacs, which can be downloaded from their respective sites. The two forks are very similar in behaviour and you can use either one. However, SML-mode was originally written for GNU Emacs, and it can be more difficult to get SML-mode working in XEmacs. Under Linux, it makes no difference which one you use, as SML-mode works well for both, but if using Windows, we would recommend GNU Emacs.

Some insight on why two forks exist is given here, while history and more background information is provided here.

Q: How do I install (1) GNU Emacs, (2) XEmacs?

A: (1) If you're running Linux, look here. For information on how to obtain and install GNU Emacs for Windows, look here. (2) XEmacs download and installation information for Unix-like OS's, MacOS, and Windows is provided here.

Q: I use Linux. (1) Where can I download beluga-mode for emacs? (2) How do I install it?

A: (1) The latest version of beluga-mode for emacs is part of the Beluga distribution. It is in the directory tools. (2) Move the belgua-mode.el contained in it into some convenient directory, such as ~/emacs/sml-mode. If you use GNU Emacs, add the following lines to the file ~/.emacs, creating it if it doesn't exist:

(add-to-list 'load-path "/home/bpientka/complogic/beluga/tools/")
(load "beluga-mode.el")

where you must replace "/home/bpientka/complogic/beluga/tools/" with the name of the directory that contains the beluga-mode file.

If you use XEmacs, you should add the lines above to the file ~/.xemacs/init.el, creating both the ~/.xemacs directory and the ~/.xemacs/init.el file if they don't exist.

If you restart emacs, Beluga-mode should now work. To test it, launch emacs (with emacs for GNU Emacs and xemacs for XEmacs) and open a file containing Beluga code (to open a file, use CTRL + x + f, then enter the name of the file). Press ALT + x to move the cursor to the minibuffer (the input line at the bottom of the Emacs window), press CTRL + c + c. Emacs should ask you what the command is to launch the Beluga interpreter and compiler:

Compile command: /home/bpientka/complogic/beluga/bin/interpreter 

Press enter to accept the default.

This should open a new buffer showing the result of compiling and executing your Beluga code.

Q: How do I use emacs?

A: Learning to use emacs is a lifelong endeavour, but here are a few key combinations that might come in handy. Again, though, bear in mind that you need not use emacs to use SML. See also "Using emacs, how do I run SML code I've saved in a file?".



ctrl-x ctrl-c

exit emacs

ctrl-x ctrl-s

save the file

ctrl-c ctrl-b

send filel to sml buffer

ctrl-x ctrl-f

open file

ctrl-x 2

split window horizontally

ctrl-x 3

split window vertically

ctrl-x 1

display current window only, hides split ones

ctrl-x ctrl-o

go to next window

ctrl-x k

kill current window (buffer)






kill everything on the current line after the cursor

alt-x sml

starts an SML buffer

alt-x shell

starts a shell buffer