Merged README and GettingStarted
This commit is contained in:
parent
7d320fdf0c
commit
8babe49f9f
2 changed files with 2 additions and 73 deletions
|
@ -1,71 +0,0 @@
|
|||
---
|
||||
layout : page
|
||||
title : Getting Started with Agda and PLFA
|
||||
permalink : /GettingStarted/
|
||||
---
|
||||
|
||||
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
|
||||
```
|
||||
|
||||
When you run Agda, it looks in this directory to figure out which libraries to use. Specifically, 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 use all the time.
|
||||
|
||||
Using your favourite text editor, 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`:
|
||||
|
||||
``` elisp
|
||||
;; Setting up Fonts for use with Agda/PLFA on DICE machines:
|
||||
;;
|
||||
;; 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")
|
||||
```
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
---
|
||||
layout: page
|
||||
title: About
|
||||
permalink: /about/
|
||||
title: Getting Started
|
||||
permalink: /GettingStarted/
|
||||
---
|
||||
|
||||
[![Build Status](https://travis-ci.org/plfa/plfa.github.io.svg?branch=dev)](https://travis-ci.org/plfa/plfa.github.io)
|
||||
|
|
Loading…
Reference in a new issue