Running F* from a docker image

Download and install Docker for your host platform, from https://docs.docker.com/, you have to make sure that the docker service is started.

• In a terminal, run $ docker pull fstarlang/fstar-emacs for a version with Emacs and the F* mode preinstalled (If you only need the command line $ docker pull fstarlang/fstar is a lighter option).

• You can get bash shell using $ docker run -it fstarlang/fstar-emacs

• To persist state, just exit from the image, look up the stopped container using $ docker ps -a and start it again using $ docker start -i <CONTAINER ID>.

• You can already run command line emacs by typing emacs in the shell or directly write $ docker run -it fstarlang/fstar-emacs emacs. Running emacs in graphics mode requires an X server which is configured differently depending on your platform:

F* in docker with Emacs GUI on Mac OS X

• Install XQuartz

• Open an XQuartz terminal, and run $ socat TCP-LISTEN:6000,reuseaddr,fork UNIX-CLIENT:\"$DISPLAY\"

• On a Mac OS X terminal, run

 $ ip=$(ifconfig en0 | grep inet | awk '$1=="inet" {print $2}')
 $ docker run -d -e DISPLAY=${ip}:0 fstarlang/fstar-emacs emacs

If you prefer to get a bash shell, then run

$ docker run -it -e DISPLAY=${ip}:0 fstarlang/fstar-emacs

From the shell, you can start an emacs client that will connect to your XQuartz server with just emacs.

F* in docker with Emacs GUI on Linux

Install docker using the package manager of your distribution.

• Ubuntu: # apt-get install docker
• Archlinux: # pacman -S docker (more information on the Arch wiki on Docker, in particular you need to enable the docker service and will probably want to allow running docker as a regular user)
• ...

Download and run the docker image.

• $ docker pull fstarlang/fstar-emacs

• $ docker run -it -e DISPLAY=:0.0 -v /tmp/.X11-unix:/tmp/.X11-unix fstarlang/fstar-emacs emacs

You should now be looking at an emacs window. To make sure everything works, open the file `/FStar/FStar/examples/hello/hello.fst. You can now verify this small example using the key combination Ctrl-c followed by Ctrl-n. The background of the verified part of the code should now be coloured blue. For more information on how to use emacs with F*, see the documentation of fstar-mode<\link>.

F* in docker with Emacs GUI on Windows

• Install docker using the binary installer. If you have only windows home edition you may have to install Docker Quickstart Terminal.

• For X-window support install MobaXterm Home Edition

• Run $ ipconfig in powershell to learn your IP address

• $ docker run -it -e DISPLAY=<ip address>:0.0 fstarlang/fstar-emacs to get a bash shell to start emacs from.