michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Made all internal URLs portable (using site.baseurl)

Browse source
This commit is contained in:
Wen Kokke 2019-07-15 17:39:12 +01:00
parent 7e30176b2b
commit 2a595363c0
7 changed files with 91 additions and 92 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
Makefile
View file

@ -14,12 +14,19 @@ endif
# Build PLFA and test hyperlinks
test: build
ruby -S bundle exec htmlproofer _site
ruby -S bundle exec htmlproofer '_site'
# Build PLFA and test hyperlinks offline
test-offline: build
ruby -S bundle exec htmlproofer _site --disable-external
ruby -S bundle exec htmlproofer '_site' --disable-external
# Build PLFA and test hyperlinks for stable
test-stable-offline: $(MARKDOWN)
ruby -S bundle exec jekyll clean
ruby -S bundle exec jekyll build --destination '_site/stable' --baseurl '/stable'
ruby -S bundle exec htmlproofer '_site' --disable-external
statistics:
@ -66,18 +73,11 @@ server-stop:
# Build website using jekyll
build: AGDA2HTML_FLAGS += --link-to-agda-stdlib=$(AGDA_STDLIB_URL)
build: $(MARKDOWN)
ruby -S bundle exec jekyll build
# Build website using jekyll offline
build-offline: $(MARKDOWN)
ruby -S bundle exec jekyll build
# Build website using jekyll incrementally
build-incremental: AGDA2HTML_FLAGS += --link-to-agda-stdlib
build-incremental: $(MARKDOWN)
ruby -S bundle exec jekyll build --incremental

1
README.md
View file

@ -58,7 +58,6 @@ The Makefile offers more than just these options:
make (see make test)
make build (builds lagda->markdown and the website)
make build-offline (builds lagda->markdown and the website offline)
make build-incremental (builds lagda->markdown and the website incrementally)
make test (checks all links are valid)
make test-offline (checks all links are valid offline)

2
_posts/2019-07-12-changes-to-plfa.md
View file

@ -5,7 +5,7 @@ title : "Changes to PLFA – Migration to Agda 2.6"
Today, we made several major changes to the PLFA infrastructure!
We upgraded to [Agda 2.6.0.1](https://github.com/agda/agda/releases/tag/v2.6.0.1) and [version 1.1 of the standard library](https://github.com/agda/agda-stdlib/releases/tag/v1.1). If you want to continue working with the book, you'll have to update your versions locally. Please follow the instructions in [Getting Started](/GettingStarted/) to reinstall Agda and the standard library.
We upgraded to [Agda 2.6.0.1](https://github.com/agda/agda/releases/tag/v2.6.0.1) and [version 1.1 of the standard library](https://github.com/agda/agda-stdlib/releases/tag/v1.1). If you want to continue working with the book, you'll have to update your versions locally. Please follow the instructions in [Getting Started]({{ site.baseurl }}/GettingStarted/) to reinstall Agda and the standard library.
We deprecated [agda2html](https://github.com/wenkokke/agda2html). In version 2.6, Agda has added support for the `--html-highlight` flag. Using this command, Agda will highlight only the code in a file, and leave the rest untouched:
```bash

12
courses/padova/2019/padova2019.md
View file

@ -1,7 +1,7 @@
---
title : "Padova: Course notes"
layout : page
permalink : /Padova/
permalink : /Padova/2019/
---
## Staff
@ -20,20 +20,20 @@ permalink : /Padova/
<table>
<tr>
<td><b>Wed 28 May</b></td>
<td><a href="/Naturals/">Naturals</a>,
<a href="/Induction/">Induction</a> &amp; <a href="/Relations/">Relations</a></td>
<td><a href="{{ site.baseurl }}/Naturals/">Naturals</a>,
<a href="{{ site.baseurl }}/Induction/">Induction</a> &amp; <a href="{{ site.baseurl }}/Relations/">Relations</a></td>
</tr>
<tr>
<td><b>Thu 29 May</b></td>
<td><a href="/Lambda/">Lambda</a> &amp;
<a href="/Properties/">Properties</a></td>
<td><a href="{{ site.baseurl }}/Lambda/">Lambda</a> &amp;
<a href="{{ site.baseurl }}/Properties/">Properties</a></td>
</tr>
</table>
## Assignments
For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/).
For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.baseurl }}/GettingStarted/).
* Wed 28 May
- Naturals (`_^_`)

48
courses/puc/2019/puc2019.md
View file

@ -21,15 +21,15 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L.
<table>
<tr>
<td><b>Fri 29 Mar</b></td>
<td><a href="/Naturals/">Naturals</a></td>
<td><a href="{{ site.baseurl }}/Naturals/">Naturals</a></td>
</tr>
<tr>
<td><b>Fri 5 Apr</b></td>
<td><a href="/Induction/">Induction</a> &amp; <a href="/Relations/">Relations</a></td>
<td><a href="{{ site.baseurl }}/Induction/">Induction</a> &amp; <a href="{{ site.baseurl }}/Relations/">Relations</a></td>
</tr>
<tr>
<td><b>Thu 11 Apr</b></td>
<td><a href="/Relations/">Relations</a></td>
<td><a href="{{ site.baseurl }}/Relations/">Relations</a></td>
</tr>
<tr>
<td><b>Fri 19 Apr</b></td>
@ -37,16 +37,16 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L.
</tr>
<tr>
<td><b>Fri 26 Apr</b></td>
<td><a href="/Equality/">Equality</a> &amp;
<a href="/Isomorphism/">Isomorphism</a> &amp;
<a href="/Connectives/">Connectives</a></td>
<td><a href="{{ site.baseurl }}/Equality/">Equality</a> &amp;
<a href="{{ site.baseurl }}/Isomorphism/">Isomorphism</a> &amp;
<a href="{{ site.baseurl }}/Connectives/">Connectives</a></td>
</tr>
<tr>
<td><b>Fri 3 May</b></td>
<td><a href="/Negation/">Negation</a> &amp;
<a href="/Quantifiers/">Quantifiers</a> &amp;
<a href="/Decidable/">Decidable</a> &amp;
<a href="/Lists/">Lists</a></td>
<td><a href="{{ site.baseurl }}/Negation/">Negation</a> &amp;
<a href="{{ site.baseurl }}/Quantifiers/">Quantifiers</a> &amp;
<a href="{{ site.baseurl }}/Decidable/">Decidable</a> &amp;
<a href="{{ site.baseurl }}/Lists/">Lists</a></td>
</tr>
<tr>
<td><b>Fri 10 May</b></td>
@ -58,8 +58,8 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L.
</tr>
<tr>
<td><b>Fri 24 May</b></td>
<td><a href="/Lambda/">Lambda</a> &amp;
<a href="/Properties/">Properties</a></td>
<td><a href="{{ site.baseurl }}/Lambda/">Lambda</a> &amp;
<a href="{{ site.baseurl }}/Properties/">Properties</a></td>
</tr>
<tr>
<td><b>Fri 31 May</b></td>
@ -67,8 +67,8 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L.
</tr>
<tr>
<td><b>Fri 7 June</b></td>
<td><a href="/DeBruijn/">DeBruijn</a> &amp;
<a href="/More/">More</a></td>
<td><a href="{{ site.baseurl }}/DeBruijn/">DeBruijn</a> &amp;
<a href="{{ site.baseurl }}/More/">More</a></td>
</tr>
<tr>
<td><b>Fri 14 June</b></td>
@ -76,8 +76,8 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L.
</tr>
<tr>
<td><b>Fri 21 June</b></td>
<td><a href="/Inference/">Inference</a> &amp;
<a href="/Untyped/">Untyped</a></td>
<td><a href="{{ site.baseurl }}/Inference/">Inference</a> &amp;
<a href="{{ site.baseurl }}/Untyped/">Untyped</a></td>
</tr>
<tr>
<td><b>Fri 28 June</b></td>
@ -92,15 +92,15 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L.
## Assignments
For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/).
For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.baseurl }}/GettingStarted/).
* [PUC Assignment 1](/PUC/2019/Assignment1/) due Friday 26 April.
* [PUC Assignment 2](/PUC/2019/Assignment2/) due Wednesday 22 May.
* [PUC Assignment 3](/PUC/2019/Assignment3/) due Wednesday 5 June.
* [PUC Assignment 4](/PUC/2019/Assignment4/) due Wednesday 19 June.
* [PUC Assignment 5](/PUC/2019/Assignment5/) due Tuesday 25 June.
* [PUC Assignment 6](/courses/tspl/2018/Mock1.pdf) due Tuesday 25 June.
Use file [Exam](/PUC/2019/Exam/). Despite the rubric, do **all three questions**.
* [PUC Assignment 1]({{ site.baseurl }}/PUC/2019/Assignment1/) due Friday 26 April.
* [PUC Assignment 2]({{ site.baseurl }}/PUC/2019/Assignment2/) due Wednesday 22 May.
* [PUC Assignment 3]({{ site.baseurl }}/PUC/2019/Assignment3/) due Wednesday 5 June.
* [PUC Assignment 4]({{ site.baseurl }}/PUC/2019/Assignment4/) due Wednesday 19 June.
* [PUC Assignment 5]({{ site.baseurl }}/PUC/2019/Assignment5/) due Tuesday 25 June.
* [PUC Assignment 6]({{ site.baseurl }}/courses/tspl/2018/Mock1.pdf) due Tuesday 25 June.
Use file [Exam]({{ site.baseurl }}/PUC/2019/Exam/). Despite the rubric, do **all three questions**.
Submit assignments by email to [wadler@inf.ed.ac.uk](mailto:wadler@inf.ed.ac.uk).
Attach a single file named `Assignment1.lagda.md` or the like. Include

54
courses/tspl/2018/tspl2018.md
View file

@ -27,51 +27,51 @@ Lectures take place Monday, Wednesday, and Friday in AT 7.02. (Moved from AT 5.0
</tr>
<tr>
<td>1</td>
<td><b>17 Sep</b> <a href="/Naturals/">Naturals</a></td>
<td><b>19 Sep</b> <a href="/Induction/">Induction</a></td>
<td><b>21 Sep</b> <a href="/Induction/">Induction</a></td>
<td><b>17 Sep</b> <a href="{{ site.baseurl }}/Naturals/">Naturals</a></td>
<td><b>19 Sep</b> <a href="{{ site.baseurl }}/Induction/">Induction</a></td>
<td><b>21 Sep</b> <a href="{{ site.baseurl }}/Induction/">Induction</a></td>
</tr>
<tr>
<td>2</td>
<td><b>24 Sep</b> <a href="/Relations/">Relations</a> (Chad)</td>
<td><b>26 Sep</b> <a href="/Relations/">Relations</a> (Chad)</td>
<td><b>24 Sep</b> <a href="{{ site.baseurl }}/Relations/">Relations</a> (Chad)</td>
<td><b>26 Sep</b> <a href="{{ site.baseurl }}/Relations/">Relations</a> (Chad)</td>
<td><b>28 Sep</b> (no class)</td>
</tr>
<tr>
<td>3</td>
<td><b>1 Oct</b> <a href="/Equality/">Equality</a> &amp; <a href="/Isomorphism/">Isomorphism</a></td>
<td><b>3 Oct</b> <a href="/Connectives/">Connectives</a></td>
<td><b>5 Oct</b> <a href="/Negation/">Negation</a></td>
<td><b>1 Oct</b> <a href="{{ site.baseurl }}/Equality/">Equality</a> &amp; <a href="{{ site.baseurl }}/Isomorphism/">Isomorphism</a></td>
<td><b>3 Oct</b> <a href="{{ site.baseurl }}/Connectives/">Connectives</a></td>
<td><b>5 Oct</b> <a href="{{ site.baseurl }}/Negation/">Negation</a></td>
</tr>
<tr>
<td>4</td>
<td><b>8 Oct</b> <a href="/Quantifiers/">Quantifiers</a></td>
<td><b>10 Oct</b> <a href="/Decidable/">Decidable</a></td>
<td><b>8 Oct</b> <a href="{{ site.baseurl }}/Quantifiers/">Quantifiers</a></td>
<td><b>10 Oct</b> <a href="{{ site.baseurl }}/Decidable/">Decidable</a></td>
<td><b>12 Oct</b> (tutorial only)</td>
</tr>
<tr>
<td>5</td>
<td><b>15 Oct</b> <a href="/Lists/">Lists</a></td>
<td><b>15 Oct</b> <a href="{{ site.baseurl }}/Lists/">Lists</a></td>
<td><b>17 Oct</b> (tutorial only)</td>
<td><b>19 Oct</b> <a href="/Lists/">Lists</a></td>
<td><b>19 Oct</b> <a href="{{ site.baseurl }}/Lists/">Lists</a></td>
</tr>
<tr>
<td>6</td>
<td><b>22 Oct</b> <a href="/Lambda/">Lambda</a></td>
<td><b>22 Oct</b> <a href="{{ site.baseurl }}/Lambda/">Lambda</a></td>
<td><b>24 Oct</b> (no class)</td>
<td><b>26 Oct</b> <a href="/Properties/">Properties</a></td>
<td><b>26 Oct</b> <a href="{{ site.baseurl }}/Properties/">Properties</a></td>
</tr>
<tr>
<td>7</td>
<td><b>29 Oct</b> <a href="/DeBruijn/">DeBruijn</a></td>
<td><b>31 Oct</b> <a href="/More/">More</a></td>
<td><b>2 Nov</b> <a href="/Inference/">Inference</a></td>
<td><b>29 Oct</b> <a href="{{ site.baseurl }}/DeBruijn/">DeBruijn</a></td>
<td><b>31 Oct</b> <a href="{{ site.baseurl }}/More/">More</a></td>
<td><b>2 Nov</b> <a href="{{ site.baseurl }}/Inference/">Inference</a></td>
</tr>
<tr>
<td>8</td>
<td><b>5 Nov</b> (no class)</td>
<td><b>7 Nov</b> (tutorial only)</td>
<td><b>9 Nov</b> <a href="/Untyped/">Untyped</a></td>
<td><b>9 Nov</b> <a href="{{ site.baseurl }}/Untyped/">Untyped</a></td>
</tr>
<tr>
<td>9</td>
@ -95,15 +95,15 @@ 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 PLFA see [Getting Started](/GettingStarted/).
For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.baseurl }}/GettingStarted/).
* [Assignment 1](/TSPL/2018/Assignment1/) cw1 due 4pm Thursday 4 October (Week 3)
* [Assignment 2](/TSPL/2018/Assignment2/) cw2 due 4pm Thursday 18 October (Week 5)
* [Assignment 3](/TSPL/2018/Assignment3/) cw3 due 4pm Thursday 1 November (Week 7)
* [Assignment 4](/TSPL/2018/Assignment4/) cw4 due 4pm Thursday 15 November (Week 9)
* [Assignment 5](/courses/tspl/2018/Mock1.pdf) cw5 due 4pm Thursday 22 November (Week 10)
* [Assignment 1]({{ site.baseurl }}/TSPL/2018/Assignment1/) cw1 due 4pm Thursday 4 October (Week 3)
* [Assignment 2]({{ site.baseurl }}/TSPL/2018/Assignment2/) cw2 due 4pm Thursday 18 October (Week 5)
* [Assignment 3]({{ site.baseurl }}/TSPL/2018/Assignment3/) cw3 due 4pm Thursday 1 November (Week 7)
* [Assignment 4]({{ site.baseurl }}/TSPL/2018/Assignment4/) cw4 due 4pm Thursday 15 November (Week 9)
* [Assignment 5]({{ site.baseurl }}/courses/tspl/2018/Mock1.pdf) cw5 due 4pm Thursday 22 November (Week 10)
<br />
Use file [Exam](/TSPL/2018/Exam/). Despite the rubric, do **all three questions**.
Use file [Exam]({{ site.baseurl }}/TSPL/2018/Exam/). Despite the rubric, do **all three questions**.
Assignments are submitted by running
@ -114,5 +114,5 @@ where N is the number of the assignment.
## Mock exam
Here is the text of the [second mock](/courses/tspl/2018/Mock2.pdf)
and the exam [instructions](/courses/tspl/2018/Instructions.pdf).
Here is the text of the [second mock]({{ site.baseurl }}/courses/tspl/2018/Mock2.pdf)
and the exam [instructions]({{ site.baseurl }}/courses/tspl/2018/Instructions.pdf).

48
index.md
View file

@ -13,48 +13,48 @@ Pull requests are encouraged.
## Front matter
- [Dedication](/Dedication/)
- [Preface](/Preface/)
- [Dedication]({{ site.baseurl }}/Dedication/)
- [Preface]({{ site.baseurl }}/Preface/)
## Part 1: Logical Foundations
- [Naturals](/Naturals/): Natural numbers
- [Induction](/Induction/): Proof by induction
- [Relations](/Relations/): Inductive definition of relations
- [Equality](/Equality/): Equality and equational reasoning
- [Isomorphism](/Isomorphism/): Isomorphism and embedding
- [Connectives](/Connectives/): Conjunction, disjunction, and implication
- [Negation](/Negation/): Negation, with intuitionistic and classical logic
- [Quantifiers](/Quantifiers/): Universals and existentials
- [Decidable](/Decidable/): Booleans and decision procedures
- [Lists](/Lists/): Lists and higher-order functions
- [Naturals]({{ site.baseurl }}/Naturals/): Natural numbers
- [Induction]({{ site.baseurl }}/Induction/): Proof by induction
- [Relations]({{ site.baseurl }}/Relations/): Inductive definition of relations
- [Equality]({{ site.baseurl }}/Equality/): Equality and equational reasoning
- [Isomorphism]({{ site.baseurl }}/Isomorphism/): Isomorphism and embedding
- [Connectives]({{ site.baseurl }}/Connectives/): Conjunction, disjunction, and implication
- [Negation]({{ site.baseurl }}/Negation/): Negation, with intuitionistic and classical logic
- [Quantifiers]({{ site.baseurl }}/Quantifiers/): Universals and existentials
- [Decidable]({{ site.baseurl }}/Decidable/): Booleans and decision procedures
- [Lists]({{ site.baseurl }}/Lists/): Lists and higher-order functions
## Part 2: Programming Language Foundations
- [Lambda](/Lambda/): Introduction to Lambda Calculus
- [Properties](/Properties/): Progress and Preservation
- [DeBruijn](/DeBruijn/): Inherently typed de Bruijn representation
- [More](/More/): Additional constructs of simply-typed lambda calculus
- [Bisimulation](/Bisimulation/): Relating reductions systems
- [Inference](/Inference/): Bidirectional type inference
- [Untyped](/Untyped/): Untyped lambda calculus with full normalisation
- [Lambda]({{ site.baseurl }}/Lambda/): Introduction to Lambda Calculus
- [Properties]({{ site.baseurl }}/Properties/): Progress and Preservation
- [DeBruijn]({{ site.baseurl }}/DeBruijn/): Inherently typed de Bruijn representation
- [More]({{ site.baseurl }}/More/): Additional constructs of simply-typed lambda calculus
- [Bisimulation]({{ site.baseurl }}/Bisimulation/): Relating reductions systems
- [Inference]({{ site.baseurl }}/Inference/): Bidirectional type inference
- [Untyped]({{ site.baseurl }}/Untyped/): Untyped lambda calculus with full normalisation
## Backmatter
- [Acknowledgements](/Acknowledgements/)
- [Fonts](/Fonts/): Test page for fonts
- [Statistics](/Statistics/): Line counts for each chapter
- [Acknowledgements]({{ site.baseurl }}/Acknowledgements/)
- [Fonts]({{ site.baseurl }}/Fonts/): Test page for fonts
- [Statistics]({{ site.baseurl }}/Statistics/): Line counts for each chapter
## Related
- Courses taught from the textbook:
* Philip Wadler, University of Edinburgh,
[2018](/TSPL/2018/)
[2018]({{ site.baseurl }}/TSPL/2018/)
* David Darais, University of Vermont,
[2018](http://david.darais.com/courses/fa2018-cs295A/)
* John Leo, Google Seattle, 2018--2019
* Philip Wadler, Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio),
[2019](/PUC/2019/)
[2019]({{ site.baseurl }}/PUC/2019/)
- A paper describing the book appeared in [SBMF][sbmf]
[wen]: https://github.com/wenkokke