Added posts and excerpts.

_config.yml

@@ -53,6 +53,8 @@ baseurl: ""
 url: "https://plfa.github.io"
 markdown: kramdown
 theme: minima
+excerpt_separator: <!--more-->
+show_excerpts: true
 exclude:
   - "hs/"
   - "extra/"

_posts/2019-07-12-migration-to-2.6.0.1.md

@@ -3,10 +3,12 @@ layout : post
 title  : "Migration to Agda 2.6.0.1"
 ---
 
-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]({{ site.baseurl }}/GettingStarted/) to reinstall Agda and the standard library.
 
+<!--more-->
+
+For this upgrade, we made several major changes to the PLFA infrastructure.
+
 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
 agda --html --html-highlight=code FILE.lagda.md

_posts/2020-01-10-plfa-as-a-notebook.md

@@ -9,3 +9,5 @@ The notebook is based on [PLFA version 19.08][PLFA-19.08], with some minor chang
 
 [PLFA-19.08]: https://plfa.github.io/19.08/
 [NextJournal-PLFA]: https://nextjournal.com/plfa/ToC
+
+<!--more-->

_posts/2020-04-30-praise-for-plfa.md

@@ -11,3 +11,5 @@ title  : "Praise for PLFA!"
 
 [TSPL-2019]: https://plfa.github.io/20.07/TSPL/2019/
 [EUSA-2020]: https://www.eusa.ed.ac.uk/representation/campaigns/teachingawards2020/
+
+<!--more-->

_posts/2020-06-02-plfa-as-epub.md

@@ -12,3 +12,5 @@ Thanks to hard work by [Michael Reed][mreed20], and a little elbow grease on our
 [EPUB]: https://plfa.github.io/out/epub/plfa.epub
 [issue112]: https://github.com/plfa/plfa.github.io/issues/112
 [mreed20]: https://github.com/mreed20
+
+<!--more-->

_posts/2020-06-23-talking-about-plfa.md

@@ -8,3 +8,5 @@ We published a paper about PLFA, which describes our experiences writing the boo
 [SBMF]: https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf
 [SCP]: https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#scp
 [SF]: https://softwarefoundations.cis.upenn.edu/
+
+<!--more-->

_posts/2020-07-13-denotational-semantics.md

@@ -5,6 +5,8 @@ title  : "Introducing Part 3: Denotational Semantics"
 
 We’re pleased to announce an entirely new part of the book, contributed by Jeremy G. Siek! You may have noticed his name appearing on the list of authors some months ago, or the chapters that make up Part 3 slowly making their appearance. Well, that’s all Jeremy’s work!
 
+<!--more-->
+
 Part 3 introduces denotational semantics, presenting the denotational semantics of the untyped lambda calculus. Our development is unusual in that emphasizes the use of intersection type systems as denotational models instead of the more traditional domain theory, but this choice allows us to build upon the simple type systems studied in Part 2.
 Part 3 also proves the basic properties of the denotational semantics using techniques and variations of the techniques introduced in Part 2. We prove the *soundness* of reduction with respect to the denotational semantics by showing that reduction preserves and reflects denotations. We prove *adequacy* of the denotational semantics using a logical-relations style proof with respect to a big-step semantics of the untyped calculus. Finally, with these results in hand, we prove a standardisation theorem, that reduction to weak-head normal form implies the termination of call-by-name evaluation.
 

_posts/2020-07-14-versions-and-releases.md

@@ -5,6 +5,8 @@ title  : "Versions and Releases"
 
 We’re adding stable releases to PLFA!
 
+<!--more-->
+
 For the past two years, we’ve tried to do major revisions of the book during winter break and early summer, to ensure that the text remains consistent throughout the teaching period… Inevitably, we fixed bugs, and make small changes here and there, perhaps resulting in a less-than-consistent experience.
 
 Starting today, you can be sure that PLFA will remain consistent, since we’re adding stable releases! You can find the releases [on GitHub][releases], and as tags in the Git repository. The releases are numbered using [calendar versioning][CalVer] using the `YY0M` format, e.g., `20.07` was released in July 2020. Each release will have two associated tags.