diff --git a/_config.yml b/_config.yml index a14f2ff9..95a13981 100644 --- a/_config.yml +++ b/_config.yml @@ -53,6 +53,8 @@ baseurl: "" url: "https://plfa.github.io" markdown: kramdown theme: minima +excerpt_separator: +show_excerpts: true exclude: - "hs/" - "extra/" diff --git a/_posts/2019-07-12-migration-to-2.6.0.1.md b/_posts/2019-07-12-migration-to-2.6.0.1.md index 65bb0300..a6708a11 100644 --- a/_posts/2019-07-12-migration-to-2.6.0.1.md +++ b/_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. + + +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 diff --git a/_posts/2020-01-10-plfa-as-a-notebook.md b/_posts/2020-01-10-plfa-as-a-notebook.md index 40df4ca8..5c15eb92 100644 --- a/_posts/2020-01-10-plfa-as-a-notebook.md +++ b/_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 + + diff --git a/_posts/2020-04-30-praise-for-plfa.md b/_posts/2020-04-30-praise-for-plfa.md index 8742b41e..f85e66e0 100644 --- a/_posts/2020-04-30-praise-for-plfa.md +++ b/_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/ + + diff --git a/_posts/2020-06-02-plfa-as-epub.md b/_posts/2020-06-02-plfa-as-epub.md index 425929b5..0756d5fb 100644 --- a/_posts/2020-06-02-plfa-as-epub.md +++ b/_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 + + diff --git a/_posts/2020-06-23-talking-about-plfa.md b/_posts/2020-06-23-talking-about-plfa.md index 05981110..3a4359f8 100644 --- a/_posts/2020-06-23-talking-about-plfa.md +++ b/_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/ + + diff --git a/_posts/2020-07-13-denotational-semantics.md b/_posts/2020-07-13-denotational-semantics.md index e6cfe520..4ec99d9b 100644 --- a/_posts/2020-07-13-denotational-semantics.md +++ b/_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! + + 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. diff --git a/_posts/2020-07-14-versions-and-releases.md b/_posts/2020-07-14-versions-and-releases.md index e8702252..f149707d 100644 --- a/_posts/2020-07-14-versions-and-releases.md +++ b/_posts/2020-07-14-versions-and-releases.md @@ -5,6 +5,8 @@ title : "Versions and Releases" We’re adding stable releases to PLFA! + + 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.