small changes

2018-10-14 11:57:05 +01:00 · 2018-10-14 11:57:05 +01:00 · f0b1dd7fbc
commit f0b1dd7fbc
parent d3ae7cbeb9 0b2539758a
9 changed files with 90 additions and 75 deletions
--- a/Gemfile.lock
+++ b/Gemfile.lock
@ -14,10 +14,11 @@ GEM
    coffee-script-source (1.11.1)
    colorator (1.1.0)
    colorize (0.8.1)
-    commonmarker (0.17.9)
+    commonmarker (0.17.13)
      ruby-enum (~> 0.5)
    concurrent-ruby (1.0.5)
-    dnsruby (1.60.2)
+    dnsruby (1.61.2)
+      addressable (~> 2.5)
    em-websocket (0.5.1)
      eventmachine (>= 0.12.9)
      http_parser.rb (~> 0.6.0)
@ -25,27 +26,27 @@ GEM
      ffi (>= 1.3.0)
    eventmachine (1.2.7)
    execjs (2.7.0)
-    faraday (0.15.2)
+    faraday (0.15.3)
      multipart-post (>= 1.2, < 3)
    ffi (1.9.25)
    forwardable-extended (2.6.0)
    gemoji (3.0.0)
-    github-pages (187)
+    github-pages (192)
      activesupport (= 4.2.10)
      github-pages-health-check (= 1.8.1)
-      jekyll (= 3.7.3)
-      jekyll-avatar (= 0.5.0)
+      jekyll (= 3.7.4)
+      jekyll-avatar (= 0.6.0)
      jekyll-coffeescript (= 1.1.1)
      jekyll-commonmark-ghpages (= 0.1.5)
      jekyll-default-layout (= 0.1.4)
-      jekyll-feed (= 0.9.3)
+      jekyll-feed (= 0.10.0)
      jekyll-gist (= 1.5.0)
      jekyll-github-metadata (= 2.9.4)
-      jekyll-mentions (= 1.3.0)
+      jekyll-mentions (= 1.4.1)
      jekyll-optional-front-matter (= 0.3.0)
      jekyll-paginate (= 1.1.0)
      jekyll-readme-index (= 0.2.0)
-      jekyll-redirect-from (= 0.13.0)
+      jekyll-redirect-from (= 0.14.0)
      jekyll-relative-links (= 0.5.3)
      jekyll-remote-theme (= 0.3.1)
      jekyll-sass-converter (= 1.5.2)
@ -66,12 +67,12 @@ GEM
      jekyll-theme-tactile (= 0.1.1)
      jekyll-theme-time-machine (= 0.1.1)
      jekyll-titles-from-headings (= 0.5.1)
-      jemoji (= 0.9.0)
-      kramdown (= 1.16.2)
+      jemoji (= 0.10.1)
+      kramdown (= 1.17.0)
      liquid (= 4.0.0)
      listen (= 3.1.5)
      mercenary (~> 0.3)
-      minima (= 2.4.1)
+      minima (= 2.5.0)
      nokogiri (>= 1.8.2, < 2.0)
      rouge (= 2.2.1)
      terminal-table (~> 1.4)
@ -81,10 +82,10 @@ GEM
      octokit (~> 4.0)
      public_suffix (~> 2.0)
      typhoeus (~> 1.3)
-    html-pipeline (2.8.3)
+    html-pipeline (2.8.4)
      activesupport (>= 2)
      nokogiri (>= 1.4)
-    html-proofer (3.9.1)
+    html-proofer (3.9.2)
      activesupport (>= 4.2, < 6.0)
      addressable (~> 2.3)
      colorize (~> 0.8)
@ -96,7 +97,7 @@ GEM
    http_parser.rb (0.6.0)
    i18n (0.9.5)
      concurrent-ruby (~> 1.0)
-    jekyll (3.7.3)
+    jekyll (3.7.4)
      addressable (~> 2.4)
      colorator (~> 1.0)
      em-websocket (~> 0.5)
@ -109,7 +110,7 @@ GEM
      pathutil (~> 0.9)
      rouge (>= 1.7, < 4)
      safe_yaml (~> 1.0)
-    jekyll-avatar (0.5.0)
+    jekyll-avatar (0.6.0)
      jekyll (~> 3.0)
    jekyll-coffeescript (1.1.1)
      coffee-script (~> 2.2)
@ -123,15 +124,14 @@ GEM
      rouge (~> 2)
    jekyll-default-layout (0.1.4)
      jekyll (~> 3.0)
-    jekyll-feed (0.9.3)
+    jekyll-feed (0.10.0)
      jekyll (~> 3.3)
    jekyll-gist (1.5.0)
      octokit (~> 4.2)
    jekyll-github-metadata (2.9.4)
      jekyll (~> 3.1)
      octokit (~> 4.0, != 4.4.0)
-    jekyll-mentions (1.3.0)
-      activesupport (~> 4.0)
+    jekyll-mentions (1.4.1)
      html-pipeline (~> 2.3)
      jekyll (~> 3.0)
    jekyll-optional-front-matter (0.3.0)
@ -139,7 +139,7 @@ GEM
    jekyll-paginate (1.1.0)
    jekyll-readme-index (0.2.0)
      jekyll (~> 3.0)
-    jekyll-redirect-from (0.13.0)
+    jekyll-redirect-from (0.14.0)
      jekyll (~> 3.3)
    jekyll-relative-links (0.5.3)
      jekyll (~> 3.3)
@ -195,14 +195,13 @@ GEM
      jekyll-seo-tag (~> 2.0)
    jekyll-titles-from-headings (0.5.1)
      jekyll (~> 3.3)
-    jekyll-watch (2.0.0)
+    jekyll-watch (2.1.1)
      listen (~> 3.0)
-    jemoji (0.9.0)
-      activesupport (~> 4.0, >= 4.2.9)
+    jemoji (0.10.1)
      gemoji (~> 3.0)
      html-pipeline (~> 2.2)
      jekyll (~> 3.0)
-    kramdown (1.16.2)
+    kramdown (1.17.0)
    liquid (4.0.0)
    listen (3.1.5)
      rb-fsevent (~> 0.9, >= 0.9.4)
@ -210,15 +209,15 @@ GEM
      ruby_dep (~> 1.2)
    mercenary (0.3.6)
    mini_portile2 (2.3.0)
-    minima (2.4.1)
+    minima (2.5.0)
      jekyll (~> 3.5)
      jekyll-feed (~> 0.9)
      jekyll-seo-tag (~> 2.1)
    minitest (5.11.3)
    multipart-post (2.0.0)
-    nokogiri (1.8.4)
+    nokogiri (1.8.5)
      mini_portile2 (~> 2.3.0)
-    octokit (4.9.0)
+    octokit (4.12.0)
      sawyer (~> 0.8.0, >= 0.5.3)
    parallel (1.12.1)
    pathutil (0.16.1)
@ -231,9 +230,9 @@ GEM
    ruby-enum (0.7.2)
      i18n
    ruby_dep (1.5.0)
-    rubyzip (1.2.1)
+    rubyzip (1.2.2)
    safe_yaml (1.0.4)
-    sass (3.5.6)
+    sass (3.6.0)
      sass-listen (~> 4.0.0)
    sass-listen (4.0.0)
      rb-fsevent (~> 0.9, >= 0.9.4)
@ -259,4 +258,4 @@ DEPENDENCIES
  html-proofer

 BUNDLED WITH
-   1.16.2
+   1.16.4
--- a/GettingStarted.md
+++ b/GettingStarted.md
@ -1,25 +1,25 @@
 ---
-layout: page
-title: Setting up Agda for PLFA
-permalink: /GettingStarted/
+layout    : page
+title     : Getting Started with Agda and PLFA
+permalink : /GettingStarted/
 ---

 Download the latest version of Programming Language Foundations in Agda from Github:

-```
-$ git clone https://github.com/plfa/plfa.github.io ~/plfa.github.io
+``` 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:

-```
-$ git clone https://github.com/plfa/agda-stdlib ~/agda-stdlib
+``` 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:

-```
-$ mkdir ~/.agda
+``` 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:
@ -42,8 +42,8 @@ plfa

 Finally, we need to enable the Emacs mode for Agda. To do so, run:

-```
-$ agda-mode setup
+``` 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!
@ -51,7 +51,8 @@ If all goes well, when you open a file ending in `.agda` or `.lagda` with Emacs,
 ## 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, 
--- a/51
+++ b/51
@ -1,6 +1,7 @@
-agda := $(wildcard src/*.lagda) $(wildcard src/**/*.lagda)
-agdai := $(wildcard src/*.agdai) $(wildcard src/**/*.agdai)
-markdown := $(subst src/,out/,$(subst .lagda,.md,$(agda)))
+agda := $(wildcard src/*.lagda) $(wildcard src/**/*.lagda) $(wildcard tspl/*.lagda) $(wildcard tspl/**/*.lagda)
+agdai := $(wildcard src/*.agdai) $(wildcard src/**/*.agdai) $(wildcard tspl/*.agdai) $(wildcard tspl/**/*.agdai)
+markdown := $(subst tspl/,out/,$(subst src/,out/,$(subst .lagda,.md,$(agda))))
+PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))

 all: $(markdown)

@ -18,6 +19,12 @@ out/%.md: src/%.lagda | out/
 		| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
 	@sed -i '1 s|---|---\nsrc       : $(<)|' $@

+# should fix this -- it's the same as above
+out/%.md: tspl/%.lagda | out/
+	agda2html --verbose --link-to-agda-stdlib --link-to-local-agda-names --use-jekyll=out/ -i $< -o $@ 2>&1 \
+		| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
+	@sed -i '1 s|---|---\nsrc       : $(<)|' $@
+
 serve:
 	ruby -S bundle exec jekyll serve

@ -34,7 +41,7 @@ build: $(markdown)
 	ruby -S bundle exec jekyll build

 # build website using jekyll incrementally
-build-incremental:
+build-incremental: $(markdown)
 	ruby -S bundle exec jekyll build --incremental

 # remove all auxiliary files
@ -58,36 +65,44 @@ macos-setup:

 # install agda, agda-stdlib, and agda2html
 travis-setup:\
-	$(HOME)/agda-master/\
-	$(HOME)/agda-stdlib-master/\
-	$(HOME)/agda2html-master/\
-	$(HOME)/acknowledgements-master/
+	$(HOME)/.local/bin/agda\
+	$(HOME)/.local/bin/agda2html\
+	$(HOME)/.local/bin/acknowledgements\
+	$(HOME)/agda-stdlib-master/src\
+	$(HOME)/.agda/defaults\
+	$(HOME)/.agda/libraries

-$(HOME)/agda-master/:
+$(HOME)/.agda/defaults:
+	echo "standard-library" >> $(HOME)/.agda/defaults
+	echo "plfa" >> $(HOME)/.agda/defaults
+
+$(HOME)/.agda/libraries:
+	echo "$(HOME)/agda-stdlib-master/standard-library.agda-lib" >> $(HOME)/.agda/libraries
+	echo "$(PLFA_DIR)/plfa.agda-lib" >> $(HOME)/.agda/libraries
+
+$(HOME)/.local/bin/agda:
 	curl -L https://github.com/agda/agda/archive/master.zip -o $(HOME)/agda-master.zip
 	unzip -qq $(HOME)/agda-master.zip -d $(HOME)
 	cd $(HOME)/agda-master;\
 		stack install --stack-yaml=stack-8.2.2.yaml

-$(HOME)/agda-stdlib-master/:
-	curl -L https://github.com/agda/agda-stdlib/archive/master.zip -o $(HOME)/agda-stdlib-master.zip
-	unzip -qq $(HOME)/agda-stdlib-master.zip -d $(HOME)
-	mkdir -p $(HOME)/.agda
-	echo "standard-library" > $(HOME)/.agda/defaults
-	echo "$(HOME)/agda-stdlib-master/standard-library.agda-lib" > $(HOME)/.agda/libraries
-
-$(HOME)/agda2html-master/:
+$(HOME)/.local/bin/agda2html:
 	curl -L https://github.com/wenkokke/agda2html/archive/master.zip -o $(HOME)/agda2html-master.zip
 	unzip -qq $(HOME)/agda2html-master.zip -d $(HOME)
 	cd $(HOME)/agda2html-master;\
 		stack install

-$(HOME)/acknowledgements-master/:
+$(HOME)/.local/bin/acknowledgements:
 	curl -L https://github.com/plfa/acknowledgements/archive/master.zip -o $(HOME)/acknowledgements-master.zip
 	unzip -qq $(HOME)/acknowledgements-master.zip -d $(HOME)
 	cd $(HOME)/acknowledgements-master;\
 		stack install

+$(HOME)/agda-stdlib-master/src:
+	curl -L https://github.com/agda/agda-stdlib/archive/master.zip -o $(HOME)/agda-stdlib-master.zip
+	unzip -qq $(HOME)/agda-stdlib-master.zip -d $(HOME)
+	mkdir -p $(HOME)/.agda
+
 .phony: serve build test clean clobber macos-setup travis-setup

 # workaround for a bug in agda2html
--- a/_config.yml
+++ b/_config.yml
@ -33,6 +33,7 @@ theme: minima
 exclude:
  - "hs/"
  - "src/"
+  - "tspl/"
  - "extra/"
  - "vendor/"
  - "Notes.md"
--- a/src/plfa/Inference.lagda
+++ b/src/plfa/Inference.lagda
@ -186,7 +186,7 @@ We can extract the grammar for terms from the above:

    L⁺, M⁺, N⁺ ::=                      terms with synthesized type
      x                                   variable
-      L⁺ · M-                             application
+      L⁺ · M⁻                             application
      M⁻ ↓ A                              switch to inherited

    L⁻, M⁻, N⁻ ::=                      terms with inherited type
--- a/src/plfa/Assignment1.lagda
+++ b/src/plfa/Assignment1.lagda
@ -34,7 +34,7 @@ open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
  ≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
-open import plfa.Relations using (_<_; z<s; s<s)
+open import plfa.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
 \end{code}

 ## Naturals
--- a/src/plfa/Assignment2.lagda
+++ b/src/plfa/Assignment2.lagda
@ -5,7 +5,7 @@ permalink : /Assignment2/
 ---

 \begin{code}
-module plfa.Assignment2 where
+module Assignment2 where
 \end{code}

 ## YOUR NAME AND EMAIL GOES HERE
--- a/src/plfa/Assignments.lagda
+++ b/src/plfa/Assignments.lagda
@ -14,7 +14,7 @@ You don't need to do all of these, but should attempt at least a few.
 Exercises without a label are optional, and may be done if you want
 some extra practice.

-* [Assignment 1][plfa.Assignment1] Due 4pm Thursday 4 October (Week 3)
+* [Assignment 1][Assignment1] Due 4pm Thursday 4 October (Week 3)

  + Naturals
    - `seven`
@ -42,12 +42,12 @@ some extra practice.
    - `<-trans` (recommended)
    - `trichotomy`
    - `+-mono-<`
-    - `≤-iff-<` (recommended) 
+    - `≤-iff-<` (recommended)
    - `<-trans-revisited`
    - `o+o≡e` (recommended)
    - `Bin-predicates` (stretch)

-* [Assignment 2][plfa.Assignment2]. Due 4pm Thursday 18 October (Week 5)
+* [Assignment 2][Assignment2]. Due 4pm Thursday 18 October (Week 5)

  + Equality
    - `≤-reasoning` (stretch)
--- a/src/plfa/TSPL.lagda
+++ b/src/plfa/TSPL.lagda
@ -95,17 +95,16 @@ Lectures take place Monday, Wednesday, and Friday in AT 7.02. (Moved from AT 5.0

 ## Assignments

-For instructions on how to set up Agda for the assignments,
-see [here](/GettingStarted/).
+For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/).

-* [Assignment 1][plfa.Assignment1] cw1 due 4pm Thursday 4 October (Week 3)
-* [Assignment 2][plfa.Assignment2] cw2 due 4pm Thursday 18 October (Week 5)
+* [Assignment 1][Assignment1] cw1 due 4pm Thursday 4 October (Week 3)
+* [Assignment 2][Assignment2] cw2 due 4pm Thursday 18 October (Week 5)
 * Assignment 3 cw3 due 4pm Thursday 1 November (Week 7)
 * Assignment 4 cw4 due 4pm Thursday 15 November (Week 9)
 * Assignment 5 cw5 due 4pm Thursday 22 November (Week 10)

-Assignments are submitted as
-
-    submit tspl cw1 Assignment1
-
-and similarly for the others.
+Assignments are submitted by running
+``` bash
+submit tspl cw1 AssignmentX
+```
+where `X` is the number of the assignment.