Frequently Asked Questions

Administrativia

Getting and Using Beluga

Getting and Using Emacs

Assignments


Answers

Administrativia

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

A: Yes, you need a McGill School of Computer Science (SOCS) account in order to be able to submit assignments electronically. 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 assignments?

A: By using the handin file submission tool, available on the SOCS server mimi.cs.mcgill.ca. On mimi.cs.mcgill.ca, there is a special file repository called cs523, which contains directories called ass01, ass02, etc.. Each of these directories contains a subdirectory with your username, into which you can submit files by using the handin tool. All file submissions are done indirectly through handin, you need not worry about where exactly the cs523 repository is. For instance, to submit files for assignment 1, you would first make sure that the files you want to submit are located in your network-wide SOCS user account. You would then log in to mimi.cs.mcgill.ca and ask handin to place the relevant files into the ass01 directory of the cs523 repository. handin will then copy your files into the subdirectory with your username, from where we will be able to retrieve them. What follows is a more detailed, step-by-step tutorial on how to use handin.

From any Linux machine (such as the SOCS computers in the Trottier labs), you can open a terminal and run

ssh your_socs_username@mimi.cs.mcgill.ca

to log into your network-wide SOCS user account on mimi.cs.mcgill.ca, the SOCS server on which handin is set up. When logging in, you may be asked for your SOCS password. If you are on a SOCS computer (in cs.mcgill.ca) and are logged in under your username, you need only type

ssh mimi

Once logged in to mimi.cs.mcgill.ca, enter

handin -l cs523

to see what submission directories are available for COMP 523. You should see something like

Existing subdirectories (comments in parentheses):
ass01
ass02
ass03
ass04
ass05

Enter

handin cs523 assXX

to see what files you have submitted into the submission directory assXX (if any). If you have not submitted any files, the listing will be empty:

The following input files have been received:

To submit a file ~/somedir/somefile.bel into the directory for assignment 1, for instance, enter

handin cs523 ass01 ~/somedir/somefile.bel

The submission will be confirmed by a message similar to

Submitting /home/user/sheila1/somedir/somefile.bel... ok

Now, when checking which files have been received, we see the file we just submitted:

The following input files have been received:
Wed Jan 17 06:41:29 2007        0 bytes somefile.bel

If you submit a file which has the same filename as a previously submitted file, the previous file will get overwritten. Note that all submitted files get timestamped, and listing the files you've submitted displays the date and time when you submitted them.

Note that you can also submit multiple files at once:

handin cs523 assXX file1.bel file2.bel file3.bel ... fileN.bel

More information on handin can be found here.

If you are working from home, you can log in to mimi.cs.mcgill.ca remotely using ssh (if running Linux) or the SSH Secure Shell Client (if running Windows). The SSH Secure Shell Client for Windows is free for non-commercial and university use.

Note that to submit files using handin, your files need to be located in your SOCS account. This means that if you are submitting remotely, you must transfer your files to your SOCS account (using, for instance, sftp if running Linux, or the SSH File Transfer Client, which comes with the SSH Secure Shell Client, if running Windows) before being able to submit them via handin. See "How do I transfer files from my home machine to my SOCS user account?" for more information.


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

sftp your_socs_username@mimi.cs.mcgill.ca

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 mimi.cs.mcgill.ca 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 cs.mcgill.ca 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 your_socs_username@mimi.cs.mcgill.ca:~/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  => 
     y
  
  | {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 
                 /home/bpientka/complogic/beluga/examples/arith/arith.bel

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?".

Command

Action

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)

ctrl-a

home

ctrl-e

end

ctrl-k

kill everything on the current line after the cursor

alt-x sml

starts an SML buffer

alt-x shell

starts a shell buffer


Assignments

None yet!