Public | Automated Build

Last pushed: 3 years ago
Short Description
Software Foundations workshop container
Full Description

This container provides a Proof General environment and the
Software Foundations
sources, ready for you to begin your automated theorem
proving and certified programming adventure!

See the
Proof General user manual
if you need help with Coq script management and the
GNU Emacs manual
for help with Emacs.

To run the container for the first time:

docker run --name sf -it frasertweedale/sf

This will launch you straight into Emacs/Proof General at

If you exit Emacs, the container will stop. To re-enter the

docker start -ai sf

When you complete a module, you will need to compile the file. This
can be done via the Emacs menu (F10 to activate):

Coq  >  COQ PROG (ARGS)  >  Compile

You can then open the next module through the Find file prompt
activated via the menu:

File > Open File

This container runs Emacs directly, so there is no shell and no job
control. You can open a interactive shell inside Emacs via
M-x shell.

Docker Pull Command
Source Repository