diff --git a/LICENSE b/LICENSE index 2fb94156..1c85e069 100644 --- a/LICENSE +++ b/LICENSE @@ -33,7 +33,7 @@ exhaustive, and do not form part of our licenses. material not subject to the license. This includes other CC- licensed material, or material used under an exception or limitation to copyright. More considerations for licensors: - wiki.creativecommons.org/Considerations_for_licensors + wiki.creativecommons.org/Considerations_for_licensors Considerations for the public: By using one of our public licenses, a licensor grants the public permission to use the @@ -49,8 +49,8 @@ exhaustive, and do not form part of our licenses. such as asking that all changes be marked or described. Although not required by our licenses, you are encouraged to respect those requests where reasonable. More considerations - for the public: - wiki.creativecommons.org/Considerations_for_licensees + for the public: + wiki.creativecommons.org/Considerations_for_licensees ======================================================================= diff --git a/Notes.md b/Notes.md index b4019c2f..6b466739 100644 --- a/Notes.md +++ b/Notes.md @@ -30,7 +30,7 @@ Git commands to create a branch and pull request git branch -- list all branches git branch -- create new local branch git checkout -- make the current branch - git merge -- merge branch into current branch + git merge -- merge branch into current branch git push origin -- make local branch into remote On website, use pulldown menu to swith branch and then @@ -39,9 +39,9 @@ click "new pull request" button. ## Suggestion from Conor for Inference Conor McBride - + 29 Oct 2018, 09:34 - + Hi Phil In a rush, but... @@ -108,11 +108,11 @@ Three possible orders: + (a) As current + (b) Put Lists immediately after Induction. - requires moving composition & extensionality earlier - - requires moving parameterised modules earlier for monoids + - requires moving parameterised modules earlier for monoids - add material to relations: - lexical ordering, subtype ordering, All, Any, All-++ iff + lexical ordering, subtype ordering, All, Any, All-++ iff - add material to isomorphism: All-++ isomorphism - - retain material on decidability of All, Any in Decidable + - retain material on decidability of All, Any in Decidable + (c) Put Lists after Decidable - requires moving Any-decidable from Decidable to Lists + (d) As (b) but put parameterised modules in a separate chapter @@ -121,7 +121,7 @@ Tradeoffs: + (b) Distribution of exercises near where material is taught + (b) Additional reinforcement for simple proofs by induction + (a,c) Can drop material if there is lack of time - + (a,c) Earlier emphasis on induction over evidence + + (a,c) Earlier emphasis on induction over evidence + (c) More consistent structuring principle ## Set up lists of exercises to do @@ -188,9 +188,9 @@ Tradeoffs: + defined break, make to extract a prefix and count primes at end of an id. But hard to do corresponding proofs. Need to figure out - how to exploit abstraction to make terms readable. + how to exploit abstraction to make terms readable. + Conversion of raw to scoped and scoped to raw - is easy if I use impossible + is easy if I use impossible + Added conversion of TypedDB to PHOAS in extra/DeBruijn-agda-list-4.lagda + Next: try adding bidirectional typing to @@ -200,7 +200,7 @@ Tradeoffs: + updated Agda from: Agda version 2.6.0-4654bfb-dirty to: - Agda version 2.6.0-2f2f4f5 + Agda version 2.6.0-2f2f4f5 Now TypedFresh.lagda computes 2+2 in milliseconds (as opposed to failing to compute it in one day). @@ -218,7 +218,7 @@ The following comments were collected on the Agda mailing list. * Nils Anders Danielsson + cites Chlipala, who uses binary parametricity - - http://adam.chlipala.net/cpdt/html/Cpdt.ProgLang.html + - http://adam.chlipala.net/cpdt/html/Cpdt.ProgLang.html - http://adam.chlipala.net/cpdt/html/Intensional.html * Roman @@ -228,7 +228,7 @@ The following comments were collected on the Agda mailing list. + also cites Abel's habilitation - http://www.cse.chalmers.se/~abela/habil.pdf + See his note to the Agda mailing list of 26 June, - "Typed Jigger in vanilla Agda" + "Typed Jigger in vanilla Agda" It points to the following solution. - https://github.com/effectfully/random-stuff/blob/master/TypedJigger.agda diff --git a/README.md b/README.md index 51fad7c9..2d0f3f50 100644 --- a/README.md +++ b/README.md @@ -4,47 +4,13 @@ title: Getting Started permalink: /GettingStarted/ --- - - -[epub]: https://plfa.github.io/out/epub/plfa.epub -[plfa]: http://plfa.inf.ed.ac.uk -[plfa-dev]: https://github.com/plfa/plfa.github.io/archive/dev.zip -[plfa-status]: https://travis-ci.org/plfa/plfa.github.io.svg?branch=dev -[plfa-travis]: https://travis-ci.org/plfa/plfa.github.io -[plfa-calver]: https://img.shields.io/badge/calver-20.07-22bfda -[plfa-latest]: https://github.com/plfa/plfa.github.io/releases/latest -[plfa-master]: https://github.com/plfa/plfa.github.io/archive/master.zip - -[agda]: https://github.com/agda/agda/releases/tag/v2.6.1 -[agda-version]: https://img.shields.io/badge/agda-v2.6.1-blue.svg -[agda-docs-emacs-mode]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html -[agda-docs-emacs-notation]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html#notation-for-key-combinations -[agda-docs-package-system]: https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html#example-using-the-standard-library - -[agda-stdlib-version]: https://img.shields.io/badge/agda--stdlib-v1.3-blue.svg -[agda-stdlib]: https://github.com/agda/agda-stdlib/releases/tag/v1.3 - -[haskell-stack]: https://docs.haskellstack.org/en/stable/README/ -[haskell-ghc]: https://www.haskell.org/ghc/ - -[mononoki]: https://madmalik.github.io/mononoki/ - -[ruby]: https://www.ruby-lang.org/en/documentation/installation/ -[ruby-bundler]: https://bundler.io/#getting-started -[ruby-jekyll]: https://jekyllrb.com/ -[ruby-html-proofer]: https://github.com/gjtorikian/html-proofer - -[kramdown]: https://kramdown.gettalong.org/syntax.html -[pandoc]: https://pandoc.org/installing.html -[epubcheck]: https://github.com/w3c/epubcheck - - [![Calendar Version][plfa-calver]][plfa-latest] [![Build Status][plfa-status]][plfa-travis] [![Agda][agda-version]][agda] [![agda-stdlib][agda-stdlib-version]][agda-stdlib] + ## Dependencies for users You can read PLFA [online][plfa] without installing anything. @@ -146,10 +112,10 @@ It is recommended that you install the font [mononoki][mononoki], and add the fo ``` elisp ;; default to mononoki (set-face-attribute 'default nil - :family "mononoki" - :height 120 - :weight 'normal - :width 'normal) + :family "mononoki" + :height 120 + :weight 'normal + :width 'normal) ``` @@ -174,8 +140,7 @@ You'll see the key sequence of the character in mini buffer. ## Dependencies for developers -PLFA is available as both a website and an EPUB e-book, -both of which can be built on Linux and macOS. +PLFA is available as both a website and an EPUB e-book, both of which can be built on Linux and macOS. PLFA is written in literate Agda with [Kramdown Markdown][kramdown]. ### Building the website @@ -195,7 +160,7 @@ Most recent versions of [Ruby][ruby] should work. The easiest way to install [Je ```bash gem install bundler ``` -You can install the remainder of the dependencies---[Jekyll][ruby-jekyll], [html-proofer][ruby-html-proofer], *etc.*---by running: +You can install the remainder of the dependencies—[Jekyll][ruby-jekyll], [html-proofer][ruby-html-proofer], *etc.*—by running: ```bash bundle install ``` @@ -234,3 +199,37 @@ Once you’ve installed Pandoc, you can build the EPUB by running: make epub ``` The EPUB is written to `out/epub/plfa.epub`. + + + +[epub]: https://plfa.github.io/out/epub/plfa.epub +[plfa]: http://plfa.inf.ed.ac.uk +[plfa-dev]: https://github.com/plfa/plfa.github.io/archive/dev.zip +[plfa-status]: https://travis-ci.org/plfa/plfa.github.io.svg?branch=dev +[plfa-travis]: https://travis-ci.org/plfa/plfa.github.io +[plfa-calver]: https://img.shields.io/badge/calver-20.07-22bfda +[plfa-latest]: https://github.com/plfa/plfa.github.io/releases/latest +[plfa-master]: https://github.com/plfa/plfa.github.io/archive/master.zip + +[agda]: https://github.com/agda/agda/releases/tag/v2.6.1 +[agda-version]: https://img.shields.io/badge/agda-v2.6.1-blue.svg +[agda-docs-emacs-mode]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html +[agda-docs-emacs-notation]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html#notation-for-key-combinations +[agda-docs-package-system]: https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html#example-using-the-standard-library + +[agda-stdlib-version]: https://img.shields.io/badge/agda--stdlib-v1.3-blue.svg +[agda-stdlib]: https://github.com/agda/agda-stdlib/releases/tag/v1.3 + +[haskell-stack]: https://docs.haskellstack.org/en/stable/README/ +[haskell-ghc]: https://www.haskell.org/ghc/ + +[mononoki]: https://madmalik.github.io/mononoki/ + +[ruby]: https://www.ruby-lang.org/en/documentation/installation/ +[ruby-bundler]: https://bundler.io/#getting-started +[ruby-jekyll]: https://jekyllrb.com/ +[ruby-html-proofer]: https://github.com/gjtorikian/html-proofer + +[kramdown]: https://kramdown.gettalong.org/syntax.html +[pandoc]: https://pandoc.org/installing.html +[epubcheck]: https://github.com/w3c/epubcheck diff --git a/courses/tspl/2019/tspl2019.md b/courses/tspl/2019/tspl2019.md index d0ba1af0..842e4154 100644 --- a/courses/tspl/2019/tspl2019.md +++ b/courses/tspl/2019/tspl2019.md @@ -66,7 +66,7 @@ Lectures take place Monday, Wednesday, and Friday in AT 5.07. 7 28 Oct Inference - 30 Oct Untyped + 30 Oct Untyped 1 Nov (no class) @@ -91,7 +91,7 @@ Lectures take place Monday, Wednesday, and Friday in AT 5.07. 11 25 Nov Quantitative (Wen) 27 Nov (no class) - 29 Nov Mock Exam + 29 Nov Mock Exam @@ -162,7 +162,7 @@ practice for the exam and familiarise yourself with exam conditions. * John Reynolds, [Three Approaches to Type Structure][reynolds], _Mathematical Foundations of Software Development_, - LNCS 185, pages 97–138, 1985. + LNCS 185, pages 97–138, 1985. * Henk Barendregt, [Introduction to generalized type systems][barendregt] diff --git a/fix-whitespace.yaml b/fix-whitespace.yaml new file mode 100644 index 00000000..0116cd20 --- /dev/null +++ b/fix-whitespace.yaml @@ -0,0 +1,60 @@ +# This file contains the project-specific settings for `fix-whitespace` a tiny +# but useful tool to +# +# * Removes trailing whitespace. +# * Removes trailing lines containing nothing but whitespace. +# * Ensures that the file ends in a newline character. +# +# By default, fix-whitespace checks every directory under the current working +# directory but no files. This program should be placed under a text-based +# project. +# +# For directories, +# +# 1) excluded-dirs is a black-list of directories, +# 2) included-dirs is a white-list of excluded-dirs +# +# For files, +# +# 3) included-files is a white-list of files, +# 4) excluded-files is a black-list of included-files. +# +# The extended glob pattern can be used to specify file/direcotory names. +# For details, see http://hackage.haskell.org/package/filemanip-0.3.6.3/docs/System-FilePath-GlobPattern.html +# +included-dirs: + - "src" + - "epub" + - "_includes" + - "_layouts" + - "_posts" + - "_sass" + - "_assets" + - "courses" + - "papers" + +excluded-dirs: + - ".stack-work" + - ".git" + - "_build" + - "_site" + - "extra" + - "tmp" + +# Every matched filename is included unless it is matched by excluded-files. +included-files: + - "*.md" + - "*.sh" + - "*.html" + - "*.yml" + - "*.yaml" + - "*.agda-lib" + - "Gemfile" + - "Guardfile" + - "LICENSE" + +excluded-files: + - "*.sed" + - ".DS_Store" + - "Gemfile.lock" + - "Makefile" diff --git a/papers/sbmf/Makefile b/papers/sbmf/Makefile index 4d41c925..d83a221e 100644 --- a/papers/sbmf/Makefile +++ b/papers/sbmf/Makefile @@ -4,17 +4,17 @@ default : PLFA.pdf PLFA.pdf : PLFA.tex PLFA.bib - pdflatex PLFA - bibtex PLFA - pdflatex PLFA - bibtex PLFA - pdflatex PLFA + pdflatex PLFA + bibtex PLFA + pdflatex PLFA + bibtex PLFA + pdflatex PLFA final.zip : PLFA.tex PLFA.bib - zip final.zip agda.sty llncs.cls PLFA.tex PLFA.bib splncsnat.bst figures/plfa-*.png figures/sf-*.png figures/raw.png figures/inherent.png + zip final.zip agda.sty llncs.cls PLFA.tex PLFA.bib splncsnat.bst figures/plfa-*.png figures/sf-*.png figures/raw.png figures/inherent.png clean: - rm -f *.aux *.log *.out *.ptb *.blg *.fdb_latexmk *.agdai *.fls + rm -f *.aux *.log *.out *.ptb *.blg *.fdb_latexmk *.agdai *.fls realclean: clean - rm -f *.glob *.vo *.bbl latex/* PLFA.pdf + rm -f *.glob *.vo *.bbl latex/* PLFA.pdf diff --git a/papers/scp/Makefile b/papers/scp/Makefile index 4d41c925..d83a221e 100644 --- a/papers/scp/Makefile +++ b/papers/scp/Makefile @@ -4,17 +4,17 @@ default : PLFA.pdf PLFA.pdf : PLFA.tex PLFA.bib - pdflatex PLFA - bibtex PLFA - pdflatex PLFA - bibtex PLFA - pdflatex PLFA + pdflatex PLFA + bibtex PLFA + pdflatex PLFA + bibtex PLFA + pdflatex PLFA final.zip : PLFA.tex PLFA.bib - zip final.zip agda.sty llncs.cls PLFA.tex PLFA.bib splncsnat.bst figures/plfa-*.png figures/sf-*.png figures/raw.png figures/inherent.png + zip final.zip agda.sty llncs.cls PLFA.tex PLFA.bib splncsnat.bst figures/plfa-*.png figures/sf-*.png figures/raw.png figures/inherent.png clean: - rm -f *.aux *.log *.out *.ptb *.blg *.fdb_latexmk *.agdai *.fls + rm -f *.aux *.log *.out *.ptb *.blg *.fdb_latexmk *.agdai *.fls realclean: clean - rm -f *.glob *.vo *.bbl latex/* PLFA.pdf + rm -f *.glob *.vo *.bbl latex/* PLFA.pdf diff --git a/src/plfa/acknowledgements.md b/src/plfa/acknowledgements.md index 6df83e23..ec225619 100644 --- a/src/plfa/acknowledgements.md +++ b/src/plfa/acknowledgements.md @@ -57,4 +57,4 @@ For support: * EPSRC Programme Grant EP/K034413/1 * NSF Grant No. 1814460 * Foundation Sciences Mathematiques de Paris (FSMP) - Distinguised Professor Fellowship \ No newline at end of file + Distinguised Professor Fellowship diff --git a/src/plfa/announcements.md b/src/plfa/announcements.md index eb91daab..50d696d7 100644 --- a/src/plfa/announcements.md +++ b/src/plfa/announcements.md @@ -4,4 +4,3 @@ layout : home permalink : /Announcements/ --- - diff --git a/src/plfa/citing.md b/src/plfa/citing.md index 8e4412ed..8ed6c12a 100644 --- a/src/plfa/citing.md +++ b/src/plfa/citing.md @@ -15,13 +15,13 @@ permalink : /Citing/ ### BibTeX - @Book{plfa2020, - author = {Philip Wadler and Wen Kokke and Jeremy G. Siek}, - title = {Programming Language Foundations in {A}gda}, - note = {Available at \url{http://plfa.inf.ed.ac.uk/20.07/}}, - year = 2020, + @Book{plfa2020, + author = {Philip Wadler and Wen Kokke and Jeremy G. Siek}, + title = {Programming Language Foundations in {A}gda}, + note = {Available at \url{http://plfa.inf.ed.ac.uk/20.07/}}, + year = 2020, month = jul, - } + } ## PLFA version 19.08 @@ -35,10 +35,10 @@ permalink : /Citing/ ### BibTeX - @Book{plfa2019, - author = {Philip Wadler and Wen Kokke}, - title = {Programming Language Foundations in {A}gda}, - note = {Available at \url{http://plfa.inf.ed.ac.uk/19.08/}}, - year = 2019, + @Book{plfa2019, + author = {Philip Wadler and Wen Kokke}, + title = {Programming Language Foundations in {A}gda}, + note = {Available at \url{http://plfa.inf.ed.ac.uk/19.08/}}, + year = 2019, month = aug, - } + } diff --git a/src/plfa/part1/Quantifiers.lagda.md b/src/plfa/part1/Quantifiers.lagda.md index ba18f34a..7349cd69 100644 --- a/src/plfa/part1/Quantifiers.lagda.md +++ b/src/plfa/part1/Quantifiers.lagda.md @@ -470,7 +470,7 @@ binary number `b`, there is only one proof of `One b` and similarly for `Can b`. ≡One : ∀{b : Bin} (o o' : One b) → o ≡ o' - + ≡Can : ∀{b : Bin} (cb : Can b) (cb' : Can b) → cb ≡ cb' Many of the alternatives for proving `to∘from` turn out to be tricky. diff --git a/src/plfa/part2/BigStep.lagda.md b/src/plfa/part2/BigStep.lagda.md index eb830b64..db7db342 100644 --- a/src/plfa/part2/BigStep.lagda.md +++ b/src/plfa/part2/BigStep.lagda.md @@ -293,7 +293,7 @@ below. ⟨ subst σ (ƛ N) , ⟨ subst σ (ƛ N) ∎ , ⟨ σ , ⟨ γ≈ₑσ , refl ⟩ ⟩ ⟩ ⟩ ⇓→—↠×≈{Γ}{γ} {σ = σ} {L · M} {V} (⇓-app {N = N} L⇓ƛNδ N⇓V) γ≈ₑσ with ⇓→—↠×≈{σ = σ} L⇓ƛNδ γ≈ₑσ -... | ⟨ _ , ⟨ σL—↠ƛτN , ⟨ τ , ⟨ δ≈ₑτ , ≡ƛτN ⟩ ⟩ ⟩ ⟩ rewrite ≡ƛτN +... | ⟨ _ , ⟨ σL—↠ƛτN , ⟨ τ , ⟨ δ≈ₑτ , ≡ƛτN ⟩ ⟩ ⟩ ⟩ rewrite ≡ƛτN with ⇓→—↠×≈ {σ = ext-subst τ (subst σ M)} N⇓V (λ {x} → ≈ₑ-ext{σ = τ} δ≈ₑτ ⟨ σ , ⟨ γ≈ₑσ , refl ⟩ ⟩ {x}) | β{∅}{subst (exts τ) N}{subst σ M} diff --git a/src/plfa/part2/Confluence.lagda.md b/src/plfa/part2/Confluence.lagda.md index 6d6e617f..9c960b12 100644 --- a/src/plfa/part2/Confluence.lagda.md +++ b/src/plfa/part2/Confluence.lagda.md @@ -221,7 +221,7 @@ The proof is by induction on `M ⇛ N`. * Suppose `L · M ⇛ L′ · M′` because `L ⇛ L′` and `M ⇛ M′`. By the induction hypothesis, we have `L —↠ L′` and `M —↠ M′`. So `L · M —↠ L′ · M` and then `L′ · M —↠ L′ · M′` - because `—↠` is a congruence. + because `—↠` is a congruence. * Suppose `(ƛ N) · M ⇛ N′ [ M′ ]` because `N ⇛ N′` and `M ⇛ M′`. By similar reasoning, we have @@ -451,7 +451,7 @@ par-triangle (papp {L = _ · _} p1 p2) = papp (par-triangle p1) (par-triangle p2 The proof of the triangle property is an induction on `M ⇛ N`. -* Suppose `x ⇛ x`. Clearly `x ⁺ = x`, so `x ⇛ x`. +* Suppose `x ⇛ x`. Clearly `x ⁺ = x`, so `x ⇛ x`. * Suppose `ƛ M ⇛ ƛ N`. By the induction hypothesis we have `N ⇛ M ⁺` and by definition `(λ M) ⁺ = λ (M ⁺)`, so we conclude that `λ N ⇛ λ @@ -619,7 +619,7 @@ and `par-confluence` are based on the notion of complete development by Takahashi (1995) and Pfenning's 1992 technical report about the Church-Rosser theorem. In addition, we consulted Nipkow and Berghofer's mechanization in Isabelle, which is based on an earlier -article by Nipkow (JAR 1996). +article by Nipkow (JAR 1996). ## Unicode diff --git a/style-guide.md b/style-guide.md index cbf3f68e..2da4de57 100644 --- a/style-guide.md +++ b/style-guide.md @@ -2,7 +2,7 @@ Style guide for PLFA ============================ This is based on [the style guide for the Agda standard library](https://github.com/agda/agda-stdlib/blob/master/notes/style-guide.md). -Like it, this is very much a work-in-progress and is not exhaustive. +Like it, this is very much a work-in-progress and is not exhaustive. ## File structure @@ -44,14 +44,14 @@ Like it, this is very much a work-in-progress and is not exhaustive. * If the type of a term does not fit on one line then the subsequent lines of the type should all be indented by two spaces, e.g. ```agda - map-cong₂ : ∀ {a b} {A : Set a} {B : Set b} - → ∀ {f g : A → B} {xs} + map-cong₂ : ∀ {a b} {A : Set a} {B : Set b} + → ∀ {f g : A → B} {xs} → All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs ``` * As can be seen in the example above, function arrows at line breaks - should always go at the beginning of the next line rather than the - end of the line. + should always go at the beginning of the next line rather than the + end of the line. #### Module parameters @@ -85,7 +85,7 @@ Like it, this is very much a work-in-progress and is not exhaustive. ```agda +-comm : Commutative _+_ +-comm zero n = sym (+-identityʳ n) - +-comm (suc m) n = + +-comm (suc m) n = begin suc m + n ≡⟨⟩ diff --git a/travis-build-cache.sh b/travis-build-cache.sh index 113f2a56..339323f6 100755 --- a/travis-build-cache.sh +++ b/travis-build-cache.sh @@ -10,24 +10,24 @@ # - Create JSON request. # body=$(cat .travis.yml \ - | yq w - script "echo 'Done'"\ - | yq d - before_deploy \ - | yq d - deploy \ - | yq p - config \ - | yq w - message "Build cache" \ - | yq w - branch dev \ - | yq w - merge_mode replace \ - | yq p - request -j) + | yq w - script "echo 'Done'"\ + | yq d - before_deploy \ + | yq d - deploy \ + | yq p - config \ + | yq w - message "Build cache" \ + | yq w - branch dev \ + | yq w - merge_mode replace \ + | yq p - request -j) # Send request to Travis. # resp=$(curl -s -X POST \ - -H "Content-Type: application/json" \ - -H "Accept: application/json" \ - -H "Travis-API-Version: 3" \ - -H "Authorization: token $TRAVIS_TOKEN" \ - -d "$body" \ - https://api.travis-ci.org/repo/plfa%2Fplfa.github.io/requests) + -H "Content-Type: application/json" \ + -H "Accept: application/json" \ + -H "Travis-API-Version: 3" \ + -H "Authorization: token $TRAVIS_TOKEN" \ + -d "$body" \ + https://api.travis-ci.org/repo/plfa%2Fplfa.github.io/requests) # Output response. #