From 2a595363c0c001fbb879342257526129f135a0c1 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Mon, 15 Jul 2019 17:39:12 +0100 Subject: [PATCH] Made all internal URLs portable (using site.baseurl) --- Makefile | 18 +++++----- README.md | 1 - _posts/2019-07-12-changes-to-plfa.md | 2 +- courses/padova/2019/padova2019.md | 12 +++---- courses/puc/2019/puc2019.md | 48 ++++++++++++------------- courses/tspl/2018/tspl2018.md | 54 ++++++++++++++-------------- index.md | 48 ++++++++++++------------- 7 files changed, 91 insertions(+), 92 deletions(-) diff --git a/Makefile b/Makefile index 75796db0..09afd41a 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/README.md b/README.md index aa12d39c..1db48783 100644 --- a/README.md +++ b/README.md @@ -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) diff --git a/_posts/2019-07-12-changes-to-plfa.md b/_posts/2019-07-12-changes-to-plfa.md index 5b1d4bf2..f3e17726 100644 --- a/_posts/2019-07-12-changes-to-plfa.md +++ b/_posts/2019-07-12-changes-to-plfa.md @@ -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 diff --git a/courses/padova/2019/padova2019.md b/courses/padova/2019/padova2019.md index dd3f2649..d9bb2b23 100644 --- a/courses/padova/2019/padova2019.md +++ b/courses/padova/2019/padova2019.md @@ -1,7 +1,7 @@ --- title : "Padova: Course notes" layout : page -permalink : /Padova/ +permalink : /Padova/2019/ --- ## Staff @@ -20,20 +20,20 @@ permalink : /Padova/ - + - +
Wed 28 MayNaturals, - Induction & RelationsNaturals, + Induction & Relations
Thu 29 MayLambda & - PropertiesLambda & + Properties
## 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 (`_^_`) diff --git a/courses/puc/2019/puc2019.md b/courses/puc/2019/puc2019.md index 42672415..af5d6d5e 100644 --- a/courses/puc/2019/puc2019.md +++ b/courses/puc/2019/puc2019.md @@ -21,15 +21,15 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L. - + - + - + @@ -37,16 +37,16 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L. - + - + @@ -58,8 +58,8 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L. - + @@ -67,8 +67,8 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L. - + @@ -76,8 +76,8 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L. - + @@ -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 diff --git a/courses/tspl/2018/tspl2018.md b/courses/tspl/2018/tspl2018.md index 70208680..b0bd4e53 100644 --- a/courses/tspl/2018/tspl2018.md +++ b/courses/tspl/2018/tspl2018.md @@ -27,51 +27,51 @@ Lectures take place Monday, Wednesday, and Friday in AT 7.02. (Moved from AT 5.0 - - - + + + - - + + - - - + + + - - + + - + - + - + - + - - - + + + - + @@ -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)
- 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). diff --git a/index.md b/index.md index 4e2e43d6..b641a6fb 100644 --- a/index.md +++ b/index.md @@ -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
Fri 29 MarNaturalsNaturals
Fri 5 AprInduction & RelationsInduction & Relations
Thu 11 AprRelationsRelations
Fri 19 Apr
Fri 26 AprEquality & - Isomorphism & - ConnectivesEquality & + Isomorphism & + Connectives
Fri 3 MayNegation & - Quantifiers & - Decidable & - ListsNegation & + Quantifiers & + Decidable & + Lists
Fri 10 May
Fri 24 MayLambda & - PropertiesLambda & + Properties
Fri 31 May
Fri 7 JuneDeBruijn & - MoreDeBruijn & + More
Fri 14 June
Fri 21 JuneInference & - UntypedInference & + Untyped
Fri 28 June
117 Sep Naturals19 Sep Induction21 Sep Induction17 Sep Naturals19 Sep Induction21 Sep Induction
224 Sep Relations (Chad)26 Sep Relations (Chad)24 Sep Relations (Chad)26 Sep Relations (Chad) 28 Sep (no class)
31 Oct Equality & Isomorphism3 Oct Connectives5 Oct Negation1 Oct Equality & Isomorphism3 Oct Connectives5 Oct Negation
48 Oct Quantifiers10 Oct Decidable8 Oct Quantifiers10 Oct Decidable 12 Oct (tutorial only)
515 Oct Lists15 Oct Lists 17 Oct (tutorial only)19 Oct Lists19 Oct Lists
622 Oct Lambda22 Oct Lambda 24 Oct (no class)26 Oct Properties26 Oct Properties
729 Oct DeBruijn31 Oct More2 Nov Inference29 Oct DeBruijn31 Oct More2 Nov Inference
8 5 Nov (no class) 7 Nov (tutorial only)9 Nov Untyped9 Nov Untyped
9