added instructions

This commit is contained in:
wadler 2018-11-26 18:57:39 -03:00
parent 0437f480e4
commit a8b1f9d46a
3 changed files with 195 additions and 0 deletions

View file

@ -6,6 +6,80 @@ permalink: /about/
[![Build Status](https://travis-ci.org/plfa/plfa.github.io.svg?branch=dev)](https://travis-ci.org/plfa/plfa.github.io) [![Build Status](https://travis-ci.org/plfa/plfa.github.io.svg?branch=dev)](https://travis-ci.org/plfa/plfa.github.io)
Download the latest version of Programming Language Foundations in Agda from Github:
``` bash
git clone https://github.com/plfa/plfa.github.io ~/plfa.github.io
```
Download the version of the Agda standard library that works with the textbook:
``` bash
git clone https://github.com/plfa/agda-stdlib ~/agda-stdlib
```
We need to tell Agda to use the standard library, and the material
from Programming Language Foundations in Agda by default. Create a
directory called `.agda` inside of your home directory:
``` bash
mkdir ~/.agda
```
Agda expects `~/.agda` to contain two files:
1. `~/.agda/libraries`, a list of all the libraries we want Agda to
know about; and
2. `~/.agda/defaults`, a list of the libraries we want Agda to load
by default.
Create `~/.agda/libraries`. It should contain:
```
~/agda-stdlib/standard-library.agda-lib
~/plfa.github.io/plfa.agda-lib
```
Next, create `~/.agda/defaults` and edit its contents to be:
```
standard-library
plfa
```
Finally, we need to enable the Emacs mode for Agda. To do so, run:
``` bash
agda-mode setup
```
If all goes well, when you open a file ending in `.agda` or `.lagda`
with Emacs, the buffer for that file should have the Agda major mode
enabled by default.
## Fonts in Emacs
It is reccommended that you add the following to the end of your emacs
configuration file at `~/.emacs`, if you have the named fonts available.
``` elisp
;; Setting up Fonts for use with Agda/PLFA
;;
;; default to DejaVu Sans Mono,
(set-face-attribute 'default nil
:family "DejaVu Sans Mono"
:height 120
:weight 'normal
:width 'normal)
;; fix \:
(set-fontset-font "fontset-default"
(cons (decode-char 'ucs #x2982)
(decode-char 'ucs #x2982))
"STIX")
```
## How to build the book ## How to build the book
There are several tools you need to build a local copy of the book: There are several tools you need to build a local copy of the book:

BIN
tspl/instructions.pdf Normal file

Binary file not shown.

121
tspl/instructions.tex Normal file
View file

@ -0,0 +1,121 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Instructions for TSPL Exam
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[12pt]{article}
\usepackage{a4,amssymb}
% \setlength{\oddsidemargin}{-1.5cm}
% \addtolength{\textwidth}{2cm}
% \addtolength{\textheight}{3cm}
\begin{document}
\pagestyle{empty}
\setcounter{page}{1}
\begin{center}
\large Types and Semantics for Programming Languages
\end{center}
\section*{Instructions}
\begin{enumerate}
\item The exam lasts two hours.
\item Place your student identity card face-up on the desk in
front of you. The invigilator may come to check your identity, and
in this case you may be asked to allow the invigilator to briefly
use your computer. The exam time has been calculated to allow time
for such interruptions.
\item You may log into your computer as soon as you are ready to do so.
\item To download the exam paper, open a terminal window and
type the following:
\begin{center}
\texttt{getpapers}
\end{center}
This will create a subdirectory \texttt{tspl-pe} in your home directory,
containing the following files.
\begin{center}
\begin{tabular}{ll}
\texttt{tspl-pe/papers/exam.pdf} & the exam \\
\texttt{tspl-pe/papers/instructions.pdf} & these instructions \\
\texttt{tspl-pe/templates/Exam.lagda} & exam template to edit \\
\texttt{tspl-pe/original\_templates/Exam.lagda} & backup of exam template
\end{tabular}
\end{center}
The directories \texttt{tspl-pe/papers}, \texttt{tspl-pe/original\_templates} are
read only, but you may read and write \texttt{tspl-pe/templates}.
\item The textbook \emph{Programming Language Foundations in Agda} is available
by pointing your browser at:
\begin{center}
\texttt{file:///group/examreadonly/full/plfa/}
\end{center}
\item The Agda standard library is available by pointing your browser at:
\begin{center}
\texttt{file:///group/examreadonly/full/agda-stdlib/}
\end{center}
\item The Agda user manual is available by pointing your browser at:
\begin{center}
\texttt{file:///group/examreadonly/full/agda-docs/}
\end{center}
{\it (Note that internet access has been disabled.)}
\begin{center}
\textbf{Do nothing further until the start of the exam is announced!}
\end{center}
\hfill \textit{Please Turn Over}
\newpage
\item When the start of the exam is announced, open the exam paper
\begin{center}
\texttt{tspl-pe/papers/exam.pdf}
\end{center}
with the standard PDF viewer.
\item Change to the template directory
\begin{center}
\texttt{cd tspl-pe/templates}
\end{center}
and edit the file
\begin{center}
\texttt{Exam.lagda}
\end{center}
to include your answers, using Emacs or anything else suitable.
You are recommended to save your work on a regular basis.
\item Before submitting, make sure your file is processed by Agda
correctly. Code which prevents the file from compiling should be
made into comments. If you fail to solve part of a problem, you
may get more credit if you indicate clearly which part you have
not solved.
\item \emph{Please ensure before submission that the file}
\texttt{Exam.lagda} \emph{contains your solutions to the exam.} Submit
your file using the command:
\begin{center}
\texttt{examsubmit Exam.lagda}
\end{center}
If you get an error, please check carefully that your file is called
\texttt{Exam.lagda} and that you are in the same directory as this
file. If you continue to have problems, please contact one of the
invigilators.
Repeated submit commands are allowed, and will overwrite previous
submissions. The last file submitted will be the one marked.
\item When the invigilators announce the end of the exam, you must
submit and log out immediately.
\end{enumerate}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: