diff --git a/.githooks/pre-commit b/.githooks/pre-commit index 6fc6d85b..a724f042 100755 --- a/.githooks/pre-commit +++ b/.githooks/pre-commit @@ -9,7 +9,3 @@ else echo "Checking for whitespace violations..." fix-whitespace --check fi - -# Run the test suite. -echo "Running the test suite..." -make test-offline diff --git a/.gitignore b/.gitignore index 3763cbcf..ef5123cc 100644 --- a/.gitignore +++ b/.gitignore @@ -3,6 +3,13 @@ .agda-stdlib.sed .links-*.sed +## Haskell files +_site/ +_cache/ +stack.yaml.lock +.stack-work/ +dist-newstyle + ## Jekyll files _site/ .sass-cache/ @@ -26,4 +33,5 @@ auto/ ## Misc build files out/ -.versions/ +*.zip +versions/plfa.github.io-web-*/ \ No newline at end of file diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 00000000..0a16f1e5 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "standard-library"] + path = standard-library + url = git@github.com:agda/agda-stdlib.git diff --git a/404.html b/404.html new file mode 100755 index 00000000..c472b4ea --- /dev/null +++ b/404.html @@ -0,0 +1,24 @@ +--- +layout: default +--- + + + +
+

404

+ +

Page not found :(

+

The requested page could not be found.

+
diff --git a/Gemfile b/Gemfile index 70f9fd15..f491af50 100644 --- a/Gemfile +++ b/Gemfile @@ -1,19 +1,8 @@ +# NOTE: the Gemfile is no longer used by the main distribution of PLFA, +# but is still used to build legacy versions 19.07 and 20.08. + source "https://rubygems.org" group :jekyll_plugins do gem 'github-pages' end - -group :development do - gem 'guard' - gem 'guard-shell' - gem 'html-proofer' - # ffi-1.13.1 is broken on macos - # https://github.com/ffi/ffi/issues/791 - gem 'ffi', '~> 1.12.2' -end - -group :epub do - gem 'safe_yaml' - gem 'liquid' -end diff --git a/Guardfile b/Guardfile deleted file mode 100644 index 60551972..00000000 --- a/Guardfile +++ /dev/null @@ -1,9 +0,0 @@ -require 'fileutils' - -guard :shell do - watch(%r{^(.+)\.lagda\.md$}) do |m| - src = m[0] - out = "#{File.dirname(src).sub('src','out')}/#{File.basename(src,'.lagda.md')}.md" - `make #{out}` unless File.basename(src).start_with?('.#') - end -end diff --git a/Makefile b/Makefile index b0999641..f8cbe690 100644 --- a/Makefile +++ b/Makefile @@ -1,273 +1,202 @@ -SHELL := /usr/bin/env bash -AGDA_FILES := $(shell find . -type f -and \( -path './src/*' -or -path './courses/*' \) -and -name '*.lagda.md') -AGDAI_FILES := $(shell find . -type f -and \( -path './src/*' -or -path './courses/*' \) -and -name '*.agdai') -MARKDOWN_FILES := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA_FILES)))) -PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST)))) -PANDOC := pandoc -EPUBCHECK := epubcheck -RUBY := ruby -GEM := $(RUBY) -S gem -BUNDLE := $(RUBY) -S bundle -JEKYLL := $(BUNDLE) exec jekyll -HTMLPROOFER := $(BUNDLE) exec htmlproofer -LUA_FILES := $(shell find . -type f -and -path '*/epub/*' -and -name '*.lua') -RELEASE_VERSIONS := 19.08 20.07 -RELEASES := $(addsuffix /,$(RELEASE_VERSIONS)) -LATEST_VERSION := $(word $(words $(RELEASE_VERSIONS)),$(RELEASE_VERSIONS)) +################################################################################# +# Configuration +################################################################################# -ifeq ($(AGDA_STDLIB_VERSION),) -AGDA_STDLIB_URL := https://agda.github.io/agda-stdlib/ -else -AGDA_STDLIB_URL := https://agda.github.io/agda-stdlib/v$(AGDA_STDLIB_VERSION)/ +SITE_DIR := _site +CACHE_DIR := _cache +TMP_DIR := $(CACHE_DIR)/tmp + + +################################################################################# +# Setup Git Hooks +################################################################################# + +.PHONY: init +init: setup-check-fix-whitespace setup-check-htmlproofer + git config core.hooksPath .githooks + + +################################################################################# +# Build PLFA site +################################################################################# + +.PHONY: build +build: $(SITE_DIR) + +$(SITE_DIR): authors contributors css courses hs posts public src templates + stack build && stack exec site build + + +################################################################################# +# Test generated site with HTMLProofer +################################################################################# + +.PHONY: test +test: setup-install-htmlproofer $(SITE_DIR) + cd $(SITE_DIR) && htmlproofer \ + --check-html \ + --disable-external \ + --report-invalid-tags \ + --report-missing-names \ + --report-script-embeds \ + --report-missing-doctype \ + --report-eof-tags \ + --report-mismatched-tags \ + --check-img-http \ + --check-opengraph \ + . + +################################################################################# +# Test generated EPUB with EPUBCheck +################################################################################# + +.PHONY: test-epub +test-epub: setup-check-epubcheck $(SITE_DIR)/plfa.epub + epubcheck $(SITE_DIR)/plfa.epub + + +################################################################################# +# Automatically rebuild the site on changes, and start a preview server +################################################################################# + +.PHONY: watch +watch: + stack build && stack exec site watch + + +################################################################################# +# Update contributor metadata in `contributors/` +################################################################################# + +.PHONY: update-contributors +update-contributors: + stack build && stack exec update-contributors + + +################################################################################# +# Clean up and remove the cache +################################################################################# + +.PHONY: clean +clean: + stack build && stack exec site clean + + +################################################################################# +# List targets in Makefile +################################################################################# + +.PHONY: list +list: + @$(MAKE) -pRrq -f $(lastword $(MAKEFILE_LIST)) : 2>/dev/null | awk -v RS= -F: '/^# File/,/^# Finished Make data base/ {if ($$1 !~ "^[#.]") {print $$1}}' | sort | egrep -v -e '^[^[:alnum:]]' -e '^$@$$' + + +################################################################################# +# Setup dependencies +################################################################################# + +.PHONY: setup-check-stack +setup-check-stack: +ifeq (,$(wildcard $(shell which stack))) + @echo "The command you called requires the Haskell Tool Stack" + @echo "See: https://docs.haskellstack.org/en/stable/install_and_upgrade/" + @exit 1 endif +.PHONY: setup-check-npm +setup-check-npm: +ifeq (,$(wildcard $(shell which npm))) + @echo "The command you called requires the Node Package Manager" + @echo "See: https://www.npmjs.com/get-npm" + @exit 1 +endif + +.PHONY: setup-check-gem +setup-check-gem: +ifeq (,$(wildcard $(shell which gem))) + @echo "The command you called requires the RubyGems Package Manager" + @echo "See: https://www.ruby-lang.org/en/documentation/installation/" + @exit 1 +endif + +.PHONY: setup-check-fix-whitespace +setup-check-fix-whitespace: setup-check-stack +ifeq (,$(wildcard $(shell which fix-whitespace))) + @echo "The command you called requires fix-whitespace" + @echo "Run: git clone https://github.com/agda/fix-whitespace" + @echo " cd fix-whitespace/" + @echo " stack install --stack-yaml stack-8.8.3.yaml" +endif + +.PHONY: setup-check-epubcheck +setup-check-epubcheck: +ifeq (,$(wildcard $(shell which epubcheck))) + @echo "The command you called requires EPUBCheck" + @echo "See: https://github.com/w3c/epubcheck" +endif + +.PHONY: setup-install-htmlproofer +setup-install-htmlproofer: setup-check-gem +ifeq (,$(wildcard $(shell which htmlproofer))) + @echo "Installing HTMLProofer..." + gem install html-proofer +endif + +.PHONY: setup-install-bundler +setup-install-bundler: setup-check-gem +ifeq (,$(wildcard $(shell which bundle))) + @echo "Installing Ruby Bundler..." + gem install bundle +endif + + +################################################################################# +# Build legacy versions of website using Jekyll +################################################################################# + +LEGACY_VERSIONS := 19.08 20.07 +LEGACY_VERSION_DIRS := $(addprefix versions/,$(addsuffix /,$(LEGACY_VERSIONS))) + +legacy-versions: setup-install-bundle $(LEGACY_VERSION_DIRS) + ifeq ($(shell sed --version >/dev/null 2>&1; echo $$?),1) SEDI := sed -i "" else SEDI := sed -i endif - -# Configure the repository to use .githooks -init: - git config core.hooksPath .githooks - - -# Build PLFA web version and test links -default: test - - -# Start Jekyll server with --incremental -serve: - $(JEKYLL) serve --incremental - -# Start detached Jekyll server -server-start: - $(JEKYLL) serve --no-watch --detach - -# Stop detached Jekyll server -server-stop: - pkill -f jekyll - -.phony: serve server-start server-stop - - -# Build PLFA web version using Jekyll -build: $(MARKDOWN_FILES) - $(JEKYLL) build - -# Build PLFA web version using Jekyll with --incremental -build-incremental: $(MARKDOWN_FILES) - $(JEKYLL) build --incremental - -# Download PLFA web releases -build-history: latest/ $(RELEASES) - -latest/: $(addprefix .versions/plfa.github.io-web-,$(addsuffix /,$(LATEST_VERSION))) - cd $< \ - && $(JEKYLL) clean \ - && $(JEKYLL) build --destination '../../latest' --baseurl '/latest' - -# Download PLFA web release and build it under the relevant folder -define build_release +define build_legacy_version version := $(1) out := $(addsuffix /,$(1)) url := $(addprefix https://github.com/plfa/plfa.github.io/archive/web-,$(addsuffix .zip,$(1))) -tmp_zip := $(addprefix .versions/plfa.github.io-web-,$(addsuffix .zip,$(1))) -tmp_dir := $(addprefix .versions/plfa.github.io-web-,$(addsuffix /,$(1))) +tmp_zip := $(addprefix versions/plfa.github.io-web-,$(addsuffix .zip,$(1))) +tmp_dir := $(addprefix versions/plfa.github.io-web-,$(addsuffix /,$(1))) baseurl := $(addprefix /,$(1)) -$$(tmp_zip): tmp_zip = $(addprefix .versions/plfa.github.io-web-,$(addsuffix .zip,$(1))) +$$(tmp_zip): tmp_zip = $(addprefix versions/plfa.github.io-web-,$(addsuffix .zip,$(1))) $$(tmp_zip): url = $(addprefix https://github.com/plfa/plfa.github.io/archive/web-,$(addsuffix .zip,$(1))) $$(tmp_zip): - @mkdir -p .versions/ - wget -c $$(url) -O $$(tmp_zip) + @mkdir -p versions/ + @wget -c $$(url) -O $$(tmp_zip) $$(tmp_dir): version = $(1) -$$(tmp_dir): tmp_dir = $(addprefix .versions/plfa.github.io-web-,$(addsuffix /,$(1))) -$$(tmp_dir): tmp_zip = $(addprefix .versions/plfa.github.io-web-,$(addsuffix .zip,$(1))) +$$(tmp_dir): tmp_dir = $(addprefix versions/plfa.github.io-web-,$(addsuffix /,$(1))) +$$(tmp_dir): tmp_zip = $(addprefix versions/plfa.github.io-web-,$(addsuffix .zip,$(1))) $$(tmp_dir): $$(tmp_zip) - yes | unzip -qq $$(tmp_zip) -d .versions/ - $(SEDI) "s/branch: dev/branch: dev-$$(version)/" $$(addsuffix _config.yml,$$(tmp_dir)) + @yes | unzip -qq $$(tmp_zip) -d versions/ + @$(SEDI) "s/branch: dev/branch: dev-$$(version)/" $$(addsuffix _config.yml,$$(tmp_dir)) -$$(out): out = $(addsuffix /,$(1)) -$$(out): url = $(addprefix https://github.com/plfa/plfa.github.io/archive/web-,$(addsuffix .zip,$(1))) -$$(out): tmp_dir = $(addprefix .versions/plfa.github.io-web-,$(addsuffix /,$(1))) -$$(out): baseurl = $(addprefix /,$(1)) -$$(out): $$(tmp_dir) - cd $$(tmp_dir) \ +versions/$$(out): out = $(addsuffix /,$(1)) +versions/$$(out): url = $(addprefix https://github.com/plfa/plfa.github.io/archive/web-,$(addsuffix .zip,$(1))) +versions/$$(out): tmp_dir = $(addprefix versions/plfa.github.io-web-,$(addsuffix /,$(1))) +versions/$$(out): baseurl = $(addprefix /,$(1)) +versions/$$(out): $$(tmp_dir) + @echo "source \"https://rubygems.org\"\n\ngroup :jekyll_plugins do\n gem 'github-pages'\nend" > $$(tmp_dir)/Gemfile + @cd $$(tmp_dir) \ && rm -rf _posts \ - && $(JEKYLL) clean \ - && $(JEKYLL) build --destination '../../$$(out)' --baseurl '$$(baseurl)' + && bundle install \ + && bundle exec jekyll clean \ + && bundle exec jekyll build --destination '../$$(out)' --baseurl '$$(baseurl)' endef -# Incorporate previous releases of PLFA web version -$(foreach release_version,$(RELEASE_VERSIONS),$(eval $(call build_release,$(release_version)))) - -# Convert literal Agda to Markdown using highlight.sh -define AGDA_template -in := $(1) -out := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(1)))) -$$(out) : in = $(1) -$$(out) : out = $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(1)))) -$$(out) : $$(in) - @echo "Processing $$(subst ./,,$$(in))" - @mkdir -p out/ -ifeq (,$$(findstring courses/,$$(in))) - ./highlight.sh $$(subst ./,,$$(in)) --include-path=src/ -else -# Fix links to the file itself (out/ to out/) - ./highlight.sh $$(subst ./,,$$(in)) --include-path=src/ --include-path=$$(subst ./,,$$(dir $$(in))) -endif -endef - -$(foreach agda,$(AGDA_FILES),$(eval $(call AGDA_template,$(agda)))) - -.phony: build build-incremental - - -# Test links using htmlproofer -test: build - $(HTMLPROOFER) '_site' - -# Test local links using htmlproofer -test-offline: build - $(HTMLPROOFER) '_site' --disable-external - -# Test local links for stability under different base URLs -test-stable-offline: $(MARKDOWN_FILES) - $(JEKYLL) clean - $(JEKYLL) build --destination '_site/stable' --baseurl '/stable' - $(HTMLPROOFER) '_site' --disable-external - -.phony: test test-offline test-stable-offline - - -# Build EPUB using Pandoc -epub: out/epub/plfa.epub - -# Test EPUB using EPUBCheck -epubcheck: out/epub/plfa.epub - $(EPUBCHECK) out/epub/plfa.epub - -out/epub/plfa.epub: $(AGDA_FILES) $(LUA_FILES) epub/main.css out/epub/acknowledgements.md - @mkdir -p out/epub/ - $(PANDOC) --strip-comments \ - --css=epub/main.css \ - --epub-embed-font='assets/fonts/mononoki.woff' \ - --epub-embed-font='assets/fonts/FreeMono.woff' \ - --epub-embed-font='assets/fonts/DejaVuSansMono.woff' \ - --lua-filter epub/include-files.lua \ - --lua-filter epub/rewrite-links.lua \ - --lua-filter epub/rewrite-html-ul.lua \ - --lua-filter epub/default-code-class.lua -M default-code-class=agda \ - --standalone \ - --fail-if-warnings \ - --toc --toc-depth=2 \ - --epub-chapter-level=2 \ - -o "$@" \ - epub/index.md - -out/epub/acknowledgements.md: src/plfa/acknowledgements.md _config.yml - @mkdir -p out/epub/ - $(BUNDLE) exec ruby epub/render-liquid-template.rb _config.yml $< $@ - -.phony: epub epubcheck - - -# Clean auxiliary files -clean: - rm -f .agda-stdlib.sed .links-*.sed out/epub/acknowledgements.md - rm -rf .versions -ifneq ($(strip $(AGDAI_FILES)),) - rm $(AGDAI_FILES) -endif - -# Clean generated files -clobber: clean - $(JEKYLL) clean - rm -rf out/ - rm -rf latest/ $(RELEASES) - -.phony: clean clobber - - -# Setup Travis -travis-setup:\ - travis-install-agda\ - travis-install-agda-stdlib\ - travis-install-acknowledgements - -.phony: travis-setup - - -# Setup Agda - -travis-install-agda:\ - $(HOME)/.local/bin/agda\ - $(HOME)/.agda/defaults\ - $(HOME)/.agda/libraries - -$(HOME)/.agda/defaults: - echo "standard-library" >> $(HOME)/.agda/defaults - echo "plfa" >> $(HOME)/.agda/defaults - -$(HOME)/.agda/libraries: - echo "$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/standard-library.agda-lib" >> $(HOME)/.agda/libraries - echo "$(PLFA_DIR)/plfa.agda-lib" >> $(HOME)/.agda/libraries - -$(HOME)/.local/bin/agda: - curl -L https://github.com/agda/agda/archive/v$(AGDA_VERSION).zip\ - -o $(HOME)/agda-$(AGDA_VERSION).zip - unzip -qq $(HOME)/agda-$(AGDA_VERSION).zip -d $(HOME) - cd $(HOME)/agda-$(AGDA_VERSION);\ - stack install --stack-yaml=stack-$(GHC_VERSION).yaml - -travis-uninstall-agda: - rm -rf $(HOME)/agda-$(AGDA_VERSION)/ - rm -f $(HOME)/.local/bin/agda - rm -f $(HOME)/.local/bin/agda-mode - -travis-reinstall-agda: travis-uninstall-agda travis-install-agda - -.phony: travis-install-agda travis-uninstall-agda travis-reinstall-agda - - -# Setup Agda Standard Library - -travis-install-agda-stdlib: $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src - -$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src: - curl -L https://github.com/agda/agda-stdlib/archive/v$(AGDA_STDLIB_VERSION).zip\ - -o $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION).zip - unzip -qq $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION).zip -d $(HOME) - mkdir -p $(HOME)/.agda - -travis-uninstall-agda-stdlib: - rm $(HOME)/.agda/defaults - rm $(HOME)/.agda/libraries - rm -rf $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/ - -travis-reinstall-agda-stdlib: travis-uninstall-agda-stdlib travis-install-agda-stdlib - -.phony: travis-install-agda-stdlib travis-uninstall-agda-stdlib travis-reinstall-agda-stdlib epub - - -# Setup Acknowledgements - -travis-install-acknowledgements: $(HOME)/.local/bin/acknowledgements - -$(HOME)/.local/bin/acknowledgements: - curl -L https://github.com/plfa/acknowledgements/archive/master.zip\ - -o $(HOME)/acknowledgements-master.zip - unzip -qq $(HOME)/acknowledgements-master.zip -d $(HOME) - cd $(HOME)/acknowledgements-master;\ - stack install - -travis-uninstall-acknowledgements: - rm -rf $(HOME)/acknowledgements-master/ - rm $(HOME)/.local/bin/acknowledgements - -travis-reinstall-acknowledgements: travis-uninstall-acknowledgements travis-reinstall-acknowledgements - -.phony: travis-install-acknowledgements travis-uninstall-acknowledgements travis-reinstall-acknowledgements +$(foreach legacy_version,$(LEGACY_VERSIONS),$(eval $(call build_legacy_version,$(legacy_version)))) diff --git a/README.md b/README.md index 607e53cc..a1fb9ab3 100644 --- a/README.md +++ b/README.md @@ -1,10 +1,13 @@ --- -layout: page -title: Getting Started -permalink: /GettingStarted/ +layout : page +title : Getting Started +prev : /Preface/ +permalink : /GettingStarted/ +next : /Naturals/ --- + [![Calendar Version][plfa-calver]][plfa-latest] [![Build Status][plfa-status]][plfa-travis] [![Agda][agda-version]][agda] @@ -12,19 +15,46 @@ permalink: /GettingStarted/ ## Dependencies for users +You can read PLFA [online][plfa] without installing anything. However, if you wish to interact with the code or complete the exercises, you need several things: -You can read PLFA [online][plfa] without installing anything. -However, if you wish to interact with the code or complete the exercises, you need several things: - - - [Agda][agda] - - [Agda standard library][agda-stdlib] - - [PLFA][plfa-dev] + - [Stack](#install-the-haskell-tool-stack) + - [Git](#install-git) + - [Agda](#install-agda-using-stack) + - [Agda standard library](#install-plfa-and-the-agda-standard-library) + - [PLFA](#install-plfa-and-the-agda-standard-library) PLFA is tested against specific versions of Agda and the standard library, which are shown in the badges above. Agda and the standard library change rapidly, and these changes often break PLFA, so using older or newer versions usually causes problems. -### Installing Agda using Stack +There are several versions of Agda and its standard library online. If you are using a package manager, like Homebrew or Debian apt, the version of Agda available there may be out-of date. Furthermore, Agda is under active development, so if you install the development version from the GitHub, you might find the developers have introduced changes which break the code here. Therefore, it’s important to have the specific versions of Agda and the standard library shown above. -The easiest way to install any specific version of Agda is using [Stack][haskell-stack]. You can get the required version of Agda from GitHub, either by cloning the repository and switching to the correct branch, or by downloading [the zip archive][agda]: + +### On macOS: Install the XCode Command Line Tools +On macOS, you’ll need to install the [XCode Command Line Tools][xcode]. For most versions of macOS, you can install these by running the following command: +```bash +xcode-select --install +``` + +### Install the Haskell Tool Stack +Agda is written in Haskell, so to install it we’ll need the *Haskell Tool Stack*, or *Stack* for short. Stack is a program for managing different Haskell compilers and packages: + +- *On UNIX and macOS.* Your package manager has a package for Stack, that’s probably your easiest option. For instance, Homebrew on macOS and APT on Debian offer the “haskell-stack” package. Otherwise, you can follow the instructions on [the Stack website][haskell-stack]. Usually, Stack installs binaries at “~/.local/bin”. Please ensure this is on your PATH, by including the following in your shell configuration, e.g., in `~/.bash_profile`: + ```bash + export PATH="${HOME}/.local/bin:${PATH}" + ``` + Finally, ensure that you’ve got the latest version of Stack, by running: + ```bash + stack upgrade + ``` + +- *On Windows.* There is a Windows installer on [the Stack website][haskell-stack]. + + +### Install Git +If you do not already have Git installed, see [the Git downloads page][git]. + + +### Install Agda using Stack +The easiest way to install a *specific version* of Agda is using [Stack][haskell-stack]. You can get the required version of Agda from GitHub, either by cloning the repository and switching to the correct branch, or by downloading [the zip archive][agda]: ```bash git clone https://github.com/agda/agda.git cd agda @@ -34,45 +64,147 @@ To install Agda, run Stack from the Agda source directory: ```bash stack install --stack-yaml stack-8.8.3.yaml ``` -If you want Stack to use you system installation of GHC, you can pass the `--system-ghc` flag and select the appropriate `stack-*.yaml` file. For instance, if you have GHC 8.2.2 installed, run: +*This step will take a long time and a lot of memory to complete.* + +#### Using an existing installation of GHC +Stack is perfectly capable of installing and managing versions of the [Glasgow Haskell Compiler][haskell-ghc] for you. However, if you already have a copy of GHC installed, and you want Stack to use your system installation, you can pass the `--system-ghc` flag and select the appropriate “stack-*.yaml” file. For instance, if you have GHC 8.2.2 installed, run: ```bash stack install --system-ghc --stack-yaml stack-8.2.2.yaml ``` -### Installing the Standard Library and PLFA +#### Check if Agda was installed correctly +If you’d like, you can test to see if you’ve installed Agda correctly. Create a file called “hello.agda” with these lines: +```agda +data Greeting : Set where + hello : Greeting -You can get the required version of the Agda standard library from GitHub, either by cloning the repository and switching to the correct branch, or by downloading [the zip archive][agda-stdlib]: +greet : Greeting +greet = hello +``` +From a command line, change to the same directory where your “hello.agda” file is located. Then run: ```bash -git clone https://github.com/agda/agda-stdlib.git +agda -v 2 hello.agda +``` +You should see a short message like the following, but no errors: +``` +Checking hello (/path/to/hello.agda). +Finished hello. +``` + + +### Install PLFA and the Agda standard library +You can get the latest version of Programming Language Foundations in Agda from GitHub, either by cloning the repository, or by downloading [the zip archive][plfa-dev]: +```bash +git clone --recurse-submodules https://github.com/plfa/plfa.github.io plfa +``` +PLFA ships with the required version of the Agda standard library, so if you cloned with the `--recurse-submodules` flag, you’ve already got, in the “standard-library” directory! + +If you forgot to add the `--recurse-submodules` flag, no worries, we can fix that! +```bash +cd plfa/ +git submodule update --recursive +``` +If you obtained PLFA by downloading the zip archive, you can get the required version of the Agda standard library from GitHub. You can either clone the repository and switch to the correct branch, or you can download the [the zip archive][agda-stdlib]: +```bash +git clone https://github.com/agda/agda-stdlib.git agda-stdlib cd agda-stdlib git checkout v1.3 ``` -You can get the latest version of Programming Language Foundations in Agda from GitHub, either by cloning the repository, or by downloading [the zip archive][plfa-dev]: -```bash -git clone https://github.com/plfa/plfa.github.io +Finally, we need to let Agda know where to find the Agda standard library. +You'll need the path where you installed the standard library, which we’ll refer to as “AGDA_STDLIB”. Check to see that the file “AGDA_STDLIB/standard-library.agda-lib” exists. +You will need to create two configuration files in “AGDA_DIR”. On UNIX and macOS, “AGDA_DIR” defaults to “~/.agda”. On Windwos, “AGDA_DIR” usually defaults to “%AppData%\agda”, where “%AppData%” usually defaults to “C:\Users\USERNAME\AppData\Roaming”. + +- If the “AGDA_DIR” directory does not already exist, create it. +- In “AGDA_DIR”, create a plain-text file called “libraries” containing the path “AGDA_STDLIB/standard-library.agda-lib”. This lets Agda know that an Agda library called “standard-library” is available, at the path “AGDA_STDLIB”. +- In “AGDA_DIR”, create a plain-text file called “defaults” containing *just* the line “standard-library”. + +More information about placing the standard libraries is available from [the Library Management page][agda-docs-package-system] of the Agda documentation. + +It is possible to set up PLFA as an Agda library as well. If you want to complete the exercises found in the “courses” folder, or to import modules from the book, you need to do this. To do so, add the path to “plfa.agda-lib” to “~/.agda/libraries” and add “plfa” to “~/.agda/defaults”, each on a line of their own. + +#### Check if the Agda standard library was installed correctly +If you’d like, you can test to see if you’ve installed the Agda standard library correctly. Create a file called “nats.agda” with these lines: +```agda +open import Data.Nat + +ten : ℕ +ten = 10 ``` -Finally, we need to let Agda know where to find the standard library. For this, you can follow the instructions [here][agda-docs-package-system]. +(Note that the ℕ is a Unicode character, not a plain capital N. You should be able to just copy-and-paste it from this page into your file.) -It is possible to set up PLFA as an Agda library as well. If you want to complete the exercises found in the `courses` folder, or to import modules from the book, you need to do this. To do so, add the path to `plfa.agda-lib` to `~/.agda/libraries` and add `plfa` to `~/.agda/defaults`, both on lines of their own. +From a command line, change to the same directory where your “nats.agda” file is located. Then run: +```bash +agda -v 2 nats.agda +``` +You should see a several lines describing the files which Agda loads while checking your file, but no errors: +``` +Checking nats (/path/to/nats.agda). +Loading Agda.Builtin.Equality (…). +… +Loading Data.Nat (…). +Finished nats. +``` -## Setting up and using Emacs +## Setting up an editor for Agda -The recommended editor for Agda is Emacs with `agda-mode`. Agda ships with `agda-mode`, so if you’ve installed Agda, all you have to do to configure `agda-mode` is run: +### Emacs +The recommended editor for Agda is Emacs. To install Emacs: + + - *On UNIX*, the version of Emacs in your repository is probably fine as long as it is fairly recent. There are also links to the most recent release on the [GNU Emacs downloads page][emacs]. + + - *On MacOS*, [Aquamacs][aquamacs] is probably the preferred version of Emacs, but GNU Emacs can also be installed via Homebrew or MacPorts. See the [GNU Emacs downloads page][emacs] for instructions. + + - *On Windows*. See the [GNU Emacs downloads page][emacs] for instructions. + +Make sure that you are able to open, edit, and save text files with your installation. The [tour of Emacs][emacstour] page on the GNU Emacs site describes how to access the tutorial within your Emacs installation. + +Agda ships with the editor support for Emacs built-in, so if you’ve installed Agda, all you have to do to configure Emacs is run: ```bash agda-mode setup +agda-mode compile +``` +If you are already an Emacs user and have customized your setup, you may want to note the configuration which the `setup` appends to your `.emacs` file, and integrate it with your own preferred setup. + +#### Check if “agda-mode” was installed correctly +Open the `nats.agda` file you created earlier, and load and type-check the file by typing [`C-c C-l`][agda-docs-emacs-notation]. + +#### Auto-loading “agda-mode” in Emacs +Since version 2.6.0, Agda has had support for literate editing with Markdown, using the “.lagda.md” extension. One issue is that Emacs will default to Markdown editing mode for files with a “.md” suffix. In order to have “agda-mode” automatically loaded whenever you open a file ending with “.agda” or “.lagda.md”, add the following line to your Emacs configuration file: +```elisp +;; auto-load agda-mode for .agda and .lagda.md +(setq auto-mode-alist + (append + '(("\\.agda\\'" . agda2-mode) + ("\\.lagda.md\\'" . agda2-mode)) + auto-mode-alist)) +``` +If you already have settings which change your “auto-mode-alist” in your configuration, put these *after* the ones you already have or combine them if you are comfortable with Emacs Lisp. The configuration file for Emacs is normally located in “~/.emacs” or “~/.emacs.d/init.el”, but Aquamacs users might need to move their startup settings to the “Preferences.el” file in “~/Library/Preferences/Aquamacs Emacs/Preferences”. + +#### Optional: using the “mononoki” font with Emacs +Agda uses Unicode characters for many key symbols, and it is important that the font which you use to view and edit Agda programs shows these symbols correctly. The most important part is that the font you use has good Unicode support, so while we recommend [mononoki][font-mononoki], fonts such as [Source Code Pro][font-sourcecodepro], [DejaVu Sans Mono][font-dejavusansmono], and [FreeMono][font-freemono] are all good alternatives. + +You can download and install mononoki directly from [GitHub][mononoki]. For most systems, installing a font is merely a matter of clicking the downloaded “.otf” or “.ttf” file. If your package manager offers a package for mononoki, that might be easier. For instance, Homebrew on macOS offers the “font-mononoki” package, and APT on Debian offers the [“fonts-mononoki” package][font-mononoki-debian]. To configure Emacs to use mononoki as its default font, add the following to the end of your Emacs configuration file: +``` elisp +;; default to mononoki +(set-face-attribute 'default nil + :family "mononoki" + :height 120 + :weight 'normal + :width 'normal) ``` +#### Using “agda-mode” in Emacs To load and type-check the file, use [`C-c C-l`][agda-docs-emacs-notation]. -Agda is edited interactively, using [“holes”][agda-docs-holes], which are bits of the program that are not yet filled in. If you use a question mark as an expression, and load the buffer using `C-c C-l`, Agda replaces the question mark with a hole. There are several things you can to while the cursor is in a hole: +Agda is edited interactively, using [“holes”][agda-docs-holes], which are bits of the program that are not yet filled in. If you use a question mark as an expression, and load the buffer using “C-c C-l”, Agda replaces the question mark with a hole. There are several things you can to while the cursor is in a hole: -- `C-c C-c x`: **c**ase split on variable x -- `C-c C-space`: fill in hole -- `C-c C-r`: **r**efine with constructor -- `C-c C-a`: **a**utomatically fill in hole -- `C-c C-,`: goal type and context -- `C-c C-.`: goal type, context, and inferred type + - `C-c C-c x`: **c**ase split on variable x + - `C-c C-space`: fill in hole + - `C-c C-r`: **r**efine with constructor + - `C-c C-a`: **a**utomatically fill in hole + - `C-c C-,`: goal type and context + - `C-c C-.`: goal type, context, and inferred type See [the emacs-mode docs][agda-docs-emacs-mode] for more details. @@ -86,47 +218,40 @@ If you want to see messages beside rather than below your Agda code, you can do Now, error messages from Agda will appear next to your file, rather than squished beneath it. +#### Entering Unicode characters in Emacs with “agda-mode” +When you write Agda code, you will need to insert characters which are not found on standard keyboards. Emacs “agda-mode” makes it easier to do this by defining character translations: when you enter certain sequences of ordinary characters (the kind you find on any keyboard), Emacs will replace them in your Agda file with the corresponding special character. -### Auto-loading `agda-mode` in Emacs - -Since version 2.6.0, Agda has support for literate editing with Markdown, using the `.lagda.md` extension. One side-effect of this extension is that most editors default to Markdown editing mode, whereas -In order to have `agda-mode` automatically loaded whenever you open a file ending with `.agda` or `.lagda.md`, put the following on your Emacs configuration file: -```elisp -(setq auto-mode-alist - (append - '(("\\.agda\\'" . agda2-mode) - ("\\.lagda.md\\'" . agda2-mode)) - auto-mode-alist)) +For example, we can add a comment line to one of the “.agda” test files. Let's say we want to add a comment line that reads: ``` - -(The configuration file for Emacs is normally located in `~/.emacs` or `~/.emacs.d/init.el`, but Aquamacs users might need to move their startup settings to the `Preferences.el` file in `~/Library/Preferences/Aquamacs Emacs/Preferences`.) - - -### Using mononoki in Emacs - -It is recommended that you install the font [mononoki][mononoki], and add the following to the end of your emacs configuration file at `~/.emacs`: - -``` elisp -;; default to mononoki -(set-face-attribute 'default nil - :family "mononoki" - :height 120 - :weight 'normal - :width 'normal) +{- I am excited to type ∀ and → and ≤ and ≡ !! -} ``` +The first few characters are ordinary, so we would just type them as usual: +``` +{- I am excited to type +``` +But after that last space, we do not find ∀ on the keyboard. The code for this character is the four characters `\all`, so we type those four characters, and when we finish, Emacs will replace them with what we want: +``` +{- I am excited to type ∀ +``` +We can continue with the codes for the other characters. Sometimes the characters will change as we type them, because a prefix of our character's code is the code of another character. This happens with the arrow, whose code is `\->`. After typing `\-` we see: +``` +{- I am excited to type ∀ and +``` +because the code `\-` corresponds to a hyphen of a certain width. When we add the `>`, the `­` becomes `→`! The code for `≤` is `\<=`, and the code for `≡` is `\==`. +``` +{- I am excited to type ∀ and → and ≤ and ≡ +``` +Finally the last few characters are ordinary again, +``` +{- I am excited to type ∀ and → and ≤ and ≡ !! -} +``` +If you're having trouble typing the Unicode characters into Emacs, the end of each chapter should provide a list of the Unicode characters introduced in that chapter. - -### Unicode characters - -If you're having trouble typing the Unicode characters into Emacs, the end of each chapter should provide a list of the unicode characters introduced in that chapter. - -`agda-mode` and emacs have a number of useful commands. Two of them are especially useful when you solve exercises. - -For a full list of supported characters, use `agda-input-show-translations` with: +Emacs with “agda-mode” offers a number of useful commands, and two of them are especially useful when it comes to working with Unicode characters. For a full list of supported characters, use “agda-input-show-translations” with: M-x agda-input-show-translations -All the supported characters in `agda-mode` are shown. +All the supported characters in “agda-mode” are shown. If you want to know how you input a specific Unicode character in agda file, move the cursor onto the character and type the following command: @@ -136,86 +261,60 @@ You'll see the key sequence of the character in mini buffer. ## Dependencies for developers +PLFA is written in literate Agda with [Pandoc Markdown][pandoc]. +PLFA is available as both a website and an EPUB e-book, both of which can be built on UNIX and macOS. +Finally, to help developers avoid common mistakes, we provide a set of Git hooks. -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 and e-book +If you’d like to build the web version of PLFA locally, [Stack](#install-the-haskell-tool-stack) is all you need! PLFA is built using [Hakyll][hakyll], a Haskell library for building static websites. We’ve setup a Makefile to help you run common tasks. For instance, to build PLFA, run: +```bash +make build +``` +If you’d like to serve PLFA locally, rebuilding the website when any of the source files are changed, run: +```bash +make watch +``` +The Makefile offers more than just building and watching, it also offers the following useful options: +``` +build # Build PLFA +watch # Build and serve PLFA, monitor for changes and rebuild +test # Test web version for broken links, invalid HTML, etc. +test-epub # Test EPUB for compliance to the EPUB3 standard +clean # Clean PLFA build +init # Setup the Git hooks (see below) +update-contributors # Pull in new contributors from GitHub to contributors/ +list # List all build targets +``` +For completeness, the Makefile also offers the following options, but you’re unlikely to need these: +``` +legacy-versions # Build legacy versions of PLFA +setup-install-bundler # Install Ruby Bundler (needed for ‘legacy-versions’) +setup-install-htmlproofer # Install HTMLProofer (needed for ‘test’ and Git hooks) +setup-check-fix-whitespace # Check to see if fix-whitespace is installed (needed for Git hooks) +setup-check-epubcheck # Check to see if epubcheck is installed (needed for EPUB tests) +setup-check-gem # Check to see if RubyGems is installed +setup-check-npm # Check to see if the Node Package Manager is installed +setup-check-stack # Check to see if the Haskell Tool Stack is installed +``` +The [EPUB version][epub] of the book is built as part of the website, since it’s hosted on the website. ### Git hooks - The repository comes with several Git hooks: 1. The [fix-whitespace][fix-whitespace] program is run to check for whitespace violations. 2. The test suite is run to check if everything type checks. -You can install these Git hooks by calling `make init`. +You can install these Git hooks by calling “make init”. You can install [fix-whitespace][fix-whitespace] by running: ```bash git clone https://github.com/agda/fix-whitespace cd fix-whitespace/ stack install --stack-yaml stack-8.8.3.yaml ``` -If you want Stack to use your system installation of GHC, you can pass the `--system-ghc` flag and select the appropriate `stack-*.yaml` file, like when installing [Agda](#installing-agda-using-stack). - - -### Building the website - -The website version of the book is built in three stages: - - 1. The `.lagda.md` files are compiled to Markdown using Agda’s highlighter. - (This requires several POSIX tools, such as `bash`, `sed`, and `grep`.) - - 2. The Markdown files are converted to HTML using [Jekyll][ruby-jekyll], a widely-used static site builder. - (This requires [Ruby][ruby] and [Jekyll][ruby-jekyll].) - - 3. The HTML is checked using [html-proofer][ruby-html-proofer]. - (This requires [Ruby][ruby] and [html-proofer][ruby-html-proofer].) - -Most recent versions of [Ruby][ruby] should work. The easiest way to install [Jekyll][ruby-jekyll] and [html-proofer][ruby-html-proofer] is using [Bundler][ruby-bundler]. You can install [Bundler][ruby-bundler] by running: -```bash -gem install bundler -``` -You can install the remainder of the dependencies—[Jekyll][ruby-jekyll], [html-proofer][ruby-html-proofer], *etc.*—by running: -```bash -bundle install -``` -Once you have installed all of the dependencies, you can build a copy of the book, and host it locally, by running: -```bash -make build -make serve -``` -The Makefile offers more than just these options: -```bash -make # see make test -make build # builds lagda->markdown and the website -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 -make serve # starts the server -make server-start # starts the server in detached mode -make server-stop # stops the server, uses pkill -make clean # removes all ~unnecessary~ generated files -make clobber # removes all generated files -``` -If you simply wish to have a local copy of the book, e.g. for offline reading, but don't care about editing and rebuilding the book, you can grab a copy of the [master branch][plfa-master], which is automatically built using Travis. You will still need [Jekyll][ruby-jekyll] and preferably [Bundler][ruby-bundler] to host the book (see above). To host the book this way, download a copy of the [master branch][plfa-master], unzip, and from within the directory run -```bash -bundle install -bundle exec jekyll serve -``` - - -### Building the EPUB - -The [EPUB version][epub] of the book is built using Pandoc. - -Install a recent version of Pandoc, [available here][pandoc]. The easiest way to install Pandoc is using their official installer, which is much faster than compiling Pandoc from source with Haskell Stack. - -Once you’ve installed Pandoc, you can build the EPUB by running: -```bash -make epub -``` -The EPUB is written to `out/epub/plfa.epub`. +If you want Stack to use your system installation of GHC, follow the instructions for [Using an existing installation of GHC](#using-an-existing-installation-of-ghc). @@ -227,29 +326,31 @@ The EPUB is written to `out/epub/plfa.epub`. [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 - +[haskell-stack]: https://docs.haskellstack.org/en/stable/README/ +[haskell-ghc]: https://www.haskell.org/ghc/ +[git]: https://git-scm.com/downloads [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-holes]: https://agda.readthedocs.io/en/v2.5.4/getting-started/quick-guide.html [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 - +[emacs]: https://www.gnu.org/software/emacs/download.html +[emacstour]: https://www.gnu.org/software/emacs/tour/ +[aquamacs]: http://aquamacs.org/ [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/ - [fix-whitespace]: https://github.com/agda/fix-whitespace - -[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 +[hakyll]: https://jaspervdj.be/hakyll/ [pandoc]: https://pandoc.org/installing.html [epubcheck]: https://github.com/w3c/epubcheck +[xcode]: https://developer.apple.com/xcode/ +[font-sourcecodepro]: https://github.com/adobe-fonts/source-code-pro +[font-dejavusansmono]: https://dejavu-fonts.github.io/ +[font-freemono]: https://www.gnu.org/software/freefont/ +[font-mononoki]: https://madmalik.github.io/mononoki/ +[font-mononoki-debian]: https://packages.debian.org/sid/fonts/fonts-mononoki diff --git a/TODO.md b/TODO.md new file mode 100644 index 00000000..bbd15a65 --- /dev/null +++ b/TODO.md @@ -0,0 +1,23 @@ +# Roadmap + +Here’s what still needs to happen in order to use Hakyll for PLFA builds. +We can release after the first milestone. +The goals in the second milestone are optional, but nice. + + +## Milestone 1 + +- migrate EPUB generation over to site.hs + + +## Milestone 2 + +- automatically generate Unicode sections + + use a context field similar to the teaser context + + create a template for book chapters which uses said field + + use book chapter template for .lagda.md files + +- automatically generate Statistics chapter + + see https://github.com/plfa/plfa.github.io/blob/41939ad0312b6012ac76f056c6da1f9ff590c040/hs/agda-count.hs + +- … diff --git a/_config.yml b/_config.yml deleted file mode 100644 index c7e10420..00000000 --- a/_config.yml +++ /dev/null @@ -1,71 +0,0 @@ -title: > - Programming Language Foundations in Agda - -description: > - Programming Language Foundations in Agda - -license: Creative Commons Attribution 4.0 International License -license-file: https://creativecommons.org/licenses/by/4.0/ - -# To include a new author, add them below in the order in which they are to be -# displayed in the author list. If they have made contributions as an author via -# GitHub, their username MUST be included in the list. -authors: - - name: Philip Wadler - email: wadler@inf.ed.ac.uk - corresponding: true - github_username: wadler - - name: Wen Kokke - email: wen.kokke@ed.ac.uk - corresponding: true - github_username: wenkokke - twitter_username: wenkokke - - name: Jeremy G. Siek - email: jsiek@indiana.edu - corresponding: true - github_username: jsiek - twitter_username: jeremysiek - -extra_contributors: - - github_username: cyberglot - - name: Vikraman Choudhury - - name: Ben Darwin - - github_username: koo5 - - name: Anish Tondwalkar - - name: Nils Anders Danielsson - - name: Miëtek Bak - - name: Gergő Érdi - - name: Adam Sandberg Eriksson - - name: David Janin - - name: András Kovács - - name: Ulf Norell - - name: Liam O'Connor - - name: N. Raghavendra - - name: Roman Kireev - - name: Amr Sabry - -google_analytics: "UA-125055580-1" - -repository: plfa/plfa.github.io -branch: dev - -baseurl: "" -url: "https://plfa.github.io" -markdown: kramdown -theme: minima -excerpt_separator: -exclude: - - "*.lagda.md" - - "*.agdai" - - "*.agda-lib" - - "extra/" - - "papers/" - - "vendor/" - - "epub/" - - ".versions/" - - "_build/" - - "Guardfile" - - "Gemfile" - - "Gemfile.lock" - - "highlight.sh" - - "out/epub/acknowledgements.md" diff --git a/_includes/footer.html b/_includes/footer.html deleted file mode 100644 index 8494b94e..00000000 --- a/_includes/footer.html +++ /dev/null @@ -1,36 +0,0 @@ -
- - -
- - - - {%- for author in site.authors -%} - {%- if author.corresponding -%} - - {%- endif -%} - {%- endfor -%} - This work is licensed under a {{ site.license }} -
-
diff --git a/_includes/head.html b/_includes/head.html deleted file mode 100644 index 08d4efa1..00000000 --- a/_includes/head.html +++ /dev/null @@ -1,17 +0,0 @@ - - - - - - {%- if page.layout == 'home' -%} - {{ site.title }} - {%- else -%} - {{ page.title }} | {{ site.title }} - {%- endif -%} - - {%- seo title=false -%} - - {%- if jekyll.environment == 'production' and site.google_analytics -%} - {%- include google-analytics.html -%} - {%- endif -%} - diff --git a/_includes/next.html b/_includes/next.html deleted file mode 100644 index 916e1e11..00000000 --- a/_includes/next.html +++ /dev/null @@ -1,17 +0,0 @@ -

- {% if page.prev %} - Prev - {% endif %} - {% if page.prev and (page.src or page.next) %} - • - {% endif %} - {% if page.src %} - Source - {% endif %} - {% if page.src and page.next %} - • - {% endif %} - {% if page.next %} - Next - {% endif %} -

diff --git a/_includes/script.html b/_includes/script.html deleted file mode 100644 index 548b53c2..00000000 --- a/_includes/script.html +++ /dev/null @@ -1,77 +0,0 @@ - - - - - - - - - - - - diff --git a/_includes/social.html b/_includes/social.html deleted file mode 100644 index 7576de8d..00000000 --- a/_includes/social.html +++ /dev/null @@ -1,13 +0,0 @@ - diff --git a/_layouts/default.html b/_layouts/default.html deleted file mode 100644 index c1dac568..00000000 --- a/_layouts/default.html +++ /dev/null @@ -1,29 +0,0 @@ - - - - {%- include head.html -%} - - - - {%- include header.html -%} - -
-
- {{ content }} -
-
- - {%- include footer.html -%} - - - - {%- include script.html -%} - - - - diff --git a/_layouts/home.html b/_layouts/home.html deleted file mode 100644 index 8cc53c77..00000000 --- a/_layouts/home.html +++ /dev/null @@ -1,30 +0,0 @@ ---- -layout: default ---- - -
- - {{ content }} - - {%- if site.posts.size > 0 -%} -

Announcements

-
    - {%- for post in site.posts -%} -
  • - {%- assign date_format = site.minima.date_format | default: "%b %-d, %Y" -%} - -

    {{ post.title | escape }}

    - {%- if post.short -%} - {{ post.excerpt }} - {%- else -%} - {{ post.excerpt }} - (more) - {%- endif -%} -
  • - {%- endfor -%} -
- -

Subscribe

- {%- endif -%} - -
diff --git a/_layouts/page.html b/_layouts/page.html deleted file mode 100644 index aea2536e..00000000 --- a/_layouts/page.html +++ /dev/null @@ -1,19 +0,0 @@ ---- -layout: default ---- - -
- -
-

{{ page.title | escape }}

-
- - {% include next.html %} - -
- {{ content }} -
- - {% include next.html %} - -
diff --git a/_layouts/post.html b/_layouts/post.html deleted file mode 100644 index fa151b3b..00000000 --- a/_layouts/post.html +++ /dev/null @@ -1,27 +0,0 @@ ---- -layout: default ---- -
- -
-

{{ page.title | escape }}

- -
- -
- {{ content }} -
- - {%- if site.disqus.shortname -%} - {%- include disqus_comments.html -%} - {%- endif -%} - - -
diff --git a/_sass/katex.scss b/_sass/katex.scss deleted file mode 100644 index 47dd09da..00000000 --- a/_sass/katex.scss +++ /dev/null @@ -1 +0,0 @@ -@font-face{font-family:KaTeX_AMS;src:url(fonts/KaTeX_AMS-Regular.eot);src:url(fonts/KaTeX_AMS-Regular.eot#iefix) format('embedded-opentype'),url(fonts/KaTeX_AMS-Regular.woff2) format('woff2'),url(fonts/KaTeX_AMS-Regular.woff) format('woff'),url(fonts/KaTeX_AMS-Regular.ttf) format('ttf');font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Caligraphic;src:url(fonts/KaTeX_Caligraphic-Bold.eot);src:url(fonts/KaTeX_Caligraphic-Bold.eot#iefix) format('embedded-opentype'),url(fonts/KaTeX_Caligraphic-Bold.woff2) format('woff2'),url(fonts/KaTeX_Caligraphic-Bold.woff) format('woff'),url(fonts/KaTeX_Caligraphic-Bold.ttf) format('ttf');font-weight:700;font-style:normal}@font-face{font-family:KaTeX_Caligraphic;src:url(fonts/KaTeX_Caligraphic-Regular.eot);src:url(fonts/KaTeX_Caligraphic-Regular.eot#iefix) format('embedded-opentype'),url(fonts/KaTeX_Caligraphic-Regular.woff2) format('woff2'),url(fonts/KaTeX_Caligraphic-Regular.woff) format('woff'),url(fonts/KaTeX_Caligraphic-Regular.ttf) format('ttf');font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Fraktur;src:url(fonts/KaTeX_Fraktur-Bold.eot);src:url(fonts/KaTeX_Fraktur-Bold.eot#iefix) format('embedded-opentype'),url(fonts/KaTeX_Fraktur-Bold.woff2) format('woff2'),url(fonts/KaTeX_Fraktur-Bold.woff) format('woff'),url(fonts/KaTeX_Fraktur-Bold.ttf) format('ttf');font-weight:700;font-style:normal}@font-face{font-family:KaTeX_Fraktur;src:url(fonts/KaTeX_Fraktur-Regular.eot);src:url(fonts/KaTeX_Fraktur-Regular.eot#iefix) format('embedded-opentype'),url(fonts/KaTeX_Fraktur-Regular.woff2) format('woff2'),url(fonts/KaTeX_Fraktur-Regular.woff) format('woff'),url(fonts/KaTeX_Fraktur-Regular.ttf) format('ttf');font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Main;src:url(fonts/KaTeX_Main-Bold.eot);src:url(fonts/KaTeX_Main-Bold.eot#iefix) format('embedded-opentype'),url(fonts/KaTeX_Main-Bold.woff2) format('woff2'),url(fonts/KaTeX_Main-Bold.woff) format('woff'),url(fonts/KaTeX_Main-Bold.ttf) format('ttf');font-weight:700;font-style:normal}@font-face{font-family:KaTeX_Main;src:url(fonts/KaTeX_Main-Italic.eot);src:url(fonts/KaTeX_Main-Italic.eot#iefix) format('embedded-opentype'),url(fonts/KaTeX_Main-Italic.woff2) format('woff2'),url(fonts/KaTeX_Main-Italic.woff) format('woff'),url(fonts/KaTeX_Main-Italic.ttf) format('ttf');font-weight:400;font-style:italic}@font-face{font-family:KaTeX_Main;src:url(fonts/KaTeX_Main-Regular.eot);src:url(fonts/KaTeX_Main-Regular.eot#iefix) format('embedded-opentype'),url(fonts/KaTeX_Main-Regular.woff2) format('woff2'),url(fonts/KaTeX_Main-Regular.woff) format('woff'),url(fonts/KaTeX_Main-Regular.ttf) format('ttf');font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Math;src:url(fonts/KaTeX_Math-Italic.eot);src:url(fonts/KaTeX_Math-Italic.eot#iefix) format('embedded-opentype'),url(fonts/KaTeX_Math-Italic.woff2) format('woff2'),url(fonts/KaTeX_Math-Italic.woff) format('woff'),url(fonts/KaTeX_Math-Italic.ttf) format('ttf');font-weight:400;font-style:italic}@font-face{font-family:KaTeX_SansSerif;src:url(fonts/KaTeX_SansSerif-Regular.eot);src:url(fonts/KaTeX_SansSerif-Regular.eot#iefix) format('embedded-opentype'),url(fonts/KaTeX_SansSerif-Regular.woff2) format('woff2'),url(fonts/KaTeX_SansSerif-Regular.woff) format('woff'),url(fonts/KaTeX_SansSerif-Regular.ttf) format('ttf');font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Script;src:url(fonts/KaTeX_Script-Regular.eot);src:url(fonts/KaTeX_Script-Regular.eot#iefix) format('embedded-opentype'),url(fonts/KaTeX_Script-Regular.woff2) format('woff2'),url(fonts/KaTeX_Script-Regular.woff) format('woff'),url(fonts/KaTeX_Script-Regular.ttf) format('ttf');font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Size1;src:url(fonts/KaTeX_Size1-Regular.eot);src:url(fonts/KaTeX_Size1-Regular.eot#iefix) format('embedded-opentype'),url(fonts/KaTeX_Size1-Regular.woff2) format('woff2'),url(fonts/KaTeX_Size1-Regular.woff) format('woff'),url(fonts/KaTeX_Size1-Regular.ttf) format('ttf');font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Size2;src:url(fonts/KaTeX_Size2-Regular.eot);src:url(fonts/KaTeX_Size2-Regular.eot#iefix) format('embedded-opentype'),url(fonts/KaTeX_Size2-Regular.woff2) format('woff2'),url(fonts/KaTeX_Size2-Regular.woff) format('woff'),url(fonts/KaTeX_Size2-Regular.ttf) format('ttf');font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Size3;src:url(fonts/KaTeX_Size3-Regular.eot);src:url(fonts/KaTeX_Size3-Regular.eot#iefix) format('embedded-opentype'),url(fonts/KaTeX_Size3-Regular.woff2) format('woff2'),url(fonts/KaTeX_Size3-Regular.woff) format('woff'),url(fonts/KaTeX_Size3-Regular.ttf) format('ttf');font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Size4;src:url(fonts/KaTeX_Size4-Regular.eot);src:url(fonts/KaTeX_Size4-Regular.eot#iefix) format('embedded-opentype'),url(fonts/KaTeX_Size4-Regular.woff2) format('woff2'),url(fonts/KaTeX_Size4-Regular.woff) format('woff'),url(fonts/KaTeX_Size4-Regular.ttf) format('ttf');font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Typewriter;src:url(fonts/KaTeX_Typewriter-Regular.eot);src:url(fonts/KaTeX_Typewriter-Regular.eot#iefix) format('embedded-opentype'),url(fonts/KaTeX_Typewriter-Regular.woff2) format('woff2'),url(fonts/KaTeX_Typewriter-Regular.woff) format('woff'),url(fonts/KaTeX_Typewriter-Regular.ttf) format('ttf');font-weight:400;font-style:normal}.katex-display{display:block;margin:1em 0;text-align:center}.katex-display>.katex{display:inline-block;text-align:initial}.katex{font:400 1.21em KaTeX_Main;line-height:1.2;white-space:nowrap;text-indent:0}.katex .katex-html{display:inline-block}.katex .katex-mathml{position:absolute;clip:rect(1px,1px,1px,1px);padding:0;border:0;height:1px;width:1px;overflow:hidden}.katex .base,.katex .strut{display:inline-block}.katex .mathit{font-family:KaTeX_Math;font-style:italic}.katex .mathbf{font-family:KaTeX_Main;font-weight:700}.katex .amsrm,.katex .mathbb{font-family:KaTeX_AMS}.katex .mathcal{font-family:KaTeX_Caligraphic}.katex .mathfrak{font-family:KaTeX_Fraktur}.katex .mathtt{font-family:KaTeX_Typewriter}.katex .mathscr{font-family:KaTeX_Script}.katex .mathsf{font-family:KaTeX_SansSerif}.katex .mainit{font-family:KaTeX_Main;font-style:italic}.katex .textstyle>.mord+.mop{margin-left:.16667em}.katex .textstyle>.mord+.mbin{margin-left:.22222em}.katex .textstyle>.mord+.mrel{margin-left:.27778em}.katex .textstyle>.mop+.mop,.katex .textstyle>.mop+.mord,.katex .textstyle>.mord+.minner{margin-left:.16667em}.katex .textstyle>.mop+.mrel{margin-left:.27778em}.katex .textstyle>.mop+.minner{margin-left:.16667em}.katex .textstyle>.mbin+.minner,.katex .textstyle>.mbin+.mop,.katex .textstyle>.mbin+.mopen,.katex .textstyle>.mbin+.mord{margin-left:.22222em}.katex .textstyle>.mrel+.minner,.katex .textstyle>.mrel+.mop,.katex .textstyle>.mrel+.mopen,.katex .textstyle>.mrel+.mord{margin-left:.27778em}.katex .textstyle>.mclose+.mop{margin-left:.16667em}.katex .textstyle>.mclose+.mbin{margin-left:.22222em}.katex .textstyle>.mclose+.mrel{margin-left:.27778em}.katex .textstyle>.mclose+.minner,.katex .textstyle>.minner+.mop,.katex .textstyle>.minner+.mord,.katex .textstyle>.mpunct+.mclose,.katex .textstyle>.mpunct+.minner,.katex .textstyle>.mpunct+.mop,.katex .textstyle>.mpunct+.mopen,.katex .textstyle>.mpunct+.mord,.katex .textstyle>.mpunct+.mpunct,.katex .textstyle>.mpunct+.mrel{margin-left:.16667em}.katex .textstyle>.minner+.mbin{margin-left:.22222em}.katex .textstyle>.minner+.mrel{margin-left:.27778em}.katex .mclose+.mop,.katex .minner+.mop,.katex .mop+.mop,.katex .mop+.mord,.katex .mord+.mop,.katex .textstyle>.minner+.minner,.katex .textstyle>.minner+.mopen,.katex .textstyle>.minner+.mpunct{margin-left:.16667em}.katex .reset-textstyle.textstyle{font-size:1em}.katex .reset-textstyle.scriptstyle{font-size:.7em}.katex .reset-textstyle.scriptscriptstyle{font-size:.5em}.katex .reset-scriptstyle.textstyle{font-size:1.42857em}.katex .reset-scriptstyle.scriptstyle{font-size:1em}.katex .reset-scriptstyle.scriptscriptstyle{font-size:.71429em}.katex .reset-scriptscriptstyle.textstyle{font-size:2em}.katex .reset-scriptscriptstyle.scriptstyle{font-size:1.4em}.katex .reset-scriptscriptstyle.scriptscriptstyle{font-size:1em}.katex .style-wrap{position:relative}.katex .vlist{display:inline-block}.katex .vlist>span{display:block;height:0;position:relative}.katex .vlist>span>span{display:inline-block}.katex .vlist .baseline-fix{display:inline-table;table-layout:fixed}.katex .msupsub{text-align:left}.katex .mfrac>span>span{text-align:center}.katex .mfrac .frac-line{width:100%}.katex .mfrac .frac-line:before{border-bottom-style:solid;border-bottom-width:1px;content:"";display:block}.katex .mfrac .frac-line:after{border-bottom-style:solid;border-bottom-width:.04em;content:"";display:block;margin-top:-1px}.katex .mspace{display:inline-block}.katex .mspace.negativethinspace{margin-left:-.16667em}.katex .mspace.thinspace{width:.16667em}.katex .mspace.mediumspace{width:.22222em}.katex .mspace.thickspace{width:.27778em}.katex .mspace.enspace{width:.5em}.katex .mspace.quad{width:1em}.katex .mspace.qquad{width:2em}.katex .llap,.katex .rlap{width:0;position:relative}.katex .llap>.inner,.katex .rlap>.inner{position:absolute}.katex .llap>.fix,.katex .rlap>.fix{display:inline-block}.katex .llap>.inner{right:0}.katex .rlap>.inner{left:0}.katex .katex-logo .a{font-size:.75em;margin-left:-.32em;position:relative;top:-.2em}.katex .katex-logo .t{margin-left:-.23em}.katex .katex-logo .e{margin-left:-.1667em;position:relative;top:.2155em}.katex .katex-logo .x{margin-left:-.125em}.katex .rule{display:inline-block;border:0 solid;position:relative}.katex .overline .overline-line,.katex .underline .underline-line{width:100%}.katex .overline .overline-line:before,.katex .underline .underline-line:before{border-bottom-style:solid;border-bottom-width:1px;content:"";display:block}.katex .overline .overline-line:after,.katex .underline .underline-line:after{border-bottom-style:solid;border-bottom-width:.04em;content:"";display:block;margin-top:-1px}.katex .sqrt>.sqrt-sign{position:relative}.katex .sqrt .sqrt-line{width:100%}.katex .sqrt .sqrt-line:before{border-bottom-style:solid;border-bottom-width:1px;content:"";display:block}.katex .sqrt .sqrt-line:after{border-bottom-style:solid;border-bottom-width:.04em;content:"";display:block;margin-top:-1px}.katex .sqrt>.root{margin-left:.27777778em;margin-right:-.55555556em}.katex .fontsize-ensurer,.katex .sizing{display:inline-block}.katex .fontsize-ensurer.reset-size1.size1,.katex .sizing.reset-size1.size1{font-size:1em}.katex .fontsize-ensurer.reset-size1.size2,.katex .sizing.reset-size1.size2{font-size:1.4em}.katex .fontsize-ensurer.reset-size1.size3,.katex .sizing.reset-size1.size3{font-size:1.6em}.katex .fontsize-ensurer.reset-size1.size4,.katex .sizing.reset-size1.size4{font-size:1.8em}.katex .fontsize-ensurer.reset-size1.size5,.katex .sizing.reset-size1.size5{font-size:2em}.katex .fontsize-ensurer.reset-size1.size6,.katex .sizing.reset-size1.size6{font-size:2.4em}.katex .fontsize-ensurer.reset-size1.size7,.katex .sizing.reset-size1.size7{font-size:2.88em}.katex .fontsize-ensurer.reset-size1.size8,.katex .sizing.reset-size1.size8{font-size:3.46em}.katex .fontsize-ensurer.reset-size1.size9,.katex .sizing.reset-size1.size9{font-size:4.14em}.katex .fontsize-ensurer.reset-size1.size10,.katex .sizing.reset-size1.size10{font-size:4.98em}.katex .fontsize-ensurer.reset-size2.size1,.katex .sizing.reset-size2.size1{font-size:.71428571em}.katex .fontsize-ensurer.reset-size2.size2,.katex .sizing.reset-size2.size2{font-size:1em}.katex .fontsize-ensurer.reset-size2.size3,.katex .sizing.reset-size2.size3{font-size:1.14285714em}.katex .fontsize-ensurer.reset-size2.size4,.katex .sizing.reset-size2.size4{font-size:1.28571429em}.katex .fontsize-ensurer.reset-size2.size5,.katex .sizing.reset-size2.size5{font-size:1.42857143em}.katex .fontsize-ensurer.reset-size2.size6,.katex .sizing.reset-size2.size6{font-size:1.71428571em}.katex .fontsize-ensurer.reset-size2.size7,.katex .sizing.reset-size2.size7{font-size:2.05714286em}.katex .fontsize-ensurer.reset-size2.size8,.katex .sizing.reset-size2.size8{font-size:2.47142857em}.katex .fontsize-ensurer.reset-size2.size9,.katex .sizing.reset-size2.size9{font-size:2.95714286em}.katex .fontsize-ensurer.reset-size2.size10,.katex .sizing.reset-size2.size10{font-size:3.55714286em}.katex .fontsize-ensurer.reset-size3.size1,.katex .sizing.reset-size3.size1{font-size:.625em}.katex .fontsize-ensurer.reset-size3.size2,.katex .sizing.reset-size3.size2{font-size:.875em}.katex .fontsize-ensurer.reset-size3.size3,.katex .sizing.reset-size3.size3{font-size:1em}.katex .fontsize-ensurer.reset-size3.size4,.katex .sizing.reset-size3.size4{font-size:1.125em}.katex .fontsize-ensurer.reset-size3.size5,.katex .sizing.reset-size3.size5{font-size:1.25em}.katex .fontsize-ensurer.reset-size3.size6,.katex .sizing.reset-size3.size6{font-size:1.5em}.katex .fontsize-ensurer.reset-size3.size7,.katex .sizing.reset-size3.size7{font-size:1.8em}.katex .fontsize-ensurer.reset-size3.size8,.katex .sizing.reset-size3.size8{font-size:2.1625em}.katex .fontsize-ensurer.reset-size3.size9,.katex .sizing.reset-size3.size9{font-size:2.5875em}.katex .fontsize-ensurer.reset-size3.size10,.katex .sizing.reset-size3.size10{font-size:3.1125em}.katex .fontsize-ensurer.reset-size4.size1,.katex .sizing.reset-size4.size1{font-size:.55555556em}.katex .fontsize-ensurer.reset-size4.size2,.katex .sizing.reset-size4.size2{font-size:.77777778em}.katex .fontsize-ensurer.reset-size4.size3,.katex .sizing.reset-size4.size3{font-size:.88888889em}.katex .fontsize-ensurer.reset-size4.size4,.katex .sizing.reset-size4.size4{font-size:1em}.katex .fontsize-ensurer.reset-size4.size5,.katex .sizing.reset-size4.size5{font-size:1.11111111em}.katex .fontsize-ensurer.reset-size4.size6,.katex .sizing.reset-size4.size6{font-size:1.33333333em}.katex .fontsize-ensurer.reset-size4.size7,.katex .sizing.reset-size4.size7{font-size:1.6em}.katex .fontsize-ensurer.reset-size4.size8,.katex .sizing.reset-size4.size8{font-size:1.92222222em}.katex .fontsize-ensurer.reset-size4.size9,.katex .sizing.reset-size4.size9{font-size:2.3em}.katex .fontsize-ensurer.reset-size4.size10,.katex .sizing.reset-size4.size10{font-size:2.76666667em}.katex .fontsize-ensurer.reset-size5.size1,.katex .sizing.reset-size5.size1{font-size:.5em}.katex .fontsize-ensurer.reset-size5.size2,.katex .sizing.reset-size5.size2{font-size:.7em}.katex .fontsize-ensurer.reset-size5.size3,.katex .sizing.reset-size5.size3{font-size:.8em}.katex .fontsize-ensurer.reset-size5.size4,.katex .sizing.reset-size5.size4{font-size:.9em}.katex .fontsize-ensurer.reset-size5.size5,.katex .sizing.reset-size5.size5{font-size:1em}.katex .fontsize-ensurer.reset-size5.size6,.katex .sizing.reset-size5.size6{font-size:1.2em}.katex .fontsize-ensurer.reset-size5.size7,.katex .sizing.reset-size5.size7{font-size:1.44em}.katex .fontsize-ensurer.reset-size5.size8,.katex .sizing.reset-size5.size8{font-size:1.73em}.katex .fontsize-ensurer.reset-size5.size9,.katex .sizing.reset-size5.size9{font-size:2.07em}.katex .fontsize-ensurer.reset-size5.size10,.katex .sizing.reset-size5.size10{font-size:2.49em}.katex .fontsize-ensurer.reset-size6.size1,.katex .sizing.reset-size6.size1{font-size:.41666667em}.katex .fontsize-ensurer.reset-size6.size2,.katex .sizing.reset-size6.size2{font-size:.58333333em}.katex .fontsize-ensurer.reset-size6.size3,.katex .sizing.reset-size6.size3{font-size:.66666667em}.katex .fontsize-ensurer.reset-size6.size4,.katex .sizing.reset-size6.size4{font-size:.75em}.katex .fontsize-ensurer.reset-size6.size5,.katex .sizing.reset-size6.size5{font-size:.83333333em}.katex .fontsize-ensurer.reset-size6.size6,.katex .sizing.reset-size6.size6{font-size:1em}.katex .fontsize-ensurer.reset-size6.size7,.katex .sizing.reset-size6.size7{font-size:1.2em}.katex .fontsize-ensurer.reset-size6.size8,.katex .sizing.reset-size6.size8{font-size:1.44166667em}.katex .fontsize-ensurer.reset-size6.size9,.katex .sizing.reset-size6.size9{font-size:1.725em}.katex .fontsize-ensurer.reset-size6.size10,.katex .sizing.reset-size6.size10{font-size:2.075em}.katex .fontsize-ensurer.reset-size7.size1,.katex .sizing.reset-size7.size1{font-size:.34722222em}.katex .fontsize-ensurer.reset-size7.size2,.katex .sizing.reset-size7.size2{font-size:.48611111em}.katex .fontsize-ensurer.reset-size7.size3,.katex .sizing.reset-size7.size3{font-size:.55555556em}.katex .fontsize-ensurer.reset-size7.size4,.katex .sizing.reset-size7.size4{font-size:.625em}.katex .fontsize-ensurer.reset-size7.size5,.katex .sizing.reset-size7.size5{font-size:.69444444em}.katex .fontsize-ensurer.reset-size7.size6,.katex .sizing.reset-size7.size6{font-size:.83333333em}.katex .fontsize-ensurer.reset-size7.size7,.katex .sizing.reset-size7.size7{font-size:1em}.katex .fontsize-ensurer.reset-size7.size8,.katex .sizing.reset-size7.size8{font-size:1.20138889em}.katex .fontsize-ensurer.reset-size7.size9,.katex .sizing.reset-size7.size9{font-size:1.4375em}.katex .fontsize-ensurer.reset-size7.size10,.katex .sizing.reset-size7.size10{font-size:1.72916667em}.katex .fontsize-ensurer.reset-size8.size1,.katex .sizing.reset-size8.size1{font-size:.28901734em}.katex .fontsize-ensurer.reset-size8.size2,.katex .sizing.reset-size8.size2{font-size:.40462428em}.katex .fontsize-ensurer.reset-size8.size3,.katex .sizing.reset-size8.size3{font-size:.46242775em}.katex .fontsize-ensurer.reset-size8.size4,.katex .sizing.reset-size8.size4{font-size:.52023121em}.katex .fontsize-ensurer.reset-size8.size5,.katex .sizing.reset-size8.size5{font-size:.57803468em}.katex .fontsize-ensurer.reset-size8.size6,.katex .sizing.reset-size8.size6{font-size:.69364162em}.katex .fontsize-ensurer.reset-size8.size7,.katex .sizing.reset-size8.size7{font-size:.83236994em}.katex .fontsize-ensurer.reset-size8.size8,.katex .sizing.reset-size8.size8{font-size:1em}.katex .fontsize-ensurer.reset-size8.size9,.katex .sizing.reset-size8.size9{font-size:1.19653179em}.katex .fontsize-ensurer.reset-size8.size10,.katex .sizing.reset-size8.size10{font-size:1.43930636em}.katex .fontsize-ensurer.reset-size9.size1,.katex .sizing.reset-size9.size1{font-size:.24154589em}.katex .fontsize-ensurer.reset-size9.size2,.katex .sizing.reset-size9.size2{font-size:.33816425em}.katex .fontsize-ensurer.reset-size9.size3,.katex .sizing.reset-size9.size3{font-size:.38647343em}.katex .fontsize-ensurer.reset-size9.size4,.katex .sizing.reset-size9.size4{font-size:.43478261em}.katex .fontsize-ensurer.reset-size9.size5,.katex .sizing.reset-size9.size5{font-size:.48309179em}.katex .fontsize-ensurer.reset-size9.size6,.katex .sizing.reset-size9.size6{font-size:.57971014em}.katex .fontsize-ensurer.reset-size9.size7,.katex .sizing.reset-size9.size7{font-size:.69565217em}.katex .fontsize-ensurer.reset-size9.size8,.katex .sizing.reset-size9.size8{font-size:.83574879em}.katex .fontsize-ensurer.reset-size9.size9,.katex .sizing.reset-size9.size9{font-size:1em}.katex .fontsize-ensurer.reset-size9.size10,.katex .sizing.reset-size9.size10{font-size:1.20289855em}.katex .fontsize-ensurer.reset-size10.size1,.katex .sizing.reset-size10.size1{font-size:.20080321em}.katex .fontsize-ensurer.reset-size10.size2,.katex .sizing.reset-size10.size2{font-size:.2811245em}.katex .fontsize-ensurer.reset-size10.size3,.katex .sizing.reset-size10.size3{font-size:.32128514em}.katex .fontsize-ensurer.reset-size10.size4,.katex .sizing.reset-size10.size4{font-size:.36144578em}.katex .fontsize-ensurer.reset-size10.size5,.katex .sizing.reset-size10.size5{font-size:.40160643em}.katex .fontsize-ensurer.reset-size10.size6,.katex .sizing.reset-size10.size6{font-size:.48192771em}.katex .fontsize-ensurer.reset-size10.size7,.katex .sizing.reset-size10.size7{font-size:.57831325em}.katex .fontsize-ensurer.reset-size10.size8,.katex .sizing.reset-size10.size8{font-size:.69477912em}.katex .fontsize-ensurer.reset-size10.size9,.katex .sizing.reset-size10.size9{font-size:.8313253em}.katex .fontsize-ensurer.reset-size10.size10,.katex .sizing.reset-size10.size10{font-size:1em}.katex .delimsizing.size1{font-family:KaTeX_Size1}.katex .delimsizing.size2{font-family:KaTeX_Size2}.katex .delimsizing.size3{font-family:KaTeX_Size3}.katex .delimsizing.size4{font-family:KaTeX_Size4}.katex .delimsizing.mult .delim-size1>span{font-family:KaTeX_Size1}.katex .delimsizing.mult .delim-size4>span{font-family:KaTeX_Size4}.katex .nulldelimiter{display:inline-block;width:.12em}.katex .op-symbol{position:relative}.katex .op-symbol.small-op{font-family:KaTeX_Size1}.katex .op-symbol.large-op{font-family:KaTeX_Size2}.katex .accent>.vlist>span,.katex .op-limits>.vlist>span{text-align:center}.katex .accent .accent-body>span{width:0}.katex .accent .accent-body.accent-vec>span{position:relative;left:.326em}.katex .mtable .vertical-separator{display:inline-block;margin:0 -.025em;border-right:.05em solid #000}.katex .mtable .arraycolsep{display:inline-block}.katex .mtable .col-align-c>.vlist{text-align:center}.katex .mtable .col-align-l>.vlist{text-align:left}.katex .mtable .col-align-r>.vlist{text-align:right} \ No newline at end of file diff --git a/assets/main.scss b/assets/main.scss deleted file mode 100644 index e566a391..00000000 --- a/assets/main.scss +++ /dev/null @@ -1,28 +0,0 @@ ---- -# Only the main Sass file needs front matter (the dashes are enough) ---- -@import "katex"; -@import "minima"; -@import "agda"; - -$on-medium: 600px !default; - -.trigger { display: none; } - -@media screen and (min-width: $on-medium) { - .trigger { display: block; } -} - -ul.list-of-contributors { - display: grid; - grid-template-columns: repeat(3, 1fr); - width: calc(100% - 2rem); -} - -ul.list-of-contributors li { - margin-right: 2rem; -} - -pre { - break-inside: avoid; -} diff --git a/authors/jsiek.metadata b/authors/jsiek.metadata new file mode 100644 index 00000000..80990914 --- /dev/null +++ b/authors/jsiek.metadata @@ -0,0 +1,7 @@ +--- +name : Jeremy G. Siek +email : jsiek@indiana.edu +corresponding : true +github : jsiek +twitter : jeremysiek +--- diff --git a/authors/wadler.metadata b/authors/wadler.metadata new file mode 100644 index 00000000..446f4eb4 --- /dev/null +++ b/authors/wadler.metadata @@ -0,0 +1,6 @@ +--- +name : Philip Wadler +email : wadler@inf.ed.ac.uk +corresponding : true +github : wadler +--- diff --git a/authors/wenkokke.metadata b/authors/wenkokke.metadata new file mode 100644 index 00000000..703c0a4e --- /dev/null +++ b/authors/wenkokke.metadata @@ -0,0 +1,7 @@ +--- +name : Wen Kokke +email : wen.kokke@ed.ac.uk +corresponding : true +github : wenkokke +twitter : wenkokke +--- diff --git a/contributors/AD1024.metadata b/contributors/AD1024.metadata new file mode 100644 index 00000000..e19dc33f --- /dev/null +++ b/contributors/AD1024.metadata @@ -0,0 +1,5 @@ +--- +count: 2 +name: Mike He +github: AD1024 +--- diff --git a/contributors/AndrasKovacs.metadata b/contributors/AndrasKovacs.metadata new file mode 100644 index 00000000..d66d9d45 --- /dev/null +++ b/contributors/AndrasKovacs.metadata @@ -0,0 +1,5 @@ +--- +name: András Kovács +github: AndrasKovacs +count: 1 +--- diff --git a/contributors/ChefYeum.metadata b/contributors/ChefYeum.metadata new file mode 100644 index 00000000..ea93037d --- /dev/null +++ b/contributors/ChefYeum.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Dee Yeum +github: ChefYeum +--- diff --git a/contributors/Cubesoup.metadata b/contributors/Cubesoup.metadata new file mode 100644 index 00000000..a2ca034b --- /dev/null +++ b/contributors/Cubesoup.metadata @@ -0,0 +1,5 @@ +--- +count: 12 +name: Chad Nester +github: Cubesoup +--- diff --git a/contributors/Fingerzam.metadata b/contributors/Fingerzam.metadata new file mode 100644 index 00000000..64dab154 --- /dev/null +++ b/contributors/Fingerzam.metadata @@ -0,0 +1,5 @@ +--- +count: 7 +name: Juhana Laurinharju +github: Fingerzam +--- diff --git a/contributors/GaganSD.metadata b/contributors/GaganSD.metadata new file mode 100644 index 00000000..01d1905f --- /dev/null +++ b/contributors/GaganSD.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Gagan Devagiri +github: GaganSD +--- diff --git a/contributors/Kwezan.metadata b/contributors/Kwezan.metadata new file mode 100644 index 00000000..c26bab00 --- /dev/null +++ b/contributors/Kwezan.metadata @@ -0,0 +1,5 @@ +--- +count: 36 +name: Zbigniew Stanasiuk +github: Kwezan +--- diff --git a/contributors/L-TChen.metadata b/contributors/L-TChen.metadata new file mode 100644 index 00000000..490e13d2 --- /dev/null +++ b/contributors/L-TChen.metadata @@ -0,0 +1,5 @@ +--- +count: 2 +name: Liang-Ting Chen +github: L-TChen +--- diff --git a/contributors/LightAndLight.metadata b/contributors/LightAndLight.metadata new file mode 100644 index 00000000..182cd1ee --- /dev/null +++ b/contributors/LightAndLight.metadata @@ -0,0 +1,5 @@ +--- +count: 2 +name: Isaac Elliott +github: LightAndLight +--- diff --git a/contributors/MatthiasGabriel.metadata b/contributors/MatthiasGabriel.metadata new file mode 100644 index 00000000..5b1ac10c --- /dev/null +++ b/contributors/MatthiasGabriel.metadata @@ -0,0 +1,5 @@ +--- +count: 2 +name: Matthias Gabriel +github: MatthiasGabriel +--- diff --git a/contributors/OlingCat.metadata b/contributors/OlingCat.metadata new file mode 100644 index 00000000..2b25af3d --- /dev/null +++ b/contributors/OlingCat.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Oling Cat +github: OlingCat +--- diff --git a/contributors/Teggy.metadata b/contributors/Teggy.metadata new file mode 100644 index 00000000..26416603 --- /dev/null +++ b/contributors/Teggy.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Torsten Grust +github: Teggy +--- diff --git a/contributors/UlfNorell.metadata b/contributors/UlfNorell.metadata new file mode 100644 index 00000000..d2dfc447 --- /dev/null +++ b/contributors/UlfNorell.metadata @@ -0,0 +1,5 @@ +--- +name: Ulf Norell +github: UlfNorell +count: 1 +--- diff --git a/contributors/abrisan.metadata b/contributors/abrisan.metadata new file mode 100644 index 00000000..7f330c8a --- /dev/null +++ b/contributors/abrisan.metadata @@ -0,0 +1,5 @@ +--- +count: 4 +name: Alexandru Brisan +github: abrisan +--- diff --git a/contributors/adamse.metadata b/contributors/adamse.metadata new file mode 100644 index 00000000..f0f14ac0 --- /dev/null +++ b/contributors/adamse.metadata @@ -0,0 +1,5 @@ +--- +name: Adam Sandberg Eriksson +github: adamse +count: 1 +--- diff --git a/contributors/atondwal.metadata b/contributors/atondwal.metadata new file mode 100644 index 00000000..c7b82fa7 --- /dev/null +++ b/contributors/atondwal.metadata @@ -0,0 +1,5 @@ +--- +name: Anish Tondwalkar +github: atondwal +count: 1 +--- diff --git a/contributors/bcdarwin.metadata b/contributors/bcdarwin.metadata new file mode 100644 index 00000000..1bd495da --- /dev/null +++ b/contributors/bcdarwin.metadata @@ -0,0 +1,5 @@ +--- +name: Ben Darwin +github: bcdarwin +count: 1 +--- diff --git a/contributors/caryoscelus.metadata b/contributors/caryoscelus.metadata new file mode 100644 index 00000000..6ec16caa --- /dev/null +++ b/contributors/caryoscelus.metadata @@ -0,0 +1,5 @@ +--- +count: 3 +name: caryoscelus +github: caryoscelus +--- diff --git a/contributors/chikeabuah.metadata b/contributors/chikeabuah.metadata new file mode 100644 index 00000000..92668fdd --- /dev/null +++ b/contributors/chikeabuah.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Chike Abuah +github: chikeabuah +--- diff --git a/contributors/citrusmunch.metadata b/contributors/citrusmunch.metadata new file mode 100644 index 00000000..54152c4a --- /dev/null +++ b/contributors/citrusmunch.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: citrusmunch +github: citrusmunch +--- diff --git a/contributors/cyberglot.metadata b/contributors/cyberglot.metadata new file mode 100644 index 00000000..1a495939 --- /dev/null +++ b/contributors/cyberglot.metadata @@ -0,0 +1,5 @@ +--- +name: April Gonçalves +github: cyberglot +count: 1 +--- diff --git a/contributors/dalpd.metadata b/contributors/dalpd.metadata new file mode 100644 index 00000000..610c670b --- /dev/null +++ b/contributors/dalpd.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Deniz Alp +github: dalpd +--- diff --git a/contributors/djanin.metadata b/contributors/djanin.metadata new file mode 100644 index 00000000..5a718939 --- /dev/null +++ b/contributors/djanin.metadata @@ -0,0 +1,5 @@ +--- +name: David Janin +github: djanin +count: 1 +--- diff --git a/contributors/effectfully.metadata b/contributors/effectfully.metadata new file mode 100644 index 00000000..7ba46329 --- /dev/null +++ b/contributors/effectfully.metadata @@ -0,0 +1,5 @@ +--- +name: Roman Kireev +github: effectfully +count: 1 +--- diff --git a/contributors/fangyi-zhou.metadata b/contributors/fangyi-zhou.metadata new file mode 100644 index 00000000..fd6fce56 --- /dev/null +++ b/contributors/fangyi-zhou.metadata @@ -0,0 +1,5 @@ +--- +count: 8 +name: Fangyi Zhou +github: fangyi-zhou +--- diff --git a/contributors/gallais.metadata b/contributors/gallais.metadata new file mode 100644 index 00000000..d8f89666 --- /dev/null +++ b/contributors/gallais.metadata @@ -0,0 +1,5 @@ +--- +count: 2 +name: G. Allais +github: gallais +--- diff --git a/contributors/gergoerdi.metadata b/contributors/gergoerdi.metadata new file mode 100644 index 00000000..51542ae9 --- /dev/null +++ b/contributors/gergoerdi.metadata @@ -0,0 +1,5 @@ +--- +name: Gergő Érdi +github: gergoerdi +count: 1 +--- diff --git a/contributors/googleson78.metadata b/contributors/googleson78.metadata new file mode 100644 index 00000000..88fb3854 --- /dev/null +++ b/contributors/googleson78.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Georgi Lyubenov +github: googleson78 +--- diff --git a/contributors/gshen42.metadata b/contributors/gshen42.metadata new file mode 100644 index 00000000..cad0978d --- /dev/null +++ b/contributors/gshen42.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Gan Shen +github: gshen42 +--- diff --git a/contributors/h4iku.metadata b/contributors/h4iku.metadata new file mode 100644 index 00000000..bf891162 --- /dev/null +++ b/contributors/h4iku.metadata @@ -0,0 +1,5 @@ +--- +count: 28 +name: Reza Gharibi +github: h4iku +--- diff --git a/contributors/hugomg.metadata b/contributors/hugomg.metadata new file mode 100644 index 00000000..d2c7c3cc --- /dev/null +++ b/contributors/hugomg.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Hugo Gualandi +github: hugomg +--- diff --git a/contributors/iblech.metadata b/contributors/iblech.metadata new file mode 100644 index 00000000..86057549 --- /dev/null +++ b/contributors/iblech.metadata @@ -0,0 +1,5 @@ +--- +count: 2 +name: Ingo Blechschmidt +github: iblech +--- diff --git a/contributors/jonaprieto.metadata b/contributors/jonaprieto.metadata new file mode 100644 index 00000000..73b94995 --- /dev/null +++ b/contributors/jonaprieto.metadata @@ -0,0 +1,5 @@ +--- +count: 4 +name: Jonathan Prieto +github: jonaprieto +--- diff --git a/contributors/jphmrst.metadata b/contributors/jphmrst.metadata new file mode 100644 index 00000000..e0a99ac2 --- /dev/null +++ b/contributors/jphmrst.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: John Maraist +github: jphmrst +--- diff --git a/contributors/k4rtik.metadata b/contributors/k4rtik.metadata new file mode 100644 index 00000000..7b8cab18 --- /dev/null +++ b/contributors/k4rtik.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Kartik Singhal +github: k4rtik +--- diff --git a/contributors/kenichi-asai.metadata b/contributors/kenichi-asai.metadata new file mode 100644 index 00000000..a6f66d8d --- /dev/null +++ b/contributors/kenichi-asai.metadata @@ -0,0 +1,5 @@ +--- +count: 5 +name: Kenichi Asai +github: kenichi-asai +--- diff --git a/contributors/koo5.metadata b/contributors/koo5.metadata new file mode 100644 index 00000000..5132613a --- /dev/null +++ b/contributors/koo5.metadata @@ -0,0 +1,5 @@ +--- +name: koo5 +github: koo5 +count: 1 +--- diff --git a/contributors/kranich.metadata b/contributors/kranich.metadata new file mode 100644 index 00000000..d2650067 --- /dev/null +++ b/contributors/kranich.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Stefan Kranich +github: kranich +--- diff --git a/contributors/kwxm.metadata b/contributors/kwxm.metadata new file mode 100644 index 00000000..8d5e5415 --- /dev/null +++ b/contributors/kwxm.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Kenneth MacKenzie +github: kwxm +--- diff --git a/contributors/laMudri.metadata b/contributors/laMudri.metadata new file mode 100644 index 00000000..2e14a96e --- /dev/null +++ b/contributors/laMudri.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: James Wood +github: laMudri +--- diff --git a/contributors/liamoc.metadata b/contributors/liamoc.metadata new file mode 100644 index 00000000..d275d800 --- /dev/null +++ b/contributors/liamoc.metadata @@ -0,0 +1,5 @@ +--- +name: Liam O'Connor +github: liamoc +count: 1 +--- diff --git a/contributors/lzmartinico.metadata b/contributors/lzmartinico.metadata new file mode 100644 index 00000000..40dc3174 --- /dev/null +++ b/contributors/lzmartinico.metadata @@ -0,0 +1,5 @@ +--- +count: 3 +name: Lorenzo Martinico +github: lzmartinico +--- diff --git a/contributors/matthew-healy.metadata b/contributors/matthew-healy.metadata new file mode 100644 index 00000000..21be6332 --- /dev/null +++ b/contributors/matthew-healy.metadata @@ -0,0 +1,5 @@ +--- +count: 3 +name: Matthew Healy +github: matthew-healy +--- diff --git a/contributors/mdimjasevic.metadata b/contributors/mdimjasevic.metadata new file mode 100644 index 00000000..456d05ea --- /dev/null +++ b/contributors/mdimjasevic.metadata @@ -0,0 +1,5 @@ +--- +count: 114 +name: Marko Dimjašević +github: mdimjasevic +--- diff --git a/contributors/mgttlinger.metadata b/contributors/mgttlinger.metadata new file mode 100644 index 00000000..6ee810e1 --- /dev/null +++ b/contributors/mgttlinger.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Merlin Göttlinger +github: mgttlinger +--- diff --git a/contributors/michel-steuwer.metadata b/contributors/michel-steuwer.metadata new file mode 100644 index 00000000..01919687 --- /dev/null +++ b/contributors/michel-steuwer.metadata @@ -0,0 +1,5 @@ +--- +count: 3 +name: Michel Steuwer +github: michel-steuwer +--- diff --git a/contributors/mietek.metadata b/contributors/mietek.metadata new file mode 100644 index 00000000..1548ccc8 --- /dev/null +++ b/contributors/mietek.metadata @@ -0,0 +1,5 @@ +--- +name: Miëtek Bak +github: mietek +count: 1 +--- diff --git a/contributors/moleike.metadata b/contributors/moleike.metadata new file mode 100644 index 00000000..95798392 --- /dev/null +++ b/contributors/moleike.metadata @@ -0,0 +1,5 @@ +--- +count: 2 +name: Alexandre Moreno +github: moleike +--- diff --git a/contributors/momirza.metadata b/contributors/momirza.metadata new file mode 100644 index 00000000..cfd5a793 --- /dev/null +++ b/contributors/momirza.metadata @@ -0,0 +1,5 @@ +--- +count: 7 +name: Mo Mirza +github: momirza +--- diff --git a/contributors/mreed20.metadata b/contributors/mreed20.metadata new file mode 100644 index 00000000..5c14d973 --- /dev/null +++ b/contributors/mreed20.metadata @@ -0,0 +1,5 @@ +--- +count: 19 +name: Michael Reed +github: mreed20 +--- diff --git a/contributors/murilogiacometti.metadata b/contributors/murilogiacometti.metadata new file mode 100644 index 00000000..19acb53a --- /dev/null +++ b/contributors/murilogiacometti.metadata @@ -0,0 +1,5 @@ +--- +count: 3 +name: Murilo Giacometti Rocha +github: murilogiacometti +--- diff --git a/contributors/nad.metadata b/contributors/nad.metadata new file mode 100644 index 00000000..056019e5 --- /dev/null +++ b/contributors/nad.metadata @@ -0,0 +1,5 @@ +--- +name: Nils Anders Danielsson +github: nad +count: 1 +--- diff --git a/contributors/navaati.metadata b/contributors/navaati.metadata new file mode 100644 index 00000000..a84e358e --- /dev/null +++ b/contributors/navaati.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Léo Gillot-Lamure +github: navaati +--- diff --git a/contributors/nyraghu.metadata b/contributors/nyraghu.metadata new file mode 100644 index 00000000..537eec65 --- /dev/null +++ b/contributors/nyraghu.metadata @@ -0,0 +1,5 @@ +--- +name: N. Raghavendra +github: nyraghu +count: 1 +--- diff --git a/contributors/odanoburu.metadata b/contributors/odanoburu.metadata new file mode 100644 index 00000000..c4a488f9 --- /dev/null +++ b/contributors/odanoburu.metadata @@ -0,0 +1,5 @@ +--- +count: 3 +name: bc² +github: odanoburu +--- diff --git a/contributors/omelkonian.metadata b/contributors/omelkonian.metadata new file mode 100644 index 00000000..feefed01 --- /dev/null +++ b/contributors/omelkonian.metadata @@ -0,0 +1,5 @@ +--- +count: 5 +name: Orestis Melkonian +github: omelkonian +--- diff --git a/contributors/pedrominicz.metadata b/contributors/pedrominicz.metadata new file mode 100644 index 00000000..fd59293d --- /dev/null +++ b/contributors/pedrominicz.metadata @@ -0,0 +1,5 @@ +--- +count: 4 +name: Pedro Minicz +github: pedrominicz +--- diff --git a/contributors/peterthiemann.metadata b/contributors/peterthiemann.metadata new file mode 100644 index 00000000..e491e638 --- /dev/null +++ b/contributors/peterthiemann.metadata @@ -0,0 +1,5 @@ +--- +count: 2 +name: Peter Thiemann +github: peterthiemann +--- diff --git a/contributors/phi16.metadata b/contributors/phi16.metadata new file mode 100644 index 00000000..4a3be502 --- /dev/null +++ b/contributors/phi16.metadata @@ -0,0 +1,5 @@ +--- +count: 4 +name: phi16 +github: phi16 +--- diff --git a/contributors/philderbeast.metadata b/contributors/philderbeast.metadata new file mode 100644 index 00000000..f52e849e --- /dev/null +++ b/contributors/philderbeast.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Phil de Joux +github: philderbeast +--- diff --git a/contributors/potato4444.metadata b/contributors/potato4444.metadata new file mode 100644 index 00000000..c79e67ee --- /dev/null +++ b/contributors/potato4444.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Nathaniel Carroll +github: potato4444 +--- diff --git a/contributors/purchan.metadata b/contributors/purchan.metadata new file mode 100644 index 00000000..2a5561e9 --- /dev/null +++ b/contributors/purchan.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: purchan +github: purchan +--- diff --git a/contributors/qaisjp.metadata b/contributors/qaisjp.metadata new file mode 100644 index 00000000..111ed077 --- /dev/null +++ b/contributors/qaisjp.metadata @@ -0,0 +1,5 @@ +--- +count: 5 +name: Qais Patankar +github: qaisjp +--- diff --git a/contributors/rodamber.metadata b/contributors/rodamber.metadata new file mode 100644 index 00000000..2e66fde1 --- /dev/null +++ b/contributors/rodamber.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Rodrigo Bernardo +github: rodamber +--- diff --git a/contributors/sabry.metadata b/contributors/sabry.metadata new file mode 100644 index 00000000..b9cb9cf1 --- /dev/null +++ b/contributors/sabry.metadata @@ -0,0 +1,5 @@ +--- +name: Amr Sabry +github: sabry +count: 1 +--- diff --git a/contributors/spwhitt.metadata b/contributors/spwhitt.metadata new file mode 100644 index 00000000..dce5b482 --- /dev/null +++ b/contributors/spwhitt.metadata @@ -0,0 +1,5 @@ +--- +count: 2 +name: Spencer Whitt +github: spwhitt +--- diff --git a/contributors/stepchowfun.metadata b/contributors/stepchowfun.metadata new file mode 100644 index 00000000..e8cd286c --- /dev/null +++ b/contributors/stepchowfun.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Stephan Boyer +github: stepchowfun +--- diff --git a/contributors/trajafri.metadata b/contributors/trajafri.metadata new file mode 100644 index 00000000..1da2cbcb --- /dev/null +++ b/contributors/trajafri.metadata @@ -0,0 +1,5 @@ +--- +count: 2 +name: Syed Turab Ali Jafri +github: trajafri +--- diff --git a/contributors/vikraman.metadata b/contributors/vikraman.metadata new file mode 100644 index 00000000..5385d9d6 --- /dev/null +++ b/contributors/vikraman.metadata @@ -0,0 +1,5 @@ +--- +name: Vikraman Choudhury +github: vikraman +count: 1 +--- diff --git a/contributors/vipo.metadata b/contributors/vipo.metadata new file mode 100644 index 00000000..51740680 --- /dev/null +++ b/contributors/vipo.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Slava +github: vipo +--- diff --git a/contributors/whxvd.metadata b/contributors/whxvd.metadata new file mode 100644 index 00000000..21bb2e95 --- /dev/null +++ b/contributors/whxvd.metadata @@ -0,0 +1,5 @@ +--- +count: 3 +name: Sebastian Miele +github: whxvd +--- diff --git a/contributors/ywata.metadata b/contributors/ywata.metadata new file mode 100644 index 00000000..338c3ca5 --- /dev/null +++ b/contributors/ywata.metadata @@ -0,0 +1,5 @@ +--- +count: 20 +name: Yasu Watanabe +github: ywata +--- diff --git a/contributors/zachrbrown.metadata b/contributors/zachrbrown.metadata new file mode 100644 index 00000000..0c0eeca2 --- /dev/null +++ b/contributors/zachrbrown.metadata @@ -0,0 +1,5 @@ +--- +count: 2 +name: Zach Brown +github: zachrbrown +--- diff --git a/contributors/zenzike.metadata b/contributors/zenzike.metadata new file mode 100644 index 00000000..6aff891a --- /dev/null +++ b/contributors/zenzike.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Nicolas Wu +github: zenzike +--- diff --git a/contributors/zgrannan.metadata b/contributors/zgrannan.metadata new file mode 100644 index 00000000..985b7af5 --- /dev/null +++ b/contributors/zgrannan.metadata @@ -0,0 +1,5 @@ +--- +count: 1 +name: Zack Grannan +github: zgrannan +--- diff --git a/courses/tspl/2019/Assignment2.lagda.md b/courses/tspl/2019/Assignment2.lagda.md index 1aa8d8e0..08d7c66e 100644 --- a/courses/tspl/2019/Assignment2.lagda.md +++ b/courses/tspl/2019/Assignment2.lagda.md @@ -81,7 +81,7 @@ Since we define equality here, any import would create a conflict. #### Exercise `≤-Reasoning` (stretch) The proof of monotonicity from -Chapter [Relations]({{ site.baseurl }}/Relations/) +Chapter [Relations](/Relations/) can be written in a more readable form by using an analogue of our notation for `≡-Reasoning`. Define `≤-Reasoning` analogously, and use it to write out an alternative proof that addition is monotonic with @@ -126,8 +126,8 @@ Show that equivalence is reflexive, symmetric, and transitive. #### Exercise `Bin-embedding` (stretch) {#Bin-embedding} Recall that Exercises -[Bin]({{ site.baseurl }}/Naturals/#Bin) and -[Bin-laws]({{ site.baseurl }}/Induction/#Bin-laws) +[Bin](/Naturals/#Bin) and +[Bin-laws](/Induction/#Bin-laws) define a datatype `Bin` of bitstrings representing natural numbers, and asks you to define the following functions and predicates: @@ -149,7 +149,7 @@ Why do `to` and `from` not form an isomorphism? #### Exercise `⇔≃×` (recommended) -Show that `A ⇔ B` as defined [earlier]({{ site.baseurl }}/Isomorphism/#iff) +Show that `A ⇔ B` as defined [earlier](/Isomorphism/#iff) is isomorphic to `(A → B) × (B → A)`. ``` @@ -221,7 +221,7 @@ Does the converse hold? If so, prove; if not, give a counterexample. #### Exercise `<-irreflexive` (recommended) Using negation, show that -[strict inequality]({{ site.baseurl }}/Relations/#strict-inequality) +[strict inequality](/Relations/#strict-inequality) is irreflexive, that is, `n < n` holds for no `n`. ``` @@ -232,7 +232,7 @@ is irreflexive, that is, `n < n` holds for no `n`. #### Exercise `trichotomy` (practice) Show that strict inequality satisfies -[trichotomy]({{ site.baseurl }}/Relations/#trichotomy), +[trichotomy](/Relations/#trichotomy), that is, for any naturals `m` and `n` exactly one of the following holds: * `m < n` @@ -310,7 +310,7 @@ postulate (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x) ``` Compare this with the result (`→-distrib-×`) in -Chapter [Connectives]({{ site.baseurl }}/Connectives/). +Chapter [Connectives](/Connectives/). #### Exercise `⊎∀-implies-∀⊎` (practice) @@ -400,9 +400,9 @@ Does the converse hold? If so, prove; if not, explain why. #### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism} Recall that Exercises -[Bin]({{ site.baseurl }}/Naturals/#Bin), -[Bin-laws]({{ site.baseurl }}/Induction/#Bin-laws), and -[Bin-predicates]({{ site.baseurl }}/Relations/#Bin-predicates) +[Bin](/Naturals/#Bin), +[Bin-laws](/Induction/#Bin-laws), and +[Bin-predicates](/Relations/#Bin-predicates) define a datatype `Bin` of bitstrings representing natural numbers, and asks you to define the following functions and predicates: @@ -469,7 +469,7 @@ postulate #### Exercise `iff-erasure` (recommended) Give analogues of the `_⇔_` operation from -Chapter [Isomorphism]({{ site.baseurl }}/Isomorphism/#iff), +Chapter [Isomorphism](/Isomorphism/#iff), operation on booleans and decidables, and also show the corresponding erasure: ``` postulate diff --git a/courses/tspl/2019/Assignment3.lagda.md b/courses/tspl/2019/Assignment3.lagda.md index 5c7c73e2..55f54e72 100644 --- a/courses/tspl/2019/Assignment3.lagda.md +++ b/courses/tspl/2019/Assignment3.lagda.md @@ -238,7 +238,7 @@ Show that `Any` and `All` satisfy a version of De Morgan's Law: (Can you see why it is important that here `_∘_` is generalised to arbitrary levels, as described in the section on -[universe polymorphism]({{ site.baseurl }}/Equality/#unipoly)?) +[universe polymorphism](/Equality/#unipoly)?) Do we also have the following? diff --git a/courses/tspl/2019/tspl2019.md b/courses/tspl/2019/tspl2019.md index 842e4154..7a5cc211 100644 --- a/courses/tspl/2019/tspl2019.md +++ b/courses/tspl/2019/tspl2019.md @@ -27,9 +27,9 @@ Lectures take place Monday, Wednesday, and Friday in AT 5.07. 1 - 16 Sep Naturals - 18 Sep Induction - 20 Sep Relations + 16 Sep Naturals + 18 Sep Induction + 20 Sep Relations 2 @@ -39,34 +39,34 @@ Lectures take place Monday, Wednesday, and Friday in AT 5.07. 3 - 30 Sep Equality & - Isomorphism - 2 Oct Connectives - 4 Oct Negation + 30 Sep Equality & + Isomorphism + 2 Oct Connectives + 4 Oct Negation 4 - 7 Oct Quantifiers - 9 Oct Decidable + 7 Oct Quantifiers + 9 Oct Decidable 11 Oct (tutorial only, 10.00–10.50) 5 - 14 Oct Lists - 16 Oct Lambda - 18 Oct Lambda and - Properties + 14 Oct Lists + 16 Oct Lambda + 18 Oct Lambda and + Properties 6 - 21 Oct Properties - 23 Oct DeBruijn - 25 Oct More + 21 Oct Properties + 23 Oct DeBruijn + 25 Oct More 7 - 28 Oct Inference - 30 Oct Untyped + 28 Oct Inference + 30 Oct Untyped 1 Nov (no class) @@ -117,14 +117,14 @@ courses where there are easier marks to be had. ## Coursework -For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.baseurl }}/GettingStarted/). +For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/). -* [Assignment 1]({{ site.baseurl }}/TSPL/2019/Assignment1/) cw1 due 4pm Thursday 3 October (Week 3) -* [Assignment 2]({{ site.baseurl }}/TSPL/2019/Assignment2/) cw2 due 4pm Thursday 17 October (Week 5) -* [Assignment 3]({{ site.baseurl }}/TSPL/2019/Assignment3/) cw3 due 4pm Thursday 31 October (Week 7) -* [Assignment 4]({{ site.baseurl }}/TSPL/2019/Assignment4/) cw4 due 4pm Thursday 14 November (Week 9) -* [Assignment 5]({{ site.baseurl }}/courses/tspl/2019/Mock1.pdf) cw5 due 4pm Thursday 21 November (Week 10)
- Use file [Exam]({{ site.baseurl }}/TSPL/2019/Exam/). Despite the rubric, do **all three questions**. +* [Assignment 1](/TSPL/2019/Assignment1/) cw1 due 4pm Thursday 3 October (Week 3) +* [Assignment 2](/TSPL/2019/Assignment2/) cw2 due 4pm Thursday 17 October (Week 5) +* [Assignment 3](/TSPL/2019/Assignment3/) cw3 due 4pm Thursday 31 October (Week 7) +* [Assignment 4](/TSPL/2019/Assignment4/) cw4 due 4pm Thursday 14 November (Week 9) +* [Assignment 5](/courses/tspl/2019/Mock1.pdf) cw5 due 4pm Thursday 21 November (Week 10)
+ Use file [Exam](/TSPL/2019/Exam/). Despite the rubric, do **all three questions**. Assignments are submitted by running @@ -192,7 +192,7 @@ Please do so by 4pm Thursday 31 October. ## Mock exam -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). +Here is the text of the [second mock](/courses/tspl/2018/Mock2.pdf) +and the exam [instructions](/courses/tspl/2018/Instructions.pdf). --> diff --git a/_sass/agda.scss b/css/agda.css similarity index 99% rename from _sass/agda.scss rename to css/agda.css index 6165a2b8..2d7eb61f 100644 --- a/_sass/agda.scss +++ b/css/agda.css @@ -1,4 +1,3 @@ -// Define variables for code formatting @font-face { font-family: 'mononoki'; src: url('fonts/mononoki.woff2') format('woff2'), @@ -32,6 +31,9 @@ } /* Code. */ +pre { + break-inside: avoid; +} pre.highlight { @include code-container; border-style: dashed !important; diff --git a/css/contributors.css b/css/contributors.css new file mode 100644 index 00000000..c24c62d8 --- /dev/null +++ b/css/contributors.css @@ -0,0 +1,8 @@ +.list-of-contributors ul { + display: grid; + grid-template-columns: repeat(3, 1fr); + width: calc(100% - 2rem); +} +.list-of-contributors ul li { + margin-right: 2rem; +} diff --git a/epub/main.css b/css/epub.css similarity index 100% rename from epub/main.css rename to css/epub.css diff --git a/css/minima.scss b/css/minima.scss new file mode 100644 index 00000000..b5b5b84c --- /dev/null +++ b/css/minima.scss @@ -0,0 +1,4 @@ +@import + "minima/skins/classic", + "minima/initialize" +; diff --git a/css/minima/_base.scss b/css/minima/_base.scss new file mode 100755 index 00000000..a6f104e4 --- /dev/null +++ b/css/minima/_base.scss @@ -0,0 +1,282 @@ +html { + font-size: $base-font-size; +} + +/** + * Reset some basic elements + */ +body, h1, h2, h3, h4, h5, h6, +p, blockquote, pre, hr, +dl, dd, ol, ul, figure { + margin: 0; + padding: 0; + +} + + + +/** + * Basic styling + */ +body { + font: $base-font-weight #{$base-font-size}/#{$base-line-height} $base-font-family; + color: $text-color; + background-color: $background-color; + -webkit-text-size-adjust: 100%; + -webkit-font-feature-settings: "kern" 1; + -moz-font-feature-settings: "kern" 1; + -o-font-feature-settings: "kern" 1; + font-feature-settings: "kern" 1; + font-kerning: normal; + display: flex; + min-height: 100vh; + flex-direction: column; + overflow-wrap: break-word; +} + + + +/** + * Set `margin-bottom` to maintain vertical rhythm + */ +h1, h2, h3, h4, h5, h6, +p, blockquote, pre, +ul, ol, dl, figure, +%vertical-rhythm { + margin-bottom: $spacing-unit / 2; +} + +hr { + margin-top: $spacing-unit; + margin-bottom: $spacing-unit; +} + +/** + * `main` element + */ +main { + display: block; /* Default value of `display` of `main` element is 'inline' in IE 11. */ +} + + + +/** + * Images + */ +img { + max-width: 100%; + vertical-align: middle; +} + + + +/** + * Figures + */ +figure > img { + display: block; +} + +figcaption { + font-size: $small-font-size; +} + + + +/** + * Lists + */ +ul, ol { + margin-left: $spacing-unit; +} + +li { + > ul, + > ol { + margin-bottom: 0; + } +} + + + +/** + * Headings + */ +h1, h2, h3, h4, h5, h6 { + font-weight: $base-font-weight; +} + + + +/** + * Links + */ +a { + color: $link-base-color; + text-decoration: none; + + &:visited { + color: $link-visited-color; + } + + &:hover { + color: $link-hover-color; + text-decoration: underline; + } + + .social-media-list &:hover { + text-decoration: none; + + .username { + text-decoration: underline; + } + } +} + + +/** + * Blockquotes + */ +blockquote { + color: $brand-color; + border-left: 4px solid $border-color-01; + padding-left: $spacing-unit / 2; + @include relative-font-size(1.125); + font-style: italic; + + > :last-child { + margin-bottom: 0; + } + + i, em { + font-style: normal; + } +} + + + +/** + * Code formatting + */ +pre, +code { + font-family: $code-font-family; + font-size: 0.9375em; + border: 1px solid $border-color-01; + border-radius: 3px; + background-color: $code-background-color; +} + +code { + padding: 1px 5px; +} + +pre { + padding: 8px 12px; + overflow-x: auto; + + > code { + border: 0; + padding-right: 0; + padding-left: 0; + } +} + +.highlight { + border-radius: 3px; + background: $code-background-color; + @extend %vertical-rhythm; + + .highlighter-rouge & { + background: $code-background-color; + } +} + + + +/** + * Wrapper + */ +.wrapper { + max-width: calc(#{$content-width} - (#{$spacing-unit})); + margin-right: auto; + margin-left: auto; + padding-right: $spacing-unit / 2; + padding-left: $spacing-unit / 2; + @extend %clearfix; + + @media screen and (min-width: $on-large) { + max-width: calc(#{$content-width} - (#{$spacing-unit} * 2)); + padding-right: $spacing-unit; + padding-left: $spacing-unit; + } +} + + + +/** + * Clearfix + */ +%clearfix:after { + content: ""; + display: table; + clear: both; +} + + + +/** + * Icons + */ + +.orange { + color: #f66a0a; +} + +.grey { + color: #828282; +} + +.svg-icon { + width: 16px; + height: 16px; + display: inline-block; + fill: currentColor; + padding: 5px 3px 2px 5px; + vertical-align: text-bottom; +} + + +/** + * Tables + */ +table { + margin-bottom: $spacing-unit; + width: 100%; + text-align: $table-text-align; + color: $table-text-color; + border-collapse: collapse; + border: 1px solid $table-border-color; + tr { + &:nth-child(even) { + background-color: $table-zebra-color; + } + } + th, td { + padding: ($spacing-unit / 3) ($spacing-unit / 2); + } + th { + background-color: $table-header-bg-color; + border: 1px solid $table-header-border; + } + td { + border: 1px solid $table-border-color; + } + + @include media-query($on-laptop) { + display: block; + overflow-x: auto; + -webkit-overflow-scrolling: touch; + -ms-overflow-style: -ms-autohiding-scrollbar; + } +} diff --git a/css/minima/_layout.scss b/css/minima/_layout.scss new file mode 100755 index 00000000..c1efe770 --- /dev/null +++ b/css/minima/_layout.scss @@ -0,0 +1,337 @@ +/** + * Site header + */ +.site-header { + border-top: 5px solid $border-color-03; + border-bottom: 1px solid $border-color-01; + min-height: $spacing-unit * 1.865; + line-height: $base-line-height * $base-font-size * 2.25; + + // Positioning context for the mobile navigation icon + position: relative; +} + +.site-title { + @include relative-font-size(1.625); + font-weight: 300; + letter-spacing: -1px; + margin-bottom: 0; + float: left; + + @include media-query($on-palm) { + padding-right: 45px; + } + + &, + &:visited { + color: $site-title-color; + } +} + +.site-nav { + position: absolute; + top: 9px; + right: $spacing-unit / 2; + background-color: $background-color; + border: 1px solid $border-color-01; + border-radius: 5px; + text-align: right; + + .nav-trigger { + display: none; + } + + .menu-icon { + float: right; + width: 36px; + height: 26px; + line-height: 0; + padding-top: 10px; + text-align: center; + + > svg path { + fill: $border-color-03; + } + } + + label[for="nav-trigger"] { + display: block; + float: right; + width: 36px; + height: 36px; + z-index: 2; + cursor: pointer; + } + + input ~ .trigger { + clear: both; + display: none; + } + + input:checked ~ .trigger { + display: block; + padding-bottom: 5px; + } + + .page-link { + color: $text-color; + line-height: $base-line-height; + display: block; + padding: 5px 10px; + + // Gaps between nav items, but not on the last one + &:not(:last-child) { + margin-right: 0; + } + margin-left: 20px; + } + + @media screen and (min-width: $on-medium) { + position: static; + float: right; + border: none; + background-color: inherit; + + label[for="nav-trigger"] { + display: none; + } + + .menu-icon { + display: none; + } + + input ~ .trigger { + display: block; + } + + .page-link { + display: inline; + padding: 0; + + &:not(:last-child) { + margin-right: 20px; + } + margin-left: auto; + } + } +} + + + +/** + * Site footer + */ +.site-footer { + border-top: 1px solid $border-color-01; + padding: $spacing-unit 0; +} + +.footer-heading { + @include relative-font-size(1.125); + margin-bottom: $spacing-unit / 2; +} + +.feed-subscribe .svg-icon { + padding: 5px 5px 2px 0 +} + +.contact-list, +.social-media-list { + list-style: none; + margin-left: 0; +} + +.footer-col-wrapper, +.social-links { + @include relative-font-size(0.9375); + color: $brand-color; +} + +.footer-col { + margin-bottom: $spacing-unit / 2; +} + +.footer-col-1, +.footer-col-2 { + width: calc(50% - (#{$spacing-unit} / 2)); +} + +.footer-col-3 { + width: calc(100% - (#{$spacing-unit} / 2)); +} + +@media screen and (min-width: $on-large) { + .footer-col-1 { + width: calc(35% - (#{$spacing-unit} / 2)); + } + + .footer-col-2 { + width: calc(20% - (#{$spacing-unit} / 2)); + } + + .footer-col-3 { + width: calc(45% - (#{$spacing-unit} / 2)); + } +} + +@media screen and (min-width: $on-medium) { + .footer-col-wrapper { + display: flex + } + + .footer-col { + width: calc(100% - (#{$spacing-unit} / 2)); + padding: 0 ($spacing-unit / 2); + + &:first-child { + padding-right: $spacing-unit / 2; + padding-left: 0; + } + + &:last-child { + padding-right: 0; + padding-left: $spacing-unit / 2; + } + } +} + + + +/** + * Page content + */ +.page-content { + padding: $spacing-unit 0; + flex: 1 0 auto; +} + +.page-heading { + @include relative-font-size(2); +} + +.post-list-heading { + @include relative-font-size(1.75); +} + +.post-list { + margin-left: 0; + list-style: none; + + > li { + margin-bottom: $spacing-unit; + } +} + +.post-meta { + font-size: $small-font-size; + color: $brand-color; +} + +.post-link { + display: block; + @include relative-font-size(1.5); +} + + + +/** + * Posts + */ +.post-header { + margin-bottom: $spacing-unit; +} + +.post-title, +.post-content h1 { + @include relative-font-size(2.625); + letter-spacing: -1px; + line-height: 1.15; + + @media screen and (min-width: $on-large) { + @include relative-font-size(2.625); + } +} + +.post-content { + margin-bottom: $spacing-unit; + + h1, h2, h3 { margin-top: $spacing-unit * 2 } + h4, h5, h6 { margin-top: $spacing-unit } + + h2 { + @include relative-font-size(1.75); + + @media screen and (min-width: $on-large) { + @include relative-font-size(2); + } + } + + h3 { + @include relative-font-size(1.375); + + @media screen and (min-width: $on-large) { + @include relative-font-size(1.625); + } + } + + h4 { + @include relative-font-size(1.25); + } + + h5 { + @include relative-font-size(1.125); + } + h6 { + @include relative-font-size(1.0625); + } +} + + +.social-media-list { + display: table; + li { + float: left; + margin: 5px 10px 5px 0; + &:last-of-type { margin-right: 0 } + a { + display: block; + padding: $spacing-unit / 4; + border: 1px solid $border-color-01; + &:hover { border-color: $border-color-02 } + } + } +} + + + +/** + * Pagination navbar + */ +.pager { + .pagination { + display: flex; + justify-content: center; + list-style: none; + li { + margin: 5px 10px 5px 0; + } + li.page-link:last-of-type { + margin-right: 0; + } + li.separator:last-of-type { + display: none; + } + } +} + + + +/** + * Grid helpers + */ +@media screen and (min-width: $on-large) { + .one-half { + width: calc(50% - (#{$spacing-unit} / 2)); + } +} + diff --git a/css/minima/custom-styles.scss b/css/minima/custom-styles.scss new file mode 100755 index 00000000..7c1417ff --- /dev/null +++ b/css/minima/custom-styles.scss @@ -0,0 +1,2 @@ +// Placeholder to allow defining custom styles that override everything else. +// (Use `_sass/minima/custom-variables.scss` to override variable defaults) diff --git a/css/minima/custom-variables.scss b/css/minima/custom-variables.scss new file mode 100755 index 00000000..2a2d0fa4 --- /dev/null +++ b/css/minima/custom-variables.scss @@ -0,0 +1 @@ +// Placeholder to allow overriding predefined variables smoothly. diff --git a/css/minima/initialize.scss b/css/minima/initialize.scss new file mode 100755 index 00000000..1f1e739b --- /dev/null +++ b/css/minima/initialize.scss @@ -0,0 +1,50 @@ +@charset "utf-8"; + +// Define defaults for each variable. + +$base-font-family: -apple-system, BlinkMacSystemFont, "Segoe UI", "Segoe UI Symbol", "Segoe UI Emoji", "Apple Color Emoji", Roboto, Helvetica, Arial, sans-serif !default; +$code-font-family: "Menlo", "Inconsolata", "Consolas", "Roboto Mono", "Ubuntu Mono", "Liberation Mono", "Courier New", monospace; +$base-font-size: 16px !default; +$base-font-weight: 400 !default; +$small-font-size: $base-font-size * 0.875 !default; +$base-line-height: 1.5 !default; + +$spacing-unit: 15px !default; + +$table-text-align: left !default; + +// Width of the content area +$content-width: 800px !default; + +$on-palm: 600px !default; +$on-laptop: 800px !default; + +$on-medium: $on-palm !default; +$on-large: $on-laptop !default; + +// Use media queries like this: +// @include media-query($on-palm) { +// .wrapper { +// padding-right: $spacing-unit / 2; +// padding-left: $spacing-unit / 2; +// } +// } +// Notice the following mixin uses max-width, in a deprecated, desktop-first +// approach, whereas media queries used elsewhere now use min-width. +@mixin media-query($device) { + @media screen and (max-width: $device) { + @content; + } +} + +@mixin relative-font-size($ratio) { + font-size: #{$ratio}rem; +} + +// Import pre-styling-overrides hook and style-partials. +@import + "minima/custom-variables", // Hook to override predefined variables. + "minima/base", // Defines element resets. + "minima/layout", // Defines structure and style based on CSS selectors. + "minima/custom-styles" // Hook to override existing styles. +; diff --git a/css/minima/skins/classic.scss b/css/minima/skins/classic.scss new file mode 100755 index 00000000..c6dc2929 --- /dev/null +++ b/css/minima/skins/classic.scss @@ -0,0 +1,91 @@ +@charset "utf-8"; + +$brand-color: #828282 !default; +$brand-color-light: lighten($brand-color, 40%) !default; +$brand-color-dark: darken($brand-color, 25%) !default; + +$site-title-color: $brand-color-dark !default; + +$text-color: #111111 !default; +$background-color: #fdfdfd !default; +$code-background-color: #eeeeff !default; + +$link-base-color: #2a7ae2 !default; +$link-visited-color: darken($link-base-color, 15%) !default; +$link-hover-color: $text-color !default; + +$border-color-01: $brand-color-light !default; +$border-color-02: lighten($brand-color, 35%) !default; +$border-color-03: $brand-color-dark !default; + +$table-text-color: lighten($text-color, 18%) !default; +$table-zebra-color: lighten($brand-color, 46%) !default; +$table-header-bg-color: lighten($brand-color, 43%) !default; +$table-header-border: lighten($brand-color, 37%) !default; +$table-border-color: $border-color-01 !default; + + +// Syntax highlighting styles should be adjusted appropriately for every "skin" +// ---------------------------------------------------------------------------- + +.highlight { + .c { color: #998; font-style: italic } // Comment + .err { color: #a61717; background-color: #e3d2d2 } // Error + .k { font-weight: bold } // Keyword + .o { font-weight: bold } // Operator + .cm { color: #998; font-style: italic } // Comment.Multiline + .cp { color: #999; font-weight: bold } // Comment.Preproc + .c1 { color: #998; font-style: italic } // Comment.Single + .cs { color: #999; font-weight: bold; font-style: italic } // Comment.Special + .gd { color: #000; background-color: #fdd } // Generic.Deleted + .gd .x { color: #000; background-color: #faa } // Generic.Deleted.Specific + .ge { font-style: italic } // Generic.Emph + .gr { color: #a00 } // Generic.Error + .gh { color: #999 } // Generic.Heading + .gi { color: #000; background-color: #dfd } // Generic.Inserted + .gi .x { color: #000; background-color: #afa } // Generic.Inserted.Specific + .go { color: #888 } // Generic.Output + .gp { color: #555 } // Generic.Prompt + .gs { font-weight: bold } // Generic.Strong + .gu { color: #aaa } // Generic.Subheading + .gt { color: #a00 } // Generic.Traceback + .kc { font-weight: bold } // Keyword.Constant + .kd { font-weight: bold } // Keyword.Declaration + .kp { font-weight: bold } // Keyword.Pseudo + .kr { font-weight: bold } // Keyword.Reserved + .kt { color: #458; font-weight: bold } // Keyword.Type + .m { color: #099 } // Literal.Number + .s { color: #d14 } // Literal.String + .na { color: #008080 } // Name.Attribute + .nb { color: #0086B3 } // Name.Builtin + .nc { color: #458; font-weight: bold } // Name.Class + .no { color: #008080 } // Name.Constant + .ni { color: #800080 } // Name.Entity + .ne { color: #900; font-weight: bold } // Name.Exception + .nf { color: #900; font-weight: bold } // Name.Function + .nn { color: #555 } // Name.Namespace + .nt { color: #000080 } // Name.Tag + .nv { color: #008080 } // Name.Variable + .ow { font-weight: bold } // Operator.Word + .w { color: #bbb } // Text.Whitespace + .mf { color: #099 } // Literal.Number.Float + .mh { color: #099 } // Literal.Number.Hex + .mi { color: #099 } // Literal.Number.Integer + .mo { color: #099 } // Literal.Number.Oct + .sb { color: #d14 } // Literal.String.Backtick + .sc { color: #d14 } // Literal.String.Char + .sd { color: #d14 } // Literal.String.Doc + .s2 { color: #d14 } // Literal.String.Double + .se { color: #d14 } // Literal.String.Escape + .sh { color: #d14 } // Literal.String.Heredoc + .si { color: #d14 } // Literal.String.Interpol + .sx { color: #d14 } // Literal.String.Other + .sr { color: #009926 } // Literal.String.Regex + .s1 { color: #d14 } // Literal.String.Single + .ss { color: #990073 } // Literal.String.Symbol + .bp { color: #999 } // Name.Builtin.Pseudo + .vc { color: #008080 } // Name.Variable.Class + .vg { color: #008080 } // Name.Variable.Global + .vi { color: #008080 } // Name.Variable.Instance + .il { color: #099 } // Literal.Number.Integer.Long +} diff --git a/css/minima/skins/dark.scss b/css/minima/skins/dark.scss new file mode 100755 index 00000000..39b893fa --- /dev/null +++ b/css/minima/skins/dark.scss @@ -0,0 +1,95 @@ +@charset "utf-8"; + +$brand-color: #999999 !default; +$brand-color-light: lighten($brand-color, 5%) !default; +$brand-color-dark: darken($brand-color, 35%) !default; + +$site-title-color: $brand-color-light !default; + +$text-color: #bbbbbb !default; +$background-color: #181818 !default; +$code-background-color: #212121 !default; + +$link-base-color: #79b8ff !default; +$link-visited-color: $link-base-color !default; +$link-hover-color: $text-color !default; + +$border-color-01: $brand-color-dark !default; +$border-color-02: $brand-color-light !default; +$border-color-03: $brand-color !default; + +$table-text-color: $text-color !default; +$table-zebra-color: lighten($background-color, 4%) !default; +$table-header-bg-color: lighten($background-color, 10%) !default; +$table-header-border: lighten($background-color, 21%) !default; +$table-border-color: $border-color-01 !default; + + +// Syntax highlighting styles should be adjusted appropriately for every "skin" +// List of tokens: https://github.com/rouge-ruby/rouge/wiki/List-of-tokens +// Some colors come from Material Theme Darker: +// https://github.com/material-theme/vsc-material-theme/blob/master/scripts/generator/settings/specific/darker-hc.ts +// https://github.com/material-theme/vsc-material-theme/blob/master/scripts/generator/color-set.ts +// ---------------------------------------------------------------------------- + +.highlight { + .c { color: #545454; font-style: italic } // Comment + .err { color: #f07178; background-color: #e3d2d2 } // Error + .k { color: #89DDFF; font-weight: bold } // Keyword + .o { font-weight: bold } // Operator + .cm { color: #545454; font-style: italic } // Comment.Multiline + .cp { color: #545454; font-weight: bold } // Comment.Preproc + .c1 { color: #545454; font-style: italic } // Comment.Single + .cs { color: #545454; font-weight: bold; font-style: italic } // Comment.Special + .gd { color: #000; background-color: #fdd } // Generic.Deleted + .gd .x { color: #000; background-color: #faa } // Generic.Deleted.Specific + .ge { font-style: italic } // Generic.Emph + .gr { color: #f07178 } // Generic.Error + .gh { color: #999 } // Generic.Heading + .gi { color: #000; background-color: #dfd } // Generic.Inserted + .gi .x { color: #000; background-color: #afa } // Generic.Inserted.Specific + .go { color: #888 } // Generic.Output + .gp { color: #555 } // Generic.Prompt + .gs { font-weight: bold } // Generic.Strong + .gu { color: #aaa } // Generic.Subheading + .gt { color: #f07178 } // Generic.Traceback + .kc { font-weight: bold } // Keyword.Constant + .kd { font-weight: bold } // Keyword.Declaration + .kp { font-weight: bold } // Keyword.Pseudo + .kr { font-weight: bold } // Keyword.Reserved + .kt { color: #FFCB6B; font-weight: bold } // Keyword.Type + .m { color: #F78C6C } // Literal.Number + .s { color: #C3E88D } // Literal.String + .na { color: #008080 } // Name.Attribute + .nb { color: #EEFFFF } // Name.Builtin + .nc { color: #FFCB6B; font-weight: bold } // Name.Class + .no { color: #008080 } // Name.Constant + .ni { color: #800080 } // Name.Entity + .ne { color: #900; font-weight: bold } // Name.Exception + .nf { color: #82AAFF; font-weight: bold } // Name.Function + .nn { color: #555 } // Name.Namespace + .nt { color: #FFCB6B } // Name.Tag + .nv { color: #EEFFFF } // Name.Variable + .ow { font-weight: bold } // Operator.Word + .w { color: #EEFFFF } // Text.Whitespace + .mf { color: #F78C6C } // Literal.Number.Float + .mh { color: #F78C6C } // Literal.Number.Hex + .mi { color: #F78C6C } // Literal.Number.Integer + .mo { color: #F78C6C } // Literal.Number.Oct + .sb { color: #C3E88D } // Literal.String.Backtick + .sc { color: #C3E88D } // Literal.String.Char + .sd { color: #C3E88D } // Literal.String.Doc + .s2 { color: #C3E88D } // Literal.String.Double + .se { color: #EEFFFF } // Literal.String.Escape + .sh { color: #C3E88D } // Literal.String.Heredoc + .si { color: #C3E88D } // Literal.String.Interpol + .sx { color: #C3E88D } // Literal.String.Other + .sr { color: #C3E88D } // Literal.String.Regex + .s1 { color: #C3E88D } // Literal.String.Single + .ss { color: #C3E88D } // Literal.String.Symbol + .bp { color: #999 } // Name.Builtin.Pseudo + .vc { color: #FFCB6B } // Name.Variable.Class + .vg { color: #EEFFFF } // Name.Variable.Global + .vi { color: #EEFFFF } // Name.Variable.Instance + .il { color: #F78C6C } // Literal.Number.Integer.Long +} diff --git a/css/minima/skins/solarized-dark.scss b/css/minima/skins/solarized-dark.scss new file mode 100755 index 00000000..f3b1f387 --- /dev/null +++ b/css/minima/skins/solarized-dark.scss @@ -0,0 +1,4 @@ +@charset "utf-8"; + +$sol-is-dark: true; +@import "minima/skins/solarized"; diff --git a/css/minima/skins/solarized.scss b/css/minima/skins/solarized.scss new file mode 100755 index 00000000..6253d696 --- /dev/null +++ b/css/minima/skins/solarized.scss @@ -0,0 +1,140 @@ +@charset "utf-8"; + +// Solarized skin +// ============== +// Created by Sander Voerman using the Solarized +// color scheme by Ethan Schoonover . + +// This style sheet implements two options for the minima.skin setting: +// "solarized" for light mode and "solarized-dark" for dark mode. +$sol-is-dark: false !default; + + +// Color scheme +// ------------ +// The inline comments show the canonical L*a*b values for each color. + +$sol-base03: #002b36; // 15 -12 -12 +$sol-base02: #073642; // 20 -12 -12 +$sol-base01: #586e75; // 45 -07 -07 +$sol-base00: #657b83; // 50 -07 -07 +$sol-base0: #839496; // 60 -06 -03 +$sol-base1: #93a1a1; // 65 -05 -02 +$sol-base2: #eee8d5; // 92 -00 10 +$sol-base3: #fdf6e3; // 97 00 10 +$sol-yellow: #b58900; // 60 10 65 +$sol-orange: #cb4b16; // 50 50 55 +$sol-red: #dc322f; // 50 65 45 +$sol-magenta: #d33682; // 50 65 -05 +$sol-violet: #6c71c4; // 50 15 -45 +$sol-blue: #268bd2; // 55 -10 -45 +$sol-cyan: #2aa198; // 60 -35 -05 +$sol-green: #859900; // 60 -20 65 + +$sol-mono3: $sol-base3; +$sol-mono2: $sol-base2; +$sol-mono1: $sol-base1; +$sol-mono00: $sol-base00; +$sol-mono01: $sol-base01; + +@if $sol-is-dark { + $sol-mono3: $sol-base03; + $sol-mono2: $sol-base02; + $sol-mono1: $sol-base01; + $sol-mono00: $sol-base0; + $sol-mono01: $sol-base1; +} + + +// Minima color variables +// ---------------------- + +$brand-color: $sol-mono1 !default; +$brand-color-light: mix($sol-mono1, $sol-mono3) !default; +$brand-color-dark: $sol-mono00 !default; + +$site-title-color: $sol-mono00 !default; + +$text-color: $sol-mono01 !default; +$background-color: $sol-mono3 !default; +$code-background-color: $sol-mono2 !default; + +$link-base-color: $sol-blue !default; +$link-visited-color: mix($sol-blue, $sol-mono00) !default; +$link-hover-color: $sol-mono00 !default; + +$border-color-01: $brand-color-light !default; +$border-color-02: $sol-mono1 !default; +$border-color-03: $sol-mono00 !default; + +$table-text-color: $sol-mono00 !default; +$table-zebra-color: mix($sol-mono2, $sol-mono3) !default; +$table-header-bg-color: $sol-mono2 !default; +$table-header-border: $sol-mono1 !default; +$table-border-color: $sol-mono1 !default; + + +// Syntax highlighting styles +// -------------------------- + +.highlight { + .c { color: $sol-mono1; font-style: italic } // Comment + .err { color: $sol-red } // Error + .k { color: $sol-mono01; font-weight: bold } // Keyword + .o { color: $sol-mono01; font-weight: bold } // Operator + .cm { color: $sol-mono1; font-style: italic } // Comment.Multiline + .cp { color: $sol-mono1; font-weight: bold } // Comment.Preproc + .c1 { color: $sol-mono1; font-style: italic } // Comment.Single + .cs { color: $sol-mono1; font-weight: bold; font-style: italic } // Comment.Special + .gd { color: $sol-red } // Generic.Deleted + .gd .x { color: $sol-red } // Generic.Deleted.Specific + .ge { color: $sol-mono00; font-style: italic } // Generic.Emph + .gr { color: $sol-red } // Generic.Error + .gh { color: $sol-mono1 } // Generic.Heading + .gi { color: $sol-green } // Generic.Inserted + .gi .x { color: $sol-green } // Generic.Inserted.Specific + .go { color: $sol-mono00 } // Generic.Output + .gp { color: $sol-mono00 } // Generic.Prompt + .gs { color: $sol-mono01; font-weight: bold } // Generic.Strong + .gu { color: $sol-mono1 } // Generic.Subheading + .gt { color: $sol-red } // Generic.Traceback + .kc { color: $sol-mono01; font-weight: bold } // Keyword.Constant + .kd { color: $sol-mono01; font-weight: bold } // Keyword.Declaration + .kp { color: $sol-mono01; font-weight: bold } // Keyword.Pseudo + .kr { color: $sol-mono01; font-weight: bold } // Keyword.Reserved + .kt { color: $sol-violet; font-weight: bold } // Keyword.Type + .m { color: $sol-cyan } // Literal.Number + .s { color: $sol-magenta } // Literal.String + .na { color: $sol-cyan } // Name.Attribute + .nb { color: $sol-blue } // Name.Builtin + .nc { color: $sol-violet; font-weight: bold } // Name.Class + .no { color: $sol-cyan } // Name.Constant + .ni { color: $sol-violet } // Name.Entity + .ne { color: $sol-violet; font-weight: bold } // Name.Exception + .nf { color: $sol-blue; font-weight: bold } // Name.Function + .nn { color: $sol-mono00 } // Name.Namespace + .nt { color: $sol-blue } // Name.Tag + .nv { color: $sol-cyan } // Name.Variable + .ow { color: $sol-mono01; font-weight: bold } // Operator.Word + .w { color: $sol-mono1 } // Text.Whitespace + .mf { color: $sol-cyan } // Literal.Number.Float + .mh { color: $sol-cyan } // Literal.Number.Hex + .mi { color: $sol-cyan } // Literal.Number.Integer + .mo { color: $sol-cyan } // Literal.Number.Oct + .sb { color: $sol-magenta } // Literal.String.Backtick + .sc { color: $sol-magenta } // Literal.String.Char + .sd { color: $sol-magenta } // Literal.String.Doc + .s2 { color: $sol-magenta } // Literal.String.Double + .se { color: $sol-magenta } // Literal.String.Escape + .sh { color: $sol-magenta } // Literal.String.Heredoc + .si { color: $sol-magenta } // Literal.String.Interpol + .sx { color: $sol-magenta } // Literal.String.Other + .sr { color: $sol-green } // Literal.String.Regex + .s1 { color: $sol-magenta } // Literal.String.Single + .ss { color: $sol-magenta } // Literal.String.Symbol + .bp { color: $sol-mono1 } // Name.Builtin.Pseudo + .vc { color: $sol-cyan } // Name.Variable.Class + .vg { color: $sol-cyan } // Name.Variable.Global + .vi { color: $sol-cyan } // Name.Variable.Instance + .il { color: $sol-cyan } // Literal.Number.Integer.Long +} diff --git a/css/pagination.css b/css/pagination.css new file mode 100644 index 00000000..e69de29b diff --git a/epub/index.md b/epub/index.md deleted file mode 100644 index 56760534..00000000 --- a/epub/index.md +++ /dev/null @@ -1,72 +0,0 @@ ---- -title: Programming Language Foundations in Agda -author: -- Philip Wadler -- Wen Kokke -- Jeremy G. Siek -description: This book is an introduction to programming language theory using the proof assistant Agda. -rights: Creative Commons Attribution 4.0 International License -language: en-US ---- - -# Front matter - -``` {.include shift-heading-level-by=1} -src/plfa/dedication.md -src/plfa/preface.md -``` - -# Part 1: Logical Foundations - -``` {.include shift-heading-level-by=1} -src/plfa/part1/Naturals.lagda.md -src/plfa/part1/Induction.lagda.md -src/plfa/part1/Relations.lagda.md -src/plfa/part1/Equality.lagda.md -src/plfa/part1/Isomorphism.lagda.md -src/plfa/part1/Connectives.lagda.md -src/plfa/part1/Negation.lagda.md -src/plfa/part1/Quantifiers.lagda.md -src/plfa/part1/Decidable.lagda.md -src/plfa/part1/Lists.lagda.md -``` - -# Part 2: Operational Semantics - -``` {.include shift-heading-level-by=1} -src/plfa/part2/Lambda.lagda.md -src/plfa/part2/Properties.lagda.md -src/plfa/part2/DeBruijn.lagda.md -src/plfa/part2/More.lagda.md -src/plfa/part2/Bisimulation.lagda.md -src/plfa/part2/Inference.lagda.md -src/plfa/part2/Untyped.lagda.md -src/plfa/part2/Confluence.lagda.md -src/plfa/part2/BigStep.lagda.md -``` - -# Part 3: Denotational Semantics - -``` {.include shift-heading-level-by=1} -src/plfa/part3/Denotational.lagda.md -src/plfa/part3/Compositional.lagda.md -src/plfa/part3/Soundness.lagda.md -src/plfa/part3/Adequacy.lagda.md -src/plfa/part3/ContextualEquivalence.lagda.md -``` - -# Appendix - -``` {.include shift-heading-level-by=1} -src/plfa/part2/Substitution.lagda.md -``` - - -# Backmatter - -``` {.include shift-heading-level-by=1} -out/epub/acknowledgements.md -src/plfa/Fonts.lagda.md -``` - - diff --git a/epub/rewrite-links.lua b/epub/rewrite-links.lua index ebd3b708..90e5008b 100644 --- a/epub/rewrite-links.lua +++ b/epub/rewrite-links.lua @@ -1,43 +1,19 @@ -local currentChapter = nil - --- Reassigns identifiers for all all Headers level 2 and higher. Level 2 Headers --- correspond to chapters, and are identified by the first word in their content --- field. Headers of level more than 2 are identified by "#-", --- where "" is the identifier of the chapter this header is nested in, --- and "" is this Header's existing identifier. -function Header (el) - if el.level == 2 then - local title = pandoc.utils.stringify(el.content[1]) - currentChapter = title:match("%w+") - el.identifier = currentChapter - elseif el.level > 2 then - el.identifier = currentChapter .. '-' .. el.identifier - end - return el -end - - - -- Performs the following transformations on Link targets: -- -- Case 1: --- [text]({{ site.baseurl }}/chapter/#more-stuff) -> [text](#chapter-more-stuff) +-- [text](/chapter/#more-stuff) -> [text](#chapter-more-stuff) -- -- Case 2: --- [text]({{ site.baseurl }}/chapter/) -> [text](#chapter) +-- [text](/chapter/) -> [text](#chapter) -- -- All other Links are ignored. function Link (el) - local n - -- When parsing a markdown link such as "[stuff]({{ site.baseurl }}/Naturals", - -- pandoc encodes the link's URL with percent-encoding, resulting in the - -- link "[stuff](%7B%7B%20site.baseurl%20%7D%7D/Naturals)". - local baseurl = "%%7B%%7B%%20site%.baseurl%%20%%7D%%7D" - el.target, n = el.target:gsub("^" .. baseurl .. "/(%w+)/#([%w-]+)$", -- case 1 - "#%1-%2") - if n == 0 then - el.target = el.target:gsub("^" .. baseurl .. "/(%w+)/$", -- case 2 - "#%1") - end - return el + local n + -- Case 1: + el.target, n = el.target:gsub("^/(%w+)/#([%w-]+)$", "#%1-%2") + -- Case 2: + if n == 0 then + el.target = el.target:gsub("^/(%w+)/$", "#%1") + end + return el end diff --git a/fix-whitespace.yaml b/fix-whitespace.yaml index e4c69e4b..577143de 100644 --- a/fix-whitespace.yaml +++ b/fix-whitespace.yaml @@ -25,36 +25,32 @@ included-dirs: - "src" - "epub" - - "_includes" - - "_layouts" - - "_posts" - - "_sass" - - "_assets" + - "posts" - "courses" - - "papers" + - "templates" + - "css" + - "public" excluded-dirs: - ".stack-work" - ".git" - - "_build" - "_site" + - "_cache" - "extra" - - "tmp" + - "standard-library" -# Every matched filename is included unless it is matched by excluded-files. included-files: + - "*.hs" + - "*.cabal" - "*.md" - "*.sh" - "*.html" - "*.yml" - "*.yaml" - "*.agda-lib" - - "Gemfile" - - "Guardfile" - "LICENSE" excluded-files: - - "*.sed" - ".DS_Store" - - "Gemfile.lock" - - "Makefile" + - "*.sed" + - "*.lock" diff --git a/highlight.sh b/highlight.sh deleted file mode 100755 index 29aa5b1f..00000000 --- a/highlight.sh +++ /dev/null @@ -1,123 +0,0 @@ -#!/bin/bash - -AGDA_STDLIB_SED=".agda-stdlib.sed" - -function sedi { - sed --version >/dev/null 2>&1 && sed -i "$@" || sed -i "" "$@" -} - -SRC="$1" -shift - -function out_path { - OUT="$1" - OUT=`echo "$OUT" | sed -e "s|src/|out/|; s|courses/|out/|; s|\.lagda\.md|\.md|;"` - echo "$OUT" -} - -OUT="$(out_path $SRC)" -OUT_DIR="$(dirname $OUT)" - -function html_path { - SRC="$1" - HTML_DIR="$2" - - # Extract the module name from the Agda file - # - # NOTE: This fails when there is no module statement, - # or when there is more than one space after 'module'. - # - MOD_NAME=`grep -o -m 1 "module\\s*\\(\\S\\S*\\)\\s.*where$" "$SRC" | cut -d ' ' -f 2` - - if [ -z "$MOD_NAME" ] - then - echo "Error: No module header detected in '$SRC'" 1>&2 - exit 1 - fi - - # Extract the extension from the Agda file - SRC_EXT="$(basename $SRC)" - SRC_EXT="${SRC_EXT##*.}" - - HTML="$HTML_DIR/$MOD_NAME.$SRC_EXT" - echo "$HTML" -} - -HTML_DIR="$(mktemp -d)" -HTML="$(html_path $SRC $HTML_DIR)" - -# Highlight Syntax using Agda -set -o pipefail \ - && agda --html --html-highlight=code --html-dir="$HTML_DIR" "$SRC" "$@" \ - | sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$/d' - -# Check if the highlighted file was successfully generated -if [[ ! -f "$HTML" ]]; then - echo "Error: File not generated: '$FILE'" 1>&2 - exit 1 -fi - -# Add source file to the Jekyll metadata -#sedi "1 s|---|---\nsrc: $SRC|" "$HTML" -ed "$HTML" </dev/null 2>&1 -2i -src : "$SRC" -. -w -q -EOF - -# Add raw tags around Agda code blocks -sedi "s|
|{% raw %}
|" "$HTML"
-sedi "s|
|
{% endraw %}|" "$HTML" - -# Fix links to the Agda standard library -STDLIB_AGDALIB=`grep -m 1 "standard-library" $HOME/.agda/libraries` -STDLIB_AGDALIB="${STDLIB_AGDALIB/#\~/$HOME}" # see https://stackoverflow.com/q/3963716/312692 -STDLIB_AGDALIB="$(eval "echo -e \"$STDLIB_AGDALIB\"")" - -STDLIB_INCLUDE=`grep -m 1 "include:" "$STDLIB_AGDALIB"` -STDLIB_INCLUDE="${STDLIB_INCLUDE#include: }" - -STDLIB_PATH="$(dirname $STDLIB_AGDALIB)" -STDLIB_PATH="$STDLIB_PATH/$STDLIB_INCLUDE" - -if [ -z "$AGDA_STDLIB_VERSION" ]; then - AGDA_STDLIB_URL="https://agda.github.io/agda-stdlib/" -else - AGDA_STDLIB_URL="https://agda.github.io/agda-stdlib/v$AGDA_STDLIB_VERSION/" -fi - -# Create a sed script which matches and replaces all Agda standard library links -if [ ! -f "$AGDA_STDLIB_SED" ]; then - echo "s|\\(Agda\\.[A-Za-z\\.]+\\)|$AGDA_STDLIB_URL\\1|;" > "$AGDA_STDLIB_SED" - find "$STDLIB_PATH" -name "*.agda" -print0 | while read -d $'\0' AGDA_MODULE_PATH; do - AGDA_MODULE=$(eval "echo \"$AGDA_MODULE_PATH\" | sed -e \"s|$STDLIB_PATH/||g; s|/|\\\.|g; s|\.agda|\\\.html|g\"") - echo "s|$AGDA_MODULE|$AGDA_STDLIB_URL$AGDA_MODULE|g;" >> "$AGDA_STDLIB_SED" - done -fi - -sedi -f "$AGDA_STDLIB_SED" "$HTML" - -# Create a sed script which matches and repairs all local links -for INCLUDE_PATH in "$@"; do - if [[ "$INCLUDE_PATH" = --include-path=* ]]; then - INCLUDE_PATH="${INCLUDE_PATH:15}" - INCLUDE_PATH="${INCLUDE_PATH%/}" - LOCAL_LINKS_SED=`echo ".links-${INCLUDE_PATH}.sed" | sed -e "s|/|-|g;"` - - if [ ! -f "$LOCAL_LINKS_SED" ]; then - find "$INCLUDE_PATH" -name "*.lagda.md" -print0 | while read -d $'\0' AGDA_MODULE_SRC; do - AGDA_MODULE_OUT="$(out_path "$AGDA_MODULE_SRC")" - AGDA_MODULE_HTML="$(basename "$(html_path "$AGDA_MODULE_SRC" "$HTML_DIR")" .md).html" - echo "s|$AGDA_MODULE_HTML|{% endraw %}{{ site.baseurl }}{% link $AGDA_MODULE_OUT %}{% raw %}|g;" >> "$LOCAL_LINKS_SED" - done - fi - - sedi -f "$LOCAL_LINKS_SED" "$HTML" - fi -done - -# Copy over the temporary file to the output path -mkdir -p "$OUT_DIR" -cp "$HTML" "$OUT" diff --git a/hs/Hakyll/Web/Agda.hs b/hs/Hakyll/Web/Agda.hs new file mode 100644 index 00000000..f8d175b2 --- /dev/null +++ b/hs/Hakyll/Web/Agda.hs @@ -0,0 +1,196 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} + +module Hakyll.Web.Agda + ( agdaCompilerWith + , agdaVerbosityQuiet + , CommandLineOptions(..) + , PragmaOptions(..) + , defaultAgdaOptions + , defaultAgdaPragmaOptions + , mkFixStdlibLink + , mkFixLocalLink + , agdaModule + , agdaModuleFromPath + ) where + +import qualified Agda.Main as Agda +import Agda.Interaction.Options +import qualified Agda.Interaction.Highlighting.HTML as Agda (generateHTML) +import qualified Agda.Utils.Trie as Trie (singleton) +import Control.Exception (catchJust) +import Control.Monad (forM, void) +import qualified Data.ByteString as B +import Data.Frontmatter (parseYamlFrontmatterEither) +import qualified Data.List.Extra as L +import Data.Maybe (fromMaybe) +import qualified Data.Map as M +import qualified Data.Text as T +import qualified Data.Text.IO as T +import qualified Data.Text.ICU as ICU +import qualified Data.Text.ICU.Replace as ICU +import Data.Yaml (FromJSON(..), ToJSON(..), (.:), (.=)) +import qualified Data.Yaml as Y +import Hakyll +import Text.Printf (printf) +import Text.Regex.TDFA ((=~)) +import System.Directory (createDirectoryIfMissing) +import System.Exit (ExitCode(..), exitFailure) +import System.FilePath.Find ((~~?), (==?), always, extension, fileName, find) +import System.FilePath ((), (<.>), dropExtension, dropExtensions, makeRelative, pathSeparator) + +-- |Default Agda command-line options. Rename of `defaultOptions`. +defaultAgdaOptions :: CommandLineOptions +defaultAgdaOptions = defaultOptions + +-- |Default Agda pragma options. Rename of `defaultPragmaOptions`. +defaultAgdaPragmaOptions :: PragmaOptions +defaultAgdaPragmaOptions = defaultPragmaOptions + +-- |Compile literate Agda to HTML +agdaCompilerWith :: CommandLineOptions -> Compiler (Item String) +agdaCompilerWith agdaOptions = do + item <- getResourceBody + let agdaPath = toFilePath (itemIdentifier item) + let moduleName = agdaModule (itemBody item) + TmpFile tmpPath <- newTmpFile ".lock" + let tmpDir = init (dropExtension tmpPath) + let mdPath = tmpDir moduleName <.> "md" + + md <- unsafeCompiler $ do + createDirectoryIfMissing True tmpDir + + -- Add input file and HTML options + let opts = agdaOptions + { optInputFile = Just agdaPath + , optHTMLDir = tmpDir + , optGenerateHTML = True + , optHTMLHighlight = HighlightCode + } + + -- Run Agda + let tcm = void $ + Agda.runAgdaWithOptions [] Agda.generateHTML (Agda.defaultInteraction opts) "agda" opts + + catchJust + (\case {e@ExitSuccess -> Just e; _ -> Nothing}) + (Agda.runTCMPrettyErrors tcm) + (\_ -> return ()) + + -- Read output Markdown file + md <- readFile mdPath + removeDirectory tmpDir + return md + + return $ itemSetBody md item + +-- |Get Agda module name from code +agdaModule :: String -> String +agdaModule code = case regexResult of + (_, _, _, [moduleName]) -> moduleName + _ -> "Main" + where + moduleRegex = "module ([^ ]*) where" :: String + regexResult = code =~ moduleRegex :: (String, String, String, [String]) + +-- |Get Agda module from a path and a root directory +agdaModuleFromPath :: FilePath -> FilePath -> String +agdaModuleFromPath rootDir = map slashToDot . makeRelative rootDir . dropExtensions + where + slashToDot c = if c == '/' then '.' else c + + +-- |Suppress non-error output +agdaVerbosityQuiet :: Verbosity +agdaVerbosityQuiet = Trie.singleton [] 0 + + +-------------------------------------------------------------------------------- +-- Fix references to Agda standard library +-------------------------------------------------------------------------------- + +-- |Default URL for the Agda standard library. +defaultStdlibUrl :: String +defaultStdlibUrl = "https://agda.github.io/agda-stdlib" + +readStdlibVersion :: FilePath -> IO String +readStdlibVersion stdlibPath = do + let changelogPath = stdlibPath "CHANGELOG.md" + changelog <- T.readFile changelogPath + let versionLine = head (T.lines changelog) + case T.stripPrefix "Version " versionLine of + Just versionStr -> return . T.unpack $ "v" <> T.strip versionStr + Nothing -> error $ printf "Could not read version from '%s'" changelogPath + +-- |Fix references to the Agda standard library. +mkFixStdlibLink :: FilePath -> IO (String -> String) +mkFixStdlibLink stdlibPath = do + stdlibVersion <- readStdlibVersion stdlibPath + let stdlibUrl = defaultStdlibUrl stdlibVersion + re <- stdlibRegex stdlibPath + let replacement = ICU.rstring stdlibUrl <> "/$1.html$2" + return $ T.unpack . ICU.replaceAll re replacement . T.pack + +-- |An ICU regular expression which matches links to the Agda standard library. +stdlibRegex :: FilePath -> IO ICU.Regex +stdlibRegex stdlibPath = do + modNames <- map T.pack <$> stdlibModules stdlibPath + let builtin = "Agda\\.[A-Za-z\\.]+" + let modPatns = T.replace "." "\\." <$> modNames + let modPatn = T.concat . L.intersperse "|" $ builtin : modPatns + let hrefPatn = "(" `T.append` modPatn `T.append` ")\\.html(#[^\"^']+)?" + return (ICU.regex [] hrefPatn) + +-- |Gather all standard library modules given a path. +stdlibModules :: FilePath -> IO [String] +stdlibModules stdlibPath = do + let stdlibPathSrc = stdlibPath "src" + agdaFiles <- find always (extension ==? ".agda") stdlibPathSrc + let sepToDot c = if c == pathSeparator then '.' else c + let fileToMod = map sepToDot . dropExtension . makeRelative stdlibPathSrc + return . map fileToMod $ agdaFiles + + + +-------------------------------------------------------------------------------- +-- Fix references to local Agda modules +-------------------------------------------------------------------------------- + +newtype Frontmatter = Frontmatter + { frontmatterPermalink :: FilePath + } + +instance FromJSON Frontmatter where + parseJSON = Y.withObject "Frontmatter" $ \v -> Frontmatter + <$> v .: "permalink" + +instance ToJSON Frontmatter where + toJSON Frontmatter{..} = + Y.object [ "permalink" .= frontmatterPermalink + ] + +-- |Create a function to fix URL references output by Agda HTML highlighter. +mkFixLocalLink :: FilePath -> IO (String -> String) +mkFixLocalLink rootDir = do + -- Get all Agda files in `rootDir`. + agdaFiles <- find always (fileName ~~? "*.lagda.md") rootDir + + -- Get all permalinks and Agda module names from these files. + localLinkList <- forM agdaFiles $ \agdaFile -> do + frontmatterOrError <- parseYamlFrontmatterEither <$> B.readFile agdaFile + case frontmatterOrError of + Left errmsg -> do + printf "Parse error in '%s': %s\n" agdaFile errmsg + exitFailure + Right Frontmatter{..} -> + return (agdaModuleFromPath rootDir agdaFile, frontmatterPermalink) + + -- Construct a Map from the local link list. + let localLinkMap = M.fromList localLinkList + + -- Construct a function which looks up the URL in the map. + return $ \url -> fromMaybe url $ do + (oldPath, anchor) <- L.stripInfix ".html" url + newPath <- M.lookup oldPath localLinkMap + return $ newPath <> anchor diff --git a/hs/Hakyll/Web/Routes/Permalink.hs b/hs/Hakyll/Web/Routes/Permalink.hs new file mode 100644 index 00000000..68a89807 --- /dev/null +++ b/hs/Hakyll/Web/Routes/Permalink.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Hakyll.Web.Routes.Permalink + ( convertPermalink + , permalinkRoute + , permalinkRouteWithDefault + ) where + +import Data.List (stripPrefix) +import Data.Maybe (fromMaybe) +import Hakyll +import System.FilePath (()) + +-- By a quirk of history, permalinks for PLFA are written as, e.g., "/DeBruijn/". +-- We convert these to links by stripping the "/" prefix, and adding "index.html". +convertPermalink :: FilePath -> FilePath +convertPermalink link = fromMaybe link (stripPrefix "/" link) "index.html" + +permalinkRoute :: Routes +permalinkRoute = permalinkRouteWithDefault (error "Missing field 'permalink'.") + +permalinkRouteWithDefault :: Routes -> Routes +permalinkRouteWithDefault def = metadataRoute $ \metadata -> + maybe def (constRoute . convertPermalink) (lookupString "permalink" metadata) + diff --git a/hs/Hakyll/Web/Sass.hs b/hs/Hakyll/Web/Sass.hs new file mode 100644 index 00000000..1f6e4df9 --- /dev/null +++ b/hs/Hakyll/Web/Sass.hs @@ -0,0 +1,24 @@ +-------------------------------------------------------------------------------- +-- Compile SASS and SCSS +-------------------------------------------------------------------------------- + +module Hakyll.Web.Sass + ( sassCompilerWith + , SassOptions(..) + , defaultSassOptions + ) where + +import Hakyll +import Text.Sass (SassOptions(..), defaultSassOptions) +import qualified Text.Sass as Sass + +sassCompilerWith :: SassOptions -> Compiler (Item String) +sassCompilerWith opts = getResourceBody >>= withItemBody renderSass + where + renderSass :: String -> Compiler String + renderSass sass = unsafeCompiler $ do + cssOrErr <- Sass.compileString sass opts + case cssOrErr of + Left err -> Sass.errorMessage err + Right css -> return (compressCss css) + diff --git a/hs/Hakyll/Web/Template/Context/Metadata.hs b/hs/Hakyll/Web/Template/Context/Metadata.hs new file mode 100644 index 00000000..ad61554b --- /dev/null +++ b/hs/Hakyll/Web/Template/Context/Metadata.hs @@ -0,0 +1,53 @@ +module Hakyll.Web.Template.Context.Metadata where + +import Control.Monad ((<=<)) +import Data.Aeson (Object, Value(..)) +import qualified Data.HashMap.Strict as H +import qualified Data.Text as T +import qualified Data.Vector as V +import Hakyll +import Text.Printf (printf) + +-- |Create a Context based on a JSON Object. +objectContext :: Context String -> Context Object +objectContext ctx = Context $ \k _ i -> + let o = itemBody i in + case H.lookup (T.pack k) o of + Just v -> decodeValue ctx v + Nothing -> fail $ printf "Key '%s' undefined in context '%s'" k (show o) + +isObject :: Value -> Bool +isObject (Object _) = True +isObject _ = False + +isString :: Value -> Bool +isString (String _) = True +isString _ = False + +toObject :: MonadFail m => Value -> m Object +toObject (Object o) = return o +toObject v = fail $ printf "Not an object '%s'" (show v) + +toString :: MonadFail m => Value -> m String +toString (String s) = return (T.unpack s) +toString v = fail $ printf "Not a string '%s'" (show v) + +-- |Decode a JSON Value to a context field. +decodeValue :: Context String -> Value -> Compiler ContextField +decodeValue ctx (Array a) + | V.all isObject a = do + objs <- mapM (makeItem <=< toObject) (V.toList a) + return $ ListField (objectContext ctx) objs + | V.all isString a = do + items <- mapM (load . fromFilePath <=< toString) (V.toList a) + return $ ListField ctx items +decodeValue _ (String s) = return . StringField $ T.unpack s +decodeValue _ (Number n) = return . StringField $ show n +decodeValue _ (Bool b) = return . StringField $ show b +decodeValue _ v = fail $ printf "Unsupported value '%s'" (show v) + +-- |Create a Context based on the Metadata. +metadataContext :: Context String -> Context String +metadataContext ctx = Context $ \k a i -> + unContext (objectContext ctx) k a <=< makeItem <=< getMetadata $ itemIdentifier i + diff --git a/hs/Main.hs b/hs/Main.hs new file mode 100644 index 00000000..ba96f941 --- /dev/null +++ b/hs/Main.hs @@ -0,0 +1,375 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TupleSections #-} + +import Control.Monad ((<=<), forM_) +import qualified Data.ByteString.Lazy as BL +import Data.List as L +import Data.List.Extra as L +import Data.Maybe (fromMaybe) +import Data.Ord (comparing) +import qualified Data.Text as T +import Hakyll +import Hakyll.Web.Agda +import Hakyll.Web.Template.Context.Metadata +import Hakyll.Web.Sass +import Hakyll.Web.Routes.Permalink +import System.FilePath ((), takeDirectory) +import Text.Pandoc as Pandoc +import Text.Pandoc.Filter +import Text.Printf (printf) +import Text.Read (readMaybe) + +-------------------------------------------------------------------------------- +-- Configuration +-------------------------------------------------------------------------------- + +tocContext :: Context String -> Context String +tocContext ctx = Context $ \k a _ -> do + m <- makeItem <=< getMetadata $ "src/plfa/toc.metadata" + unContext (objectContext ctx) k a m + +siteContext :: Context String +siteContext = mconcat + [ constField "pagetitle" "Programming Language Foundations in Agda" + , constField "pageurl" "https://plfa.github.io" + , constField "description" "An introduction to programming language theory using the proof assistant Agda." + , constField "language" "en-US" + , constField "rights" "Creative Commons Attribution 4.0 International License" + , constField "rights_url" "https://creativecommons.org/licenses/by/4.0/" + , constField "repository" "plfa/plfa.github.io" + , constField "branch" "dev" + , modificationTimeField "modified" "%0Y-%m-%dT%H:%M:%SZ" + , field "source" (return . toFilePath . itemIdentifier) + , listField "authors" defaultContext $ mapM load + [ "authors/wadler.metadata" + , "authors/wenkokke.metadata" + , "authors/jsiek.metadata" + ] + , constField "google_analytics" "UA-125055580-1" + , defaultContext + ] + +siteSectionContext :: Context String +siteSectionContext = mconcat + [ titlerunningField + , subtitleField + , siteContext + ] + +acknowledgementsContext :: Context String +acknowledgementsContext = mconcat + [ listField "contributors" defaultContext $ + byNumericFieldDesc "count" =<< loadAll "contributors/*.metadata" + , siteContext + ] + +postContext :: Context String +postContext = mconcat + [ dateField "date" "%B %e, %Y" + , siteContext + ] + +postListContext :: Context String +postListContext = mconcat + [ listField "posts" postItemContext $ + recentFirst =<< loadAll "posts/*" + , siteContext + ] + where + postItemContext :: Context String + postItemContext = mconcat + [ teaserField "teaser" "content" + , contentField "content" "content" + , postContext + ] + +agdaStdlibPath :: FilePath +agdaStdlibPath = "standard-library" + +agdaOptions :: CommandLineOptions +agdaOptions = defaultAgdaOptions + { optUseLibs = False + , optIncludePaths = [agdaStdlibPath "src", "src"] + , optPragmaOptions = defaultAgdaPragmaOptions + { optVerbose = agdaVerbosityQuiet + } + } + +sassOptions :: SassOptions +sassOptions = defaultSassOptions + { sassIncludePaths = Just ["css"] + } + +-------------------------------------------------------------------------------- +-- Build site +-------------------------------------------------------------------------------- + +main :: IO () +main = do + + -- Build function to fix standard library URLs + fixStdlibLink <- mkFixStdlibLink agdaStdlibPath + + -- Build function to fix local URLs + fixLocalLink <- mkFixLocalLink "src" + + -- Build compiler for Markdown pages + let pageCompiler :: Compiler (Item String) + pageCompiler = pandocCompiler + >>= saveSnapshot "content" + >>= loadAndApplyTemplate "templates/page.html" siteContext + >>= loadAndApplyTemplate "templates/default.html" siteContext + >>= relativizeUrls + + -- Build compiler for literate Agda pages + let pageWithAgdaCompiler :: CommandLineOptions -> Compiler (Item String) + pageWithAgdaCompiler opts = agdaCompilerWith opts + >>= withItemBody (return . withUrls fixStdlibLink) + >>= withItemBody (return . withUrls fixLocalLink) + >>= renderPandoc + >>= saveSnapshot "content" + >>= loadAndApplyTemplate "templates/page.html" siteContext + >>= loadAndApplyTemplate "templates/default.html" siteContext + >>= relativizeUrls + + -- Run Hakyll + -- + -- NOTE: The order of the various match expressions is important: + -- Special-case compilation instructions for files such as + -- "src/plfa/epub.md" and "src/plfa/index.md" would be overwritten + -- by the general purpose compilers for "src/**.md", which would + -- cause them to render incorrectly. It is possible to explicitly + -- exclude such files using `complement` patterns, but this vastly + -- complicates the match patterns. + -- + hakyll $ do + + -- Compile EPUB + match "src/plfa/epub.md" $ do + route $ constRoute "plfa.epub" + compile $ do + epubTemplate <- load "templates/epub.html" + >>= compilePandocTemplate + epubMetadata <- load "src/plfa/meta.xml" + let ropt = epubReaderOptions + let wopt = epubWriterOptions + { writerTemplate = Just . itemBody $ epubTemplate + , writerEpubMetadata = Just . T.pack . itemBody $ epubMetadata + } + getResourceBody + >>= applyAsTemplate (tocContext epubSectionContext) + >>= readPandocWith ropt + >>= applyPandocFilters ropt [] "epub3" + >>= writeEPUB3With wopt + + match "templates/epub.html" $ + compile $ getResourceBody + >>= applyAsTemplate siteContext + + match "src/plfa/meta.xml" $ + compile $ getResourceBody + >>= applyAsTemplate siteContext + + -- Compile Table of Contents + match "src/plfa/index.md" $ do + route permalinkRoute + compile $ getResourceBody + >>= applyAsTemplate (tocContext siteSectionContext) + >>= renderPandoc + >>= loadAndApplyTemplate "templates/page.html" siteContext + >>= loadAndApplyTemplate "templates/default.html" siteContext + >>= relativizeUrls + + match "src/**.metadata" $ + compile getResourceBody + + -- Compile Acknowledgements + match "src/plfa/backmatter/acknowledgements.md" $ do + route permalinkRoute + compile $ getResourceBody + >>= applyAsTemplate acknowledgementsContext + >>= renderPandoc + >>= saveSnapshot "content" + >>= loadAndApplyTemplate "templates/page.html" siteContext + >>= loadAndApplyTemplate "templates/default.html" siteContext + >>= relativizeUrls + + match "authors/*.metadata" $ + compile getResourceBody + + match "contributors/*.metadata" $ + compile getResourceBody + + -- Compile Announcements + match "src/pages/announcements.html" $ do + route permalinkRoute + compile $ getResourceBody + >>= applyAsTemplate postListContext + >>= loadAndApplyTemplate "templates/page.html" siteContext + >>= loadAndApplyTemplate "templates/default.html" siteContext + >>= relativizeUrls + + match "posts/*" $ do + route $ setExtension "html" + compile $ pandocCompiler + >>= saveSnapshot "content" + >>= loadAndApplyTemplate "templates/post.html" postContext + >>= loadAndApplyTemplate "templates/default.html" siteContext + >>= relativizeUrls + + -- Compile sections using literate Agda + match "src/**.lagda.md" $ do + route permalinkRoute + compile $ pageWithAgdaCompiler agdaOptions + + -- Compile other sections and pages + match ("README.md" .||. "src/**.md") $ do + route permalinkRoute + compile pageCompiler + + -- Compile course pages + match "courses/**.lagda.md" $ do + route permalinkRoute + compile $ do + courseDir <- takeDirectory . toFilePath <$> getUnderlying + let courseOptions = agdaOptions + { optIncludePaths = courseDir : optIncludePaths agdaOptions + } + pageWithAgdaCompiler courseOptions + + match "courses/**.md" $ do + route permalinkRoute + compile pageCompiler + + match "courses/**.pdf" $ do + route idRoute + compile copyFileCompiler + + -- Compile 404 page + match "404.html" $ do + route idRoute + compile $ pandocCompiler + >>= loadAndApplyTemplate "templates/default.html" siteContext + + -- Compile templates + match "templates/*" $ compile templateBodyCompiler + + -- Copy resources + match "public/**" $ do + route idRoute + compile copyFileCompiler + + -- Compile CSS + match "css/*.css" $ compile compressCssCompiler + + scss <- makePatternDependency "css/minima/**.scss" + rulesExtraDependencies [scss] $ + match "css/minima.scss" $ + compile $ sassCompilerWith sassOptions + + create ["public/css/style.css"] $ do + route idRoute + compile $ do + csses <- loadAll ("css/*.css" .||. "css/*.scss" .&&. complement "css/epub.css") + makeItem $ unlines $ map itemBody csses + + -- Copy versions + let versions = ["19.08", "20.07"] + forM_ versions $ \v -> do + + -- Relativise URLs in HTML files + match (fromGlob $ "versions" v "**.html") $ do + route $ gsubRoute ".versions/" (const "") + compile $ getResourceBody + >>= relativizeUrls + + -- Copy other files + match (fromGlob $ "versions" v "**") $ do + route $ gsubRoute ".versions/" (const "") + compile copyFileCompiler + +-------------------------------------------------------------------------------- +-- EPUB generation +-------------------------------------------------------------------------------- + +epubSectionContext :: Context String +epubSectionContext = mconcat + [ contentField "content" "content" + , titlerunningField + , subtitleField + ] + +epubReaderOptions :: ReaderOptions +epubReaderOptions = defaultHakyllReaderOptions + { readerStandalone = True + , readerStripComments = True + } + +epubWriterOptions :: WriterOptions +epubWriterOptions = defaultHakyllWriterOptions + { writerTableOfContents = True + , writerTOCDepth = 2 + , writerEpubFonts = [ "public/webfonts/DejaVuSansMono.woff" + , "public/webfonts/FreeMono.woff" + , "public/webfonts/mononoki.woff" + ] + , writerEpubChapterLevel = 2 + } + +applyPandocFilters :: ReaderOptions -> [Filter] -> String -> Item Pandoc -> Compiler (Item Pandoc) +applyPandocFilters ropt filters fmt = withItemBody $ + unsafeCompiler . runIOorExplode . applyFilters ropt filters [fmt] + +compilePandocTemplate :: Item String -> Compiler (Item (Pandoc.Template T.Text)) +compilePandocTemplate i = do + let templatePath = toFilePath $ itemIdentifier i + let templateBody = T.pack $ itemBody i + templateOrError <- unsafeCompiler $ Pandoc.compileTemplate templatePath templateBody + template <- either fail return templateOrError + makeItem template + +writeEPUB3With :: WriterOptions -> Item Pandoc -> Compiler (Item BL.ByteString) +writeEPUB3With wopt (Item itemi doc) = do + return $ case runPure $ writeEPUB3 wopt doc of + Left err -> error $ "Hakyll.Web.Pandoc.writeEPUB3With: " ++ show err + Right doc' -> Item itemi doc' + + +-------------------------------------------------------------------------------- +-- Supply snapshot as a field to the template +-------------------------------------------------------------------------------- + +subtitleField :: Context String +subtitleField = Context go + where + go "subtitle" _ i = do + title <- maybe (fail "No title") return =<< getMetadataField (itemIdentifier i) "title" + case L.stripInfix ":" title of + Nothing -> fail "No titlerunning/subtitle distinction" + Just (_, subtitle) -> return . StringField $ L.trim subtitle + go k _ i = fail $ printf "Missing field %s in context for item %s" k (show (itemIdentifier i)) + +titlerunningField :: Context String +titlerunningField = Context go + where + go "titlerunning" _ i = do + title <- maybe (fail "No title") return =<< getMetadataField (itemIdentifier i) "title" + case L.stripInfix ":" title of + Nothing -> fail "No titlerunning/subtitle distinction" + Just (titlerunning, _) -> return . StringField $ titlerunning + go k _ i = fail $ printf "Missing field %s in context for item %s" k (show (itemIdentifier i)) + +contentField :: String -> Snapshot -> Context String +contentField key snapshot = field key $ \item -> + itemBody <$> loadSnapshot (itemIdentifier item) snapshot + +byNumericFieldAsc :: MonadMetadata m => String -> [Item a] -> m [Item a] +byNumericFieldAsc key = sortOnM $ \i -> do + maybeInt <- getMetadataField (itemIdentifier i) key + return $ fromMaybe (0 :: Int) (readMaybe =<< maybeInt) + +byNumericFieldDesc :: MonadMetadata m => String -> [Item a] -> m [Item a] +byNumericFieldDesc key is = reverse <$> byNumericFieldAsc key is + +sortOnM :: (Monad m, Ord k) => (a -> m k) -> [a] -> m [a] +sortOnM f xs = map fst . L.sortBy (comparing snd) <$> mapM (\ x -> (x,) <$> f x) xs diff --git a/hs/UpdateContributors.hs b/hs/UpdateContributors.hs new file mode 100644 index 00000000..983dc1c9 --- /dev/null +++ b/hs/UpdateContributors.hs @@ -0,0 +1,209 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE OverloadedStrings #-} + +module Main where + +import Control.Monad (forM, forM_) +import qualified Data.ByteString as B +import qualified Data.ByteString.Char8 as BC +import Data.Frontmatter (parseYamlFrontmatterEither) +import Data.Map (Map) +import qualified Data.Map as M +import Data.Maybe (fromMaybe, mapMaybe) +import Data.String (IsString(..)) +import Data.Text (Text) +import qualified Data.Text as T +import qualified Data.Vector as V +import Data.Yaml (FromJSON(..), ToJSON(..), (.:), (.:?), (.=)) +import qualified Data.Yaml as Y +import qualified GitHub as GH +import System.Directory (createDirectoryIfMissing) +import System.Exit (exitFailure) +import System.FilePath ((), (<.>)) +import System.FilePath.Glob (namesMatching) +import System.Environment (lookupEnv) +import Text.Printf (printf) + + +-- * Configuration + +authorDir, contributorDir :: FilePath +authorDir = "authors" +contributorDir = "contributors" + +githubOwner, githubRepo :: Text +githubOwner = "plfa" +githubRepo = "plfa.github.io" + +githubErrors :: [Text] +githubErrors = ["invalid-email-address"] + + +-- * Main + +main :: IO () +main = do + -- Get the GitHub authentication token from `GITHUB_TOKEN` + auth <- getAuth + + -- Read the current set of authors from `authorDir` + authors <- readAuthors authorDir + + -- Read the current set of contributors from `contributorDir` + localContributors <- readContributors contributorDir + remoteContributorAndAuthors <- + getContributors auth (GH.mkOwnerName githubOwner) (GH.mkRepoName githubRepo) + + -- Filter the contributor list by the authors + let authorGithubs :: [Text] + authorGithubs = map authorGithub authors + + let isAuthorOrError :: Contributor -> Bool + isAuthorOrError Contributor{..} = + contributorGithub `elem` authorGithubs || contributorGithub `elem` githubErrors + + let remoteContributors :: [Contributor] + remoteContributors = filter (not . isAuthorOrError) remoteContributorAndAuthors + + -- Turn contributor lists into maps and merge them + let localContributorMap :: Map Text Contributor + localContributorMap = M.fromList [(contributorGithub c, c) | c <- localContributors] + + let remoteContributorMap :: Map Text Contributor + remoteContributorMap = M.fromList [(contributorGithub c, c) | c <- remoteContributors] + + let contributorMap :: Map Text Contributor + contributorMap = M.unionWith (<>) localContributorMap remoteContributorMap + + -- Write contributor files + createDirectoryIfMissing True contributorDir + forM_ (M.toList contributorMap) $ \(github, contributor) -> do + let contributorFile = contributorDir T.unpack github <.> "metadata" + let contributorBS = "---\n" <> Y.encode contributor <> "---\n" + BC.writeFile contributorFile contributorBS + + +-- * Authors + +data Author = Author + { authorName :: Text + , authorEmail :: Text + , authorCorresponding :: Bool + , authorGithub :: Text + , authorTwitter :: Maybe Text + } + deriving (Show) + +readAuthors :: FilePath -> IO [Author] +readAuthors dir = do + authorFiles <- namesMatching (dir "*.metadata") + forM authorFiles $ \authorFile -> do + authorOrError <- parseYamlFrontmatterEither <$> B.readFile authorFile + case authorOrError of + Left errmsg -> do + printf "Parse error in '%s': %s\n" authorFile errmsg + exitFailure + Right author -> + return author + +instance FromJSON Author where + parseJSON = Y.withObject "Author" $ \v -> Author + <$> v .: "name" + <*> v .: "email" + <*> v .: "corresponding" + <*> v .: "github" + <*> v .:? "twitter" + +instance ToJSON Author where + toJSON Author{..} = + Y.object [ "name" .= authorName + , "email" .= authorEmail + , "corresponding" .= authorCorresponding + , "github" .= authorGithub + , "twitter" .= authorTwitter + ] + + +-- * Contributors + +data Contributor = Contributor + { contributorName :: Text + , contributorGithub :: Text + , contributorCount :: Int + } + +instance Semigroup Contributor where + Contributor _name1 github1 count1 <> Contributor name2 github2 count2 + = if github1 == github2 + then Contributor name2 github2 (count1 `max` count2) + else error $ printf "Cannot merge unrelated contributors '%s' and '%s'" github1 github2 + +instance FromJSON Contributor where + parseJSON = Y.withObject "Contributor" $ \v -> Contributor + <$> v .: "name" + <*> v .: "github" + <*> v .: "count" + +instance ToJSON Contributor where + toJSON Contributor{..} = + Y.object [ "name" .= contributorName + , "github" .= contributorGithub + , "count" .= contributorCount + ] + +readContributors :: FilePath -> IO [Contributor] +readContributors dir = do + contributorFiles <- namesMatching (dir "*.metadata") + forM contributorFiles $ \contributorFile -> do + contributorOrError <- parseYamlFrontmatterEither <$> B.readFile contributorFile + case contributorOrError of + Left errmsg -> do + printf "Parse error in '%s': %s\n" contributorFile errmsg + exitFailure + Right contributor -> + return contributor + + +-- * Github interaction + +-- |Get user information for every user who authored a commit. +getContributors :: GH.Auth -> GH.Name GH.Owner -> GH.Name GH.Repo -> IO [Contributor] +getContributors auth owner repo = do + commits <- getCommits auth owner repo + forM (frequency (mapMaybe GH.commitAuthor commits)) $ \(simpleUser, count) -> do + user <- getUserInfo auth simpleUser + return $ toContributor user count + +-- |Convert a |GH.User| value to a |Contributor| value. +toContributor :: GH.User -> Int -> Contributor +toContributor commitAuthor count = Contributor name github count + where + name = fromMaybe github (GH.userName commitAuthor) + github = GH.untagName (GH.userLogin commitAuthor) + +-- |Get an authentication token from the environment. +getAuth :: IO GH.Auth +getAuth = do + mtoken <- lookupEnv "GITHUB_TOKEN" + case mtoken of + Nothing -> error "Please set GITHUB_TOKEN" + Just token -> return (GH.OAuth . fromString $ token) + +-- |Get user information from a user login. +getUserInfo :: GH.Auth -> GH.SimpleUser -> IO GH.User +getUserInfo auth simpleUser = + fromRight =<< GH.github auth GH.userInfoForR (GH.simpleUserLogin simpleUser) + +-- |Get commit history for a repository. +getCommits :: GH.Auth -> GH.Name GH.Owner -> GH.Name GH.Repo -> IO [GH.Commit] +getCommits auth owner repo = + V.toList <$> (fromRight =<< GH.github auth GH.commitsForR owner repo GH.FetchAll) + + +-- * Utils + +frequency :: (Ord a) => [a] -> [(a, Int)] +frequency xs = M.toList (M.fromListWith (+) [(x, 1) | x <- xs]) + +fromRight :: Show e => Either e a -> IO a +fromRight = either (fail . show) return diff --git a/plfa.cabal b/plfa.cabal new file mode 100644 index 00000000..8029e1d8 --- /dev/null +++ b/plfa.cabal @@ -0,0 +1,58 @@ +cabal-version: 2.2 +name: plfa +version: 20.10 +description: Programming Language Foundations in Agda +homepage: https://plfa.inf.ed.ac.uk +license-file: LICENSE +author: Wen Kokke +copyright: © 2017-2020 Wen Kokke, Jeremy G. Siek, and Philip Wadler +category: Web +build-type: Simple + +common shared-properties + ghc-options: -Wall + default-language: Haskell2010 + build-depends: aeson >=1.4 && <1.5 + , base >=4.6 && <5 + , bytestring >=0.10 && <0.11 + , containers >=0.6 && <0.7 + , directory >=1.2 && <1.4 + , doctemplates >=0.8 && <0.9 + , extra >=1.7 && <1.8 + , filemanip >=0.3 && <0.4 + , filepath >=1.3 && <1.5 + , frontmatter >=0.1 && <0.2 + , hakyll >=4.10 && <4.15 + , pandoc >=2.1 && <2.11 + , pandoc-types >=1.20 && <1.21 + , pandoc-citeproc >=0.17 && <0.18 + , text >=1.2 && <1.3 + , unordered-containers >=0.2 && <0.3 + , vector >=0.12 && <0.13 + , yaml >=0.11 && <0.12 + +library + import: shared-properties + hs-source-dirs: hs + exposed-modules: Hakyll.Web.Agda + , Hakyll.Web.Template.Context.Metadata + , Hakyll.Web.Sass + , Hakyll.Web.Routes.Permalink + build-depends: Agda ==2.6.1.1 + , hsass >=0.8 && <0.9 + , regex-tdfa >=1.3 && <1.4 + , text-icu >=0.7 && <0.8 + , text-regex-replace >=0.1 && <0.2 + +executable site + import: shared-properties + main-is: hs/Main.hs + build-depends: plfa + ghc-options: -threaded + +executable update-contributors + import: shared-properties + main-is: hs/UpdateContributors.hs + build-depends: exceptions >=0.10 && <0.11 + , github >=0.26 && <0.27 + , vector >=0.12 && <0.13 diff --git a/_posts/2019-07-12-migration-to-2.6.0.1.md b/posts/2019-07-12-migration-to-agda-2.6.0.1.md similarity index 92% rename from _posts/2019-07-12-migration-to-2.6.0.1.md rename to posts/2019-07-12-migration-to-agda-2.6.0.1.md index 13d842f1..850eb495 100644 --- a/_posts/2019-07-12-migration-to-2.6.0.1.md +++ b/posts/2019-07-12-migration-to-agda-2.6.0.1.md @@ -1,10 +1,8 @@ --- -layout : post -title : "Migration to Agda 2.6.0.1" -short : false +title: "Migration to Agda 2.6.0.1" --- -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 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. diff --git a/_posts/2020-01-10-plfa-as-a-notebook.md b/posts/2020-01-10-plfa-as-a-notebook.md similarity index 83% rename from _posts/2020-01-10-plfa-as-a-notebook.md rename to posts/2020-01-10-plfa-as-a-notebook.md index fdbfae21..81a92c39 100644 --- a/_posts/2020-01-10-plfa-as-a-notebook.md +++ b/posts/2020-01-10-plfa-as-a-notebook.md @@ -1,12 +1,8 @@ --- -layout : post -title : "PLFA as a Notebook" -short : true +title: "PLFA as a Notebook" --- NextJournal has created [a notebook version of PLFA][NextJournal-PLFA], which lets you edit and run the code samples from the book online! The notebook is based on [PLFA version 19.08][PLFA-19.08], with some minor changes to adapt the contents to NextJournal. [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 similarity index 91% rename from _posts/2020-04-30-praise-for-plfa.md rename to posts/2020-04-30-praise-for-plfa.md index 64475efa..dce31473 100644 --- a/_posts/2020-04-30-praise-for-plfa.md +++ b/posts/2020-04-30-praise-for-plfa.md @@ -1,7 +1,5 @@ --- -layout : post -title : "Praise for PLFA" -short : true +title: "Praise for PLFA" --- [*Types and Semantics for Programming Languages*][TSPL-2019], the course we teach in Edinburgh, was shortlisted as an Outstanding Course by the [Edinburgh University Student Association][EUSA-2020] (Runner Up)! @@ -12,5 +10,3 @@ short : true [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 similarity index 86% rename from _posts/2020-06-02-plfa-as-epub.md rename to posts/2020-06-02-plfa-as-epub.md index 460e65c4..83f434c3 100644 --- a/_posts/2020-06-02-plfa-as-epub.md +++ b/posts/2020-06-02-plfa-as-epub.md @@ -1,7 +1,5 @@ --- -layout : post -title : "PLFA as EPUB" -short : true +title: "PLFA as EPUB" --- It has been just over a year and a half since this feature was first requested in [#112][issue112]… Thanks to hard work by [Michael Reed][mreed20], and a little elbow grease on our part, it is finally here! [An EPUB version of PLFA!][EPUB] @@ -9,5 +7,3 @@ It has been just over a year and a half since this feature was first requested [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 similarity index 85% rename from _posts/2020-06-23-talking-about-plfa.md rename to posts/2020-06-23-talking-about-plfa.md index 3b1e2d7f..93189ccc 100644 --- a/_posts/2020-06-23-talking-about-plfa.md +++ b/posts/2020-06-23-talking-about-plfa.md @@ -1,7 +1,5 @@ --- -layout : post -title : "Talking about PLFA…" -short : true +title: "Talking about PLFA…" --- We published a paper about PLFA at the [Brazilian Symposium on Formal Methods][SBMF] and in the [Science of Computer Programming][SCP] (extended version). In them, we describe our experiences writing the book, and compare it to [Software Foundations][SF]. @@ -9,5 +7,3 @@ We published a paper about PLFA at the [Brazilian Symposium on Formal Methods][S [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 similarity index 96% rename from _posts/2020-07-13-denotational-semantics.md rename to posts/2020-07-13-denotational-semantics.md index c5c99705..594e48fe 100644 --- a/_posts/2020-07-13-denotational-semantics.md +++ b/posts/2020-07-13-denotational-semantics.md @@ -1,7 +1,5 @@ --- -layout : post -title : "Introducing Part 3: Denotational Semantics" -short : false +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! diff --git a/_posts/2020-07-14-versions-and-releases.md b/posts/2020-07-14-versions-and-releases.md similarity index 98% rename from _posts/2020-07-14-versions-and-releases.md rename to posts/2020-07-14-versions-and-releases.md index 79418db7..f4accb44 100644 --- a/_posts/2020-07-14-versions-and-releases.md +++ b/posts/2020-07-14-versions-and-releases.md @@ -1,7 +1,5 @@ --- -layout : post title : "Versions and Releases" -short : false --- We’re adding stable releases to PLFA, which you can find [on GitHub][releases]! diff --git a/_posts/2020-07-20-migration-to-agda-2.6.1.md b/posts/2020-07-20-migration-to-agda-2.6.1.md similarity index 95% rename from _posts/2020-07-20-migration-to-agda-2.6.1.md rename to posts/2020-07-20-migration-to-agda-2.6.1.md index b5e134f2..01d72ede 100644 --- a/_posts/2020-07-20-migration-to-agda-2.6.1.md +++ b/posts/2020-07-20-migration-to-agda-2.6.1.md @@ -1,10 +1,8 @@ --- -layout : post title : "Migration to Agda 2.6.1" -short : false --- -We upgraded to [Agda 2.6.1](https://github.com/agda/agda/releases/tag/v2.6.1) and [version 1.3 of the standard library](https://github.com/agda/agda-stdlib/releases/tag/v1.3). If you want to continue working with the latest version of 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 upgraded to [Agda 2.6.1](https://github.com/agda/agda/releases/tag/v2.6.1) and [version 1.3 of the standard library](https://github.com/agda/agda-stdlib/releases/tag/v1.3). If you want to continue working with the latest version of 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. diff --git a/public/minima-social-icons.svg b/public/minima-social-icons.svg new file mode 100755 index 00000000..ff02f3ef --- /dev/null +++ b/public/minima-social-icons.svg @@ -0,0 +1,50 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/assets/fonts/DejaVuSansMono.woff b/public/webfonts/DejaVuSansMono.woff old mode 100755 new mode 100644 similarity index 100% rename from assets/fonts/DejaVuSansMono.woff rename to public/webfonts/DejaVuSansMono.woff diff --git a/assets/fonts/FreeMono.woff b/public/webfonts/FreeMono.woff similarity index 100% rename from assets/fonts/FreeMono.woff rename to public/webfonts/FreeMono.woff diff --git a/assets/fonts/mononoki.woff b/public/webfonts/mononoki.woff similarity index 100% rename from assets/fonts/mononoki.woff rename to public/webfonts/mononoki.woff diff --git a/assets/fonts/mononoki.woff2 b/public/webfonts/mononoki.woff2 similarity index 100% rename from assets/fonts/mononoki.woff2 rename to public/webfonts/mononoki.woff2 diff --git a/src/pages/announcements.html b/src/pages/announcements.html new file mode 100644 index 00000000..3514c5d6 --- /dev/null +++ b/src/pages/announcements.html @@ -0,0 +1,21 @@ +--- +title : "Announcements" +permalink : /Announcements/ +--- + +$if(posts)$ +
+ $for(posts)$ +
  • +

    $title$

    + + $if(teaser)$ + $teaser$ + (more) + $else$ + $content$ + $endif$ +
  • + $endfor$ + +$endif$ diff --git a/src/plfa/citing.md b/src/pages/citing.md similarity index 100% rename from src/plfa/citing.md rename to src/pages/citing.md diff --git a/RELEASES.md b/src/pages/howto.md similarity index 58% rename from RELEASES.md rename to src/pages/howto.md index 5e89347b..a1c3ecac 100644 --- a/RELEASES.md +++ b/src/pages/howto.md @@ -1,4 +1,22 @@ -# How to create a new release +--- +title : "Checklists for various tasks" +permalink : /HOWTO/ +--- + +# Publishing an announcement + +PLFA announcements are files with names of the form `YYYY-0M-0D-SLUG.md`, where `YYYY` is the long year, `0M` is the zero-padded month, `0D` is the zero-padded day, and `SLUG` is the URL slug for the post, usually an URL-safe version of the title. + +There are several steps to writing an announcement for PLFA: + +- [ ] Create a new file in `posts` with the name `YYYY-0M-0D-SLUG.md`. +- [ ] Add the metadata block, setting at least the `title` field. +- [ ] Write the announcement in the remainder of the file. + +If the announcement is short, it will be displayed inline in on the announcements page. If the announcement is long, insert a `` tag after the first paragraph. Everything before this tag will be displayed on the announcements page, as a “teaser” followed by a link to the full text. + + +# Publishing a release For a project such as PLFA, [Semantic Versioning][SemVer] doesn’t make a huge amount of sense. Instead, we’ve adopted [Calendar Versioning][CalVer], following, e.g., [Ubuntu][Ubuntu]. PLFA versions are of the form `YY.0M`, where `YY` is the short year, and `0M` is the zero-padded month. For each release, there are two tags in the repository: @@ -9,6 +27,7 @@ The former contains everything you’d need to work with that version of PLFA, w There are several steps to creating a new release for PLFA: +- [ ] Update the version in `plfa.cabal` to `YY.M` (no zero padding). - [ ] Create a new tag `dev-YY.0M` of the `dev` branch. - [ ] Create a new tag `web-YY.0M` of the `master` branch. - [ ] Push the new tags. diff --git a/Notes.md b/src/pages/notes.md similarity index 100% rename from Notes.md rename to src/pages/notes.md diff --git a/src/pages/style-guide.md b/src/pages/style-guide.md new file mode 100644 index 00000000..f0a8f227 --- /dev/null +++ b/src/pages/style-guide.md @@ -0,0 +1,256 @@ +--- +title : "Style guide for PLFA" +permalink : /StyleGuide/ +--- + +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. + +## File structure + +#### Module imports + +* All module imports should be placed at the top of the file immediately + after the module declaration. + +* If the module takes parameters that require imports from other files + then those imports only may be placed above the module declaration. + +* If it is important that certain names only come into scope later in + the file then the module should still be imported at the top of the + file but it can be given a shorter name using `as` and then opened + later on in the file when needed, e.g. + ```agda + import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality + ... + ... + open SetoidEquality S + ``` + +* The list of module imports should be in alphabetical order. + +* When using only a few items from a module, the items should be + enumerated in the import with `using` in order to make dependencies + clearer. + +#### Indentation + +* The contents of a top-level module should have zero indentation. + +* Every subsequent nested scope should then be indented by an additional + two spaces. + +* `where` blocks should be indented by two spaces and their contents + should be aligned with the `where`. + +* 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} + → 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. + +#### Module parameters + +* Module parameters should be put on a single line if they fit. + +* If they don't fit on a single line, then they should be spread out + over multiple lines, each indented by two spaces. If they can be + grouped logically by line then it is fine to do so, otherwise a line + each is probably clearest. + +* The `where` should go on it's own line at the end. + +* For example: + ```agda + module Relation.Binary.Reasoning.Base.Single + {a ℓ} {A : Set a} (_∼_ : Rel A ℓ) + (refl : Reflexive _∼_) (trans : Transitive _∼_) + where + ``` + +#### Reasoning layout + +* The `begin` clause should go on a new line. + +* Every subsequent combinator `_≡⟨_⟩_` should go on its own line, + with the intermediate terms on their own line, indented by two spaces. + +* The relation sign (e.g. `≡`) for each line should be aligned if possible. + +* For example: + ```agda + +-comm : Commutative _+_ + +-comm zero n = sym (+-identityʳ n) + +-comm (suc m) n = + begin + suc m + n + ≡⟨⟩ + suc (m + n) + ≡⟨ cong suc (+-comm m n) ⟩ + suc (n + m) + ≡⟨ sym (+-suc n m) ⟩ + n + suc m + ∎ + ``` + +* When multiple reasoning frameworks need to be used in the same file, the + `open` statement should always come in a where clause local to the + definition. This way users can easily see which reasoning toolkit is + being used. For instance: + ```agda + foo m n p = begin + (...) ∎ + where open ≤-Reasoning + ``` + +#### Record layout + +* The `record` declaration should go on the same line as the rest of the proof. + +* The next line with the first record item should start with a single `{`. + +* Every subsequent item of the record should go on its own line starting with + a `;`. + +* The final line should end with `}` on its own. + +* For example: + ```agda + ≤-isPreorder : IsPreorder _≡_ _≤_ + ≤-isPreorder = record + { isEquivalence = isEquivalence + ; reflexive = ≤-reflexive + ; trans = ≤-trans + } + ``` + +#### `where` blocks + +* `where` blocks are preferred rather than the `let` construction. + +* The `where` should be placed on the line below the main proof, + indented by two spaces. + +* If the contents of the block is non-trivial then types should be + provided alongside the terms, and all terms should be on lines after + the `where`, e.g. + ```agda + statement : Statement + statement = proof + where + proof : Proof + proof = some-very-long-proof + ``` + +* If the contents of the block is trivial or is an `open` statement then + it can provided on the same line as the `where` and a type can be + omitted, e.g. + ```agda + statement : Statement + statement = proof + where proof = x + ``` + +#### Other + +* Non-trivial proofs in `private` blocks are generally discouraged. If its + non-trivial then the chances are someone will want to reuse it as some + point! + +* The `with` syntax is preferred over the use of `case` from the `Function` + module. + +## Types + +#### Implicit and explicit arguments + +* Functions arguments should be implicit if they can "almost always" + be inferred. If there are common cases where they cannot be inferred + then they should be left explicit. + +* If there are lots of implicit arguments that are common to a collection + of proofs they should be extracted by using an anonymous module. + +* Implicit of type `Level` and `Set` can be generalised using `variable`. + At the moment the policy is *not* to generalise over any other types in + order to minimise the amount of information that users have to keep in + their head concurrently. + +## Naming conventions + +* Names should be descriptive - i.e. given the name of a proof and the + module it lives in then users should be able to make a reasonable + guess at what it contains. + +* Terms from other modules should only be renamed to avoid name clashes, + otherwise all names should be used as defined. + +* Datatype names should be capitalised and function names should be + lowercase. + +#### Variables + +* Natural variables are named `m`, `n`, `o`, ... (default `n`) + +* Integer variables are named `i`, `j`, `k`, ... (default `i`) + +* Rational variables are named `p`, `q`, `r`, ... (default `p`) + +* When naming proofs, the variables should occur in order, e.g. + `m≤n+m` rather than `n≤m+n`. + +* Collections of elements are usually indicated by appending an `s` + (e.g. if you are naming your variables `x` and `y` then lists + should be named `xs` and `ys`). + + +#### Preconditions and postconditions + +* Preconditions should only be included in names of results if + "important" (mostly judgement call). + +* Preconditions of results should be prepended to a description + of the result by using the symbol `⇒` in names (e.g. `asym⇒antisym`) + +* Preconditions and postconditions should be combined using the symbols + `∨` and `∧` (e.g. `m*n≡0⇒m≡0∨n≡0`) + +* Try to avoid the need for bracketing but if necessary use square + brackets (e.g. `[m∸n]⊓[n∸m]≡0`) + +#### Operators and relations + +* Operators and relations should be defined using mixfix notation where + applicable (e.g. `_+_`, `_<_`) + +* Common properties such as those in rings/orders/equivalences etc. + have defined abbreviations (e.g. commutativity is shortened to `comm`). + `Data.Nat.Properties` is a good place to look for examples. + +* Properties should be by prefixed by the relevant operator/relation + (e.g. commutativity of `_+_` is named `+-comm`) + +* If the relevant unicode characters are available, negated forms of + relations should be used over the `¬` symbol (e.g. `m+n≮n` should be + used instead of `¬m+n -
  • Andreas Abel
  • -
  • Catarina Coquand
  • -
  • Thierry Coquand
  • -
  • David Darais
  • -
  • Per Martin-Löf
  • -
  • Lena Magnusson
  • -
  • Conor McBride
  • -
  • James McKinna
  • -
  • Ulf Norell
  • - - -{% if site.contributors or site.extra_contributors %} -For pull requests big and small, and for answering questions on the Agda mailing list: - -
      -{% for contributor in site.contributors %} -
    • {{ contributor.name }}
    • -{% endfor %} -{% for contributor in site.extra_contributors %} - {% if contributor.name and contributor.github_username %} -
    • {{ contributor.name }}
    • - {% else %} - {% if contributor.name %} -
    • {{ contributor.name }}
    • - {% endif %} - {% if contributor.github_username %} -
    • {{ contributor.github_username }}
    • - {% endif %} - {% endif %} -{% endfor %} -
    • [Your name goes here]
    • -
    -{% else %} -{% endif %} - - -For support: - -* EPSRC Programme Grant EP/K034413/1 -* NSF Grant No. 1814460 -* Foundation Sciences Mathematiques de Paris (FSMP) - Distinguised Professor Fellowship diff --git a/src/plfa/announcements.md b/src/plfa/announcements.md deleted file mode 100644 index 50d696d7..00000000 --- a/src/plfa/announcements.md +++ /dev/null @@ -1,6 +0,0 @@ ---- -title : "Announcements" -layout : home -permalink : /Announcements/ ---- - diff --git a/src/plfa/Fonts.lagda.md b/src/plfa/backmatter/Fonts.lagda.md similarity index 98% rename from src/plfa/Fonts.lagda.md rename to src/plfa/backmatter/Fonts.lagda.md index d9e63ff2..b0c6f50c 100644 --- a/src/plfa/Fonts.lagda.md +++ b/src/plfa/backmatter/Fonts.lagda.md @@ -6,7 +6,7 @@ permalink : /Fonts/ --- ``` -module plfa.Fonts where +module plfa.backmatter.Fonts where ``` Preferably, all vertical bars should line up. diff --git a/src/plfa/backmatter/acknowledgements.md b/src/plfa/backmatter/acknowledgements.md new file mode 100644 index 00000000..a0df2d7a --- /dev/null +++ b/src/plfa/backmatter/acknowledgements.md @@ -0,0 +1,43 @@ +--- +title : "Acknowledgements" +layout : page +prev : /Untyped/ +permalink : /Acknowledgements/ +next : /Fonts/ +--- + +Thank you to: + + - The inventors of Agda, for a new playground. + - The authors of Software Foundations, for inspiration. + +A special thank you, for inventing ideas on which this book is based, and for hand-holding: +
    + - Andreas Abel + - Catarina Coquand + - Thierry Coquand + - David Darais + - Per Martin-Löf + - Lena Magnusson + - Conor McBride + - James McKinna + - Ulf Norell +
    + +$if(contributors)$ +For pull requests big and small, and for answering questions on the Agda mailing list: +
    +
      +$for(contributors)$ +
    • $name$
    • +$endfor$ +
    • [Your name goes here]
    • +
    +
    +$endif$ + +For support: + + - EPSRC Programme Grant EP/K034413/1 + - NSF Grant No. 1814460 + - Foundation Sciences Mathematiques de Paris (FSMP) Distinguised Professor Fellowship diff --git a/src/plfa/epub.md b/src/plfa/epub.md new file mode 100644 index 00000000..fef0519c --- /dev/null +++ b/src/plfa/epub.md @@ -0,0 +1,7 @@ +$for(parts)$ +# $title$ +$for(sections)$ +$content$ +$endfor$ +$endfor$ + diff --git a/src/plfa/dedication.md b/src/plfa/frontmatter/dedication.md similarity index 100% rename from src/plfa/dedication.md rename to src/plfa/frontmatter/dedication.md diff --git a/src/plfa/preface.md b/src/plfa/frontmatter/preface.md similarity index 99% rename from src/plfa/preface.md rename to src/plfa/frontmatter/preface.md index cb694ce0..4600d5d2 100644 --- a/src/plfa/preface.md +++ b/src/plfa/frontmatter/preface.md @@ -3,7 +3,7 @@ title : "Preface" layout : page prev : /Dedication/ permalink : /Preface/ -next : /Naturals/ +next : /GettingStarted/ --- The most profound connection between logic and computation is a pun. diff --git a/index.md b/src/plfa/index.md similarity index 52% rename from index.md rename to src/plfa/index.md index 5978bb27..0b74c630 100644 --- a/index.md +++ b/src/plfa/index.md @@ -1,6 +1,6 @@ --- -title : Table of Contents -layout : page +title : Table of Contents +permalink : / --- This book is an introduction to programming language theory using the @@ -11,54 +11,18 @@ remove, parts that require better explanation, good exercises, errors, and typos---are welcome. The book repository is on [GitHub]. Pull requests are encouraged. -## Front matter - - - [Dedication]({{ site.baseurl }}/Dedication/) - - [Preface]({{ site.baseurl }}/Preface/) - - [Getting Started]({{ site.baseurl }}/GettingStarted/) - -## Part 1: Logical Foundations - - - [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]({{ site.baseurl }}/Lambda/): Introduction to Lambda Calculus - - [Properties]({{ site.baseurl }}/Properties/): Progress and Preservation - - [DeBruijn]({{ site.baseurl }}/DeBruijn/): Intrinsically-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 - - [Confluence]({{ site.baseurl }}/Confluence/): Confluence of untyped lambda calculus - - [BigStep]({{ site.baseurl }}/BigStep/): Big-step semantics of untyped lambda calculus - -## Part 3: Denotational Semantics - - - [Denotational]({{ site.baseurl }}/Denotational/): Denotational semantics of untyped lambda calculus - - [Compositional]({{ site.baseurl }}/Compositional/): The denotational semantics is compositional - - [Soundness]({{ site.baseurl }}/Soundness/): Soundness of reduction with respect to denotational semantics - - [Adequacy]({{ site.baseurl }}/Adequacy/): Adequacy of denotational semantics with respect to operational semantics - - [ContextualEquivalence]({{ site.baseurl }}/ContextualEquivalence/): Denotational equality implies contextual equivalence - -## Appendix - - - [Substitution]({{ site.baseurl }}/Substitution/): Substitution in untyped lambda calculus - - -## Backmatter - - - [Acknowledgements]({{ site.baseurl }}/Acknowledgements/) - - [Fonts]({{ site.baseurl }}/Fonts/): Test page for fonts +$for(parts)$ +## $title$ + +$endfor$ ## Related diff --git a/src/plfa/meta.xml b/src/plfa/meta.xml new file mode 100644 index 00000000..0332ff23 --- /dev/null +++ b/src/plfa/meta.xml @@ -0,0 +1,7 @@ +$pagetitle$ +$for(authors)$ +$name$ +$endfor$ +$rights$ +$language$ +$modified$ diff --git a/src/plfa/part1/Connectives.lagda.md b/src/plfa/part1/Connectives.lagda.md index b5a2222d..de454e20 100644 --- a/src/plfa/part1/Connectives.lagda.md +++ b/src/plfa/part1/Connectives.lagda.md @@ -237,7 +237,7 @@ corresponds to `⟨ 1 , ⟨ true , aa ⟩ ⟩`, which is a member of the latter. #### Exercise `⇔≃×` (recommended) -Show that `A ⇔ B` as defined [earlier]({{ site.baseurl }}/Isomorphism/#iff) +Show that `A ⇔ B` as defined [earlier](/Isomorphism/#iff) is isomorphic to `(A → B) × (B → A)`. ``` @@ -796,9 +796,9 @@ The standard library constructs pairs with `_,_` whereas we use `⟨_,_⟩`. The former makes it convenient to build triples or larger tuples from pairs, permitting `a , b , c` to stand for `(a , (b , c))`. But it conflicts with other useful notations, such as `[_,_]` to construct a list of two elements in -Chapter [Lists]({{ site.baseurl }}/Lists/) +Chapter [Lists](/Lists/) and `Γ , A` to extend environments in -Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/). +Chapter [DeBruijn](/DeBruijn/). The standard library `_⇔_` is similar to ours, but the one in the standard library is less convenient, since it is parameterised with respect to an arbitrary notion of equivalence. diff --git a/src/plfa/part1/Decidable.lagda.md b/src/plfa/part1/Decidable.lagda.md index 57fb90c6..59805ba3 100644 --- a/src/plfa/part1/Decidable.lagda.md +++ b/src/plfa/part1/Decidable.lagda.md @@ -39,7 +39,7 @@ open import plfa.part1.Isomorphism using (_⇔_) ## Evidence vs Computation -Recall that Chapter [Relations]({{ site.baseurl }}/Relations/) +Recall that Chapter [Relations](/Relations/) defined comparison as an inductive datatype, which provides _evidence_ that one number is less than or equal to another: @@ -548,7 +548,7 @@ postulate #### Exercise `iff-erasure` (recommended) Give analogues of the `_⇔_` operation from -Chapter [Isomorphism]({{ site.baseurl }}/Isomorphism/#iff), +Chapter [Isomorphism](/Isomorphism/#iff), operation on booleans and decidables, and also show the corresponding erasure: ``` postulate @@ -564,7 +564,7 @@ postulate ## Proof by reflection {#proof-by-reflection} Let's revisit our definition of monus from -Chapter [Naturals]({{ site.baseurl }}/Naturals/). +Chapter [Naturals](/Naturals/). If we subtract a larger number from a smaller number, we take the result to be zero. We had to do something, after all. What could we have done differently? We could have defined a *guarded* version of minus, a function which subtracts `n` diff --git a/src/plfa/part1/Equality.lagda.md b/src/plfa/part1/Equality.lagda.md index 3d3c6d2e..51ac3041 100644 --- a/src/plfa/part1/Equality.lagda.md +++ b/src/plfa/part1/Equality.lagda.md @@ -347,7 +347,7 @@ an order that will make sense to the reader. #### Exercise `≤-Reasoning` (stretch) The proof of monotonicity from -Chapter [Relations]({{ site.baseurl }}/Relations/) +Chapter [Relations](/Relations/) can be written in a more readable form by using an analogue of our notation for `≡-Reasoning`. Define `≤-Reasoning` analogously, and use it to write out an alternative proof that addition is monotonic with diff --git a/src/plfa/part1/Induction.lagda.md b/src/plfa/part1/Induction.lagda.md index 055b7e4a..70468189 100644 --- a/src/plfa/part1/Induction.lagda.md +++ b/src/plfa/part1/Induction.lagda.md @@ -364,7 +364,7 @@ proof of associativity. The symbol `∀` appears in the statement of associativity to indicate that it holds for all numbers `m`, `n`, and `p`. We refer to `∀` as the _universal -quantifier_, and it is discussed further in Chapter [Quantifiers]({{ site.baseurl }}/Quantifiers/). +quantifier_, and it is discussed further in Chapter [Quantifiers](/Quantifiers/). Evidence for a universal quantifier is a function. The notations @@ -699,7 +699,7 @@ which is left as an exercise for the reader. Write out what is known about associativity of addition on each of the first four days using a finite story of creation, as -[earlier]({{ site.baseurl }}/Naturals/#finite-creation). +[earlier](/Naturals/#finite-creation). ``` -- Your code goes here @@ -952,7 +952,7 @@ for all `m`, `n`, and `p`. #### Exercise `Bin-laws` (stretch) {#Bin-laws} Recall that -Exercise [Bin]({{ site.baseurl }}/Naturals/#Bin) +Exercise [Bin](/Naturals/#Bin) defines a datatype `Bin` of bitstrings representing natural numbers, and asks you to define functions diff --git a/src/plfa/part1/Isomorphism.lagda.md b/src/plfa/part1/Isomorphism.lagda.md index c9836ba3..9b3f5334 100644 --- a/src/plfa/part1/Isomorphism.lagda.md +++ b/src/plfa/part1/Isomorphism.lagda.md @@ -89,7 +89,7 @@ Extensionality asserts that the only way to distinguish functions is by applying them; if two functions applied to the same argument always yield the same result, then they are the same function. It is the converse of `cong-app`, as introduced -[earlier]({{ site.baseurl }}/Equality/#cong). +[earlier](/Equality/#cong). Agda does not presume extensionality, but we can postulate that it holds: ``` @@ -104,7 +104,7 @@ known to be consistent with the theory that underlies Agda. As an example, consider that we need results from two libraries, one where addition is defined, as in -Chapter [Naturals]({{ site.baseurl }}/Naturals/), +Chapter [Naturals](/Naturals/), and one where it is defined the other way around. ``` _+′_ : ℕ → ℕ → ℕ @@ -170,7 +170,7 @@ the fourth that `to ∘ from` is the identity, hence the names. The declaration `open _≃_` makes available the names `to`, `from`, `from∘to`, and `to∘from`, otherwise we would need to write `_≃_.to` and so on. -The above is our first use of records. A record declaration behaves similar to a single-constructor data declaration (there are minor differences, which we discuss in [Connectives]({{ site.baseurl }}/Connectives/)): +The above is our first use of records. A record declaration behaves similar to a single-constructor data declaration (there are minor differences, which we discuss in [Connectives](/Connectives/)): ``` data _≃′_ (A B : Set): Set where mk-≃′ : ∀ (to : A → B) → @@ -468,8 +468,8 @@ Show that equivalence is reflexive, symmetric, and transitive. #### Exercise `Bin-embedding` (stretch) {#Bin-embedding} Recall that Exercises -[Bin]({{ site.baseurl }}/Naturals/#Bin) and -[Bin-laws]({{ site.baseurl }}/Induction/#Bin-laws) +[Bin](/Naturals/#Bin) and +[Bin-laws](/Induction/#Bin-laws) define a datatype `Bin` of bitstrings representing natural numbers, and asks you to define the following functions and predicates: diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md index ecd5f0f8..8dcc3541 100644 --- a/src/plfa/part1/Lists.lagda.md +++ b/src/plfa/part1/Lists.lagda.md @@ -177,7 +177,7 @@ and follows by straightforward computation combined with the inductive hypothesis. As usual, the inductive hypothesis is indicated by a recursive invocation of the proof, in this case `++-assoc xs ys zs`. -Recall that Agda supports [sections]({{ site.baseurl }}/Induction/#sections). +Recall that Agda supports [sections](/Induction/#sections). Applying `cong (x ∷_)` promotes the inductive hypothesis: (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs) @@ -966,7 +966,7 @@ Show that `Any` and `All` satisfy a version of De Morgan's Law: (Can you see why it is important that here `_∘_` is generalised to arbitrary levels, as described in the section on -[universe polymorphism]({{ site.baseurl }}/Equality/#unipoly)?) +[universe polymorphism](/Equality/#unipoly)?) Do we also have the following? diff --git a/src/plfa/part1/Naturals.lagda.md b/src/plfa/part1/Naturals.lagda.md index 3c2087b5..f6f1c199 100644 --- a/src/plfa/part1/Naturals.lagda.md +++ b/src/plfa/part1/Naturals.lagda.md @@ -1,7 +1,7 @@ --- title : "Naturals: Natural numbers" layout : page -prev : /Preface/ +prev : /GettingStarted/ permalink : /Naturals/ next : /Induction/ --- @@ -276,7 +276,7 @@ all the names specified in the `using` clause into the current scope. In this case, the names added are `begin_`, `_≡⟨⟩_`, and `_∎`. We will see how these are used below. We take these as givens for now, but will see how they are defined in -Chapter [Equality]({{ site.baseurl }}/Equality/). +Chapter [Equality](/Equality/). Agda uses underbars to indicate where terms appear in infix or mixfix operators. Thus, `_≡_` and `_≡⟨⟩_` are infix (each operator is written diff --git a/src/plfa/part1/Negation.lagda.md b/src/plfa/part1/Negation.lagda.md index b5f23a1a..bfb94cc4 100644 --- a/src/plfa/part1/Negation.lagda.md +++ b/src/plfa/part1/Negation.lagda.md @@ -189,7 +189,7 @@ again causing the equality to hold trivially. #### Exercise `<-irreflexive` (recommended) Using negation, show that -[strict inequality]({{ site.baseurl }}/Relations/#strict-inequality) +[strict inequality](/Relations/#strict-inequality) is irreflexive, that is, `n < n` holds for no `n`. ``` @@ -200,7 +200,7 @@ is irreflexive, that is, `n < n` holds for no `n`. #### Exercise `trichotomy` (practice) Show that strict inequality satisfies -[trichotomy]({{ site.baseurl }}/Relations/#trichotomy), +[trichotomy](/Relations/#trichotomy), that is, for any naturals `m` and `n` exactly one of the following holds: * `m < n` diff --git a/src/plfa/part1/Quantifiers.lagda.md b/src/plfa/part1/Quantifiers.lagda.md index 7349cd69..a51d91b2 100644 --- a/src/plfa/part1/Quantifiers.lagda.md +++ b/src/plfa/part1/Quantifiers.lagda.md @@ -97,7 +97,7 @@ postulate (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x) ``` Compare this with the result (`→-distrib-×`) in -Chapter [Connectives]({{ site.baseurl }}/Connectives/). +Chapter [Connectives](/Connectives/). #### Exercise `⊎∀-implies-∀⊎` (practice) @@ -242,7 +242,7 @@ Indeed, the converse also holds, and the two together form an isomorphism: ``` The result can be viewed as a generalisation of currying. Indeed, the code to establish the isomorphism is identical to what we wrote when discussing -[implication]({{ site.baseurl }}/Connectives/#implication). +[implication](/Connectives/#implication). #### Exercise `∃-distrib-⊎` (recommended) @@ -272,7 +272,7 @@ Show that `∃[ x ] B x` is isomorphic to `B aa ⊎ B bb ⊎ B cc`. ## An existential example Recall the definitions of `even` and `odd` from -Chapter [Relations]({{ site.baseurl }}/Relations/): +Chapter [Relations](/Relations/): ``` data even : ℕ → Set data odd : ℕ → Set @@ -441,9 +441,9 @@ Does the converse hold? If so, prove; if not, explain why. #### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism} Recall that Exercises -[Bin]({{ site.baseurl }}/Naturals/#Bin), -[Bin-laws]({{ site.baseurl }}/Induction/#Bin-laws), and -[Bin-predicates]({{ site.baseurl }}/Relations/#Bin-predicates) +[Bin](/Naturals/#Bin), +[Bin-laws](/Induction/#Bin-laws), and +[Bin-predicates](/Relations/#Bin-predicates) define a datatype `Bin` of bitstrings representing natural numbers, and asks you to define the following functions and predicates: diff --git a/src/plfa/part1/Relations.lagda.md b/src/plfa/part1/Relations.lagda.md index 3bf76ef2..7c35c4b5 100644 --- a/src/plfa/part1/Relations.lagda.md +++ b/src/plfa/part1/Relations.lagda.md @@ -167,7 +167,7 @@ either `(1 ≤ 2) ≤ 3` or `1 ≤ (2 ≤ 3)`. Given two numbers, it is straightforward to compute whether or not the first is less than or equal to the second. We don't give the code for doing so here, but will return to this point in -Chapter [Decidable]({{ site.baseurl }}/Decidable/). +Chapter [Decidable](/Decidable/). ## Inversion @@ -395,7 +395,7 @@ evidence of `m ≤ n` and `n ≤ m` respectively. (For those familiar with logic, the above definition could also be written as a disjunction. Disjunctions will -be introduced in Chapter [Connectives]({{ site.baseurl }}/Connectives/).) +be introduced in Chapter [Connectives](/Connectives/).) This is our first use of a datatype with _parameters_, in this case `m` and `n`. It is equivalent to the following @@ -590,7 +590,7 @@ It is also monotonic with regards to addition and multiplication. Most of the above are considered in exercises below. Irreflexivity requires negation, as does the fact that the three cases in trichotomy are mutually exclusive, so those points are deferred to -Chapter [Negation]({{ site.baseurl }}/Negation/). +Chapter [Negation](/Negation/). It is straightforward to show that `suc m ≤ n` implies `m < n`, and conversely. One can then give an alternative derivation of the @@ -617,7 +617,7 @@ Define `m > n` to be the same as `n < m`. You will need a suitable data declaration, similar to that used for totality. (We will show that the three cases are exclusive after we introduce -[negation]({{ site.baseurl }}/Negation/).) +[negation](/Negation/).) ``` -- Your code goes here @@ -760,7 +760,7 @@ Show that the sum of two odd numbers is even. #### Exercise `Bin-predicates` (stretch) {#Bin-predicates} Recall that -Exercise [Bin]({{ site.baseurl }}/Naturals/#Bin) +Exercise [Bin](/Naturals/#Bin) defines a datatype `Bin` of bitstrings representing natural numbers. Representations are not unique due to leading zeros. Hence, eleven may be represented by both of the following: @@ -820,7 +820,7 @@ import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total; ``` In the standard library, `≤-total` is formalised in terms of disjunction (which we define in -Chapter [Connectives]({{ site.baseurl }}/Connectives/)), +Chapter [Connectives](/Connectives/)), and `+-monoʳ-≤`, `+-monoˡ-≤`, `+-mono-≤` are proved differently than here, and more arguments are implicit. diff --git a/src/plfa/part2/BigStep.lagda.md b/src/plfa/part2/BigStep.lagda.md index 5c1114eb..7fe5025f 100644 --- a/src/plfa/part2/BigStep.lagda.md +++ b/src/plfa/part2/BigStep.lagda.md @@ -198,8 +198,7 @@ Before starting the proof, we establish a couple lemmas about equivalent environments and substitutions. The empty environment is equivalent to the identity substitution -`ids`, which we import from Chapter [Substitution]({{ site.baseurl -}}/Substitution/). +`ids`, which we import from Chapter [Substitution](/Substitution/). ``` ≈ₑ-id : ∅' ≈ₑ ids @@ -232,7 +231,7 @@ for the induction step we need the following lemma, which states that applying the composition of `exts σ` and `subst-zero` to `S x` is the same as just `σ x`, which is a corollary of a theorem in -Chapter [Substitution]({{ site.baseurl }}/Substitution/). +Chapter [Substitution](/Substitution/). ``` subst-zero-exts : ∀{Γ Δ}{σ : Subst Γ Δ}{B}{M : Δ ⊢ B}{x : Γ ∋ ★} diff --git a/src/plfa/part2/Bisimulation.lagda.md b/src/plfa/part2/Bisimulation.lagda.md index de161ea8..b6643798 100644 --- a/src/plfa/part2/Bisimulation.lagda.md +++ b/src/plfa/part2/Bisimulation.lagda.md @@ -119,14 +119,14 @@ above is a simulation from source to target. We leave establishing it in the reverse direction as an exercise. Another exercise is to show the alternative formulations of products in -Chapter [More]({{ site.baseurl }}/More/) +Chapter [More](/More/) are in bisimulation. ## Imports We import our source language from -Chapter [More]({{ site.baseurl }}/More/): +Chapter [More](/More/): ``` open import plfa.part2.More ``` @@ -164,7 +164,7 @@ data _~_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where ---------------------- → `let M N ~ (ƛ N†) · M† ``` -The language in Chapter [More]({{ site.baseurl }}/More/) has more constructs, which we could easily add. +The language in Chapter [More](/More/) has more constructs, which we could easily add. However, leaving the simulation small let's us focus on the essence. It's a handy technical trick that we can have a large source language, but only bother to include in the simulation the terms of interest. @@ -468,7 +468,7 @@ a bisimulation. #### Exercise `products` (practice) Show that the two formulations of products in -Chapter [More]({{ site.baseurl }}/More/) +Chapter [More](/More/) are in bisimulation. The only constructs you need to include are variables, and those connected to functions and products. In this case, the simulation is _not_ lock-step. diff --git a/src/plfa/part2/Confluence.lagda.md b/src/plfa/part2/Confluence.lagda.md index e9a796df..a0fc6bf7 100644 --- a/src/plfa/part2/Confluence.lagda.md +++ b/src/plfa/part2/Confluence.lagda.md @@ -1,5 +1,5 @@ --- -title : "Confluence: Confluence of untyped lambda calculus 🚧" +title : "Confluence: Confluence of untyped lambda calculus" layout : page prev : /Untyped/ permalink : /Confluence/ @@ -264,7 +264,7 @@ in turn relies on `rename`, we start with a version of the substitution lemma, called `par-rename`, that is specialized to renamings. The proof of `par-rename` relies on the fact that renaming and substitution commute with one another, which is a lemma that we -import from Chapter [Substitution]({{ site.baseurl }}/Substitution/) +import from Chapter [Substitution](/Substitution/) and restate here. ``` @@ -319,7 +319,7 @@ par-subst-exts s {x = S x} = par-rename s The next lemma that we need for proving that substitution respects parallel reduction is the following which states that simultaneoous substitution commutes with single substitution. We import this -lemma from Chapter [Substitution]({{ site.baseurl }}/Substitution/) +lemma from Chapter [Substitution](/Substitution/) and restate it below. ``` diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md index 6b8ac35a..63c9e707 100644 --- a/src/plfa/part2/DeBruijn.lagda.md +++ b/src/plfa/part2/DeBruijn.lagda.md @@ -70,10 +70,10 @@ And here is its corresponding type derivation: ∋z = Z (These are both taken from Chapter -[Lambda]({{ site.baseurl }}/Lambda/) +[Lambda](/Lambda/) and you can see the corresponding derivation tree written out in full -[here]({{ site.baseurl }}/Lambda/#derivation).) +[here](/Lambda/#derivation).) The two definitions are in close correspondence, where: * `` `_ `` corresponds to `` ⊢` `` @@ -126,7 +126,7 @@ which in context `Γ` have type `A`. While these two choices fit well, they are independent. One can use de Bruijn indices in raw terms, or have intrinsically-typed terms with names. In -Chapter [Untyped]({{ site.baseurl }}/Untyped/), +Chapter [Untyped](/Untyped/), we will introduce terms with de Bruijn indices that are intrinsically scoped but not typed. @@ -427,12 +427,11 @@ lookup : {Γ : Context} → {n : ℕ} → (p : n < length Γ) → Type lookup {(_ , A)} {zero} (s≤s z≤n) = A lookup {(Γ , _)} {(suc n)} (s≤s p) = lookup p ``` -The function takes a proof `p` that the natural number is within the -context's bounds. This guarantees we will never try to select a type -at a non-existing position within the context. Strict inequality `n < -length Γ` holds whenever inequality `suc n ≤ length Γ` holds. When -recursing, proof `p` is pattern-matched via the `s≤s` constructor to a -proof for a context with the rightmost type removed. + +We intend to apply the function only when the natural is +shorter than the length of the context, which we indicate by +postulating an `impossible` term, just as we did +[here](/Lambda/#primed). Given the above, we can convert a natural to a corresponding de Bruijn index, looking up its type in the context: @@ -471,9 +470,9 @@ _ = ƛ ƛ (# 1 · (# 1 · # 0)) ### Test examples {#examples} We repeat the test examples from -Chapter [Lambda]({{ site.baseurl }}/Lambda/). +Chapter [Lambda](/Lambda/). You can find them -[here]({{ site.baseurl }}/Lambda/#derivation) +[here](/Lambda/#derivation) for comparison. First, computing two plus two on naturals: @@ -806,7 +805,7 @@ data Value : ∀ {Γ A} → Γ ⊢ A → Set where Here `zero` requires an implicit parameter to aid inference, much in the same way that `[]` did in -[Lists]({{ site.baseurl }}/Lists/). +[Lists](/Lists/). ## Reduction diff --git a/src/plfa/part2/Inference.lagda.md b/src/plfa/part2/Inference.lagda.md index fb69dc36..da815c5a 100644 --- a/src/plfa/part2/Inference.lagda.md +++ b/src/plfa/part2/Inference.lagda.md @@ -12,9 +12,9 @@ module plfa.part2.Inference where So far in our development, type derivations for the corresponding term have been provided by fiat. -In Chapter [Lambda]({{ site.baseurl }}/Lambda/) +In Chapter [Lambda](/Lambda/) type derivations are extrinsic to the term, while -in Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/) +in Chapter [DeBruijn](/DeBruijn/) type derivations are intrinsic to the term, but in both we have written out the type derivations in full. @@ -28,9 +28,9 @@ inference, which will be presented in this chapter. This chapter ties our previous developments together. We begin with a term with some type annotations, close to the raw terms of -Chapter [Lambda]({{ site.baseurl }}/Lambda/), +Chapter [Lambda](/Lambda/), and from it we compute an intrinsically-typed term, in the style of -Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/). +Chapter [DeBruijn](/DeBruijn/). ## Introduction: Inference rules as algorithms {#algorithms} @@ -381,7 +381,7 @@ required for `sucᶜ`, which inherits its type as an argument of `plusᶜ`. ## Bidirectional type checking The typing rules for variables are as in -[Lambda]({{ site.baseurl }}/Lambda/): +[Lambda](/Lambda/): ``` data _∋_⦂_ : Context → Id → Type → Set where @@ -455,25 +455,25 @@ data _⊢_↓_ where → Γ ⊢ (M ↑) ↓ B ``` We follow the same convention as -Chapter [Lambda]({{ site.baseurl }}/Lambda/), +Chapter [Lambda](/Lambda/), prefacing the constructor with `⊢` to derive the name of the corresponding type rule. The rules are similar to those in -Chapter [Lambda]({{ site.baseurl }}/Lambda/), +Chapter [Lambda](/Lambda/), modified to support synthesised and inherited types. The two new rules are those for `⊢↓` and `⊢↑`. The former both passes the type decoration as the inherited type and returns it as the synthesised type. The latter takes the synthesised type and the inherited type and confirms they are identical --- it should remind you of the equality test in the application rule in the first -[section]({{ site.baseurl }}/Inference/#algorithms). +[section](/Inference/#algorithms). #### Exercise `bidirectional-mul` (recommended) {#bidirectional-mul} Rewrite your definition of multiplication from -Chapter [Lambda]({{ site.baseurl }}/Lambda/), decorated to support inference. +Chapter [Lambda](/Lambda/), decorated to support inference. ``` -- Your code goes here @@ -483,7 +483,7 @@ Chapter [Lambda]({{ site.baseurl }}/Lambda/), decorated to support inference. #### Exercise `bidirectional-products` (recommended) {#bidirectional-products} Extend the bidirectional type rules to include products from -Chapter [More]({{ site.baseurl }}/More/). +Chapter [More](/More/). ``` -- Your code goes here @@ -493,7 +493,7 @@ Chapter [More]({{ site.baseurl }}/More/). #### Exercise `bidirectional-rest` (stretch) Extend the bidirectional type rules to include the rest of the constructs from -Chapter [More]({{ site.baseurl }}/More/). +Chapter [More](/More/). ``` -- Your code goes here @@ -1003,7 +1003,7 @@ _ = refl From the evidence that a decorated term has the correct type it is easy to extract the corresponding intrinsically-typed term. We use the name `DB` to refer to the code in -Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/). +Chapter [DeBruijn](/DeBruijn/). It is easy to define an _erasure_ function that takes an extrinsic type judgment into the corresponding intrinsically-typed term. @@ -1066,17 +1066,17 @@ _ = refl ``` Thus, we have confirmed that bidirectional type inference converts decorated versions of the lambda terms from -Chapter [Lambda]({{ site.baseurl }}/Lambda/) +Chapter [Lambda](/Lambda/) to the intrinsically-typed terms of -Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/). +Chapter [DeBruijn](/DeBruijn/). #### Exercise `inference-multiplication` (recommended) Apply inference to your decorated definition of multiplication from -exercise [`bidirectional-mul`]({{ site.baseurl }}/Inference/#bidirectional-mul), and show that +exercise [`bidirectional-mul`](/Inference/#bidirectional-mul), and show that erasure of the inferred typing yields your definition of -multiplication from Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/). +multiplication from Chapter [DeBruijn](/DeBruijn/). ``` -- Your code goes here @@ -1085,7 +1085,7 @@ multiplication from Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/). #### Exercise `inference-products` (recommended) Using your rules from exercise -[`bidirectional-products`]({{ site.baseurl }}/Inference/#bidirectional-products), extend +[`bidirectional-products`](/Inference/#bidirectional-products), extend bidirectional inference to include products. ``` @@ -1095,7 +1095,7 @@ bidirectional inference to include products. #### Exercise `inference-rest` (stretch) Extend the bidirectional type rules to include the rest of the constructs from -Chapter [More]({{ site.baseurl }}/More/). +Chapter [More](/More/). ``` -- Your code goes here diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md index f6930d78..b64426d2 100644 --- a/src/plfa/part2/Lambda.lagda.md +++ b/src/plfa/part2/Lambda.lagda.md @@ -25,7 +25,7 @@ recursive function definitions. This chapter formalises the simply-typed lambda calculus, giving its syntax, small-step semantics, and typing rules. The next chapter -[Properties]({{ site.baseurl }}/Properties/) +[Properties](/Properties/) proves its main properties, including progress and preservation. Following chapters will look at a number of variants of lambda calculus. @@ -33,7 +33,7 @@ of variants of lambda calculus. Be aware that the approach we take here is _not_ our recommended approach to formalisation. Using de Bruijn indices and intrinsically-typed terms, as we will do in -Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/), +Chapter [DeBruijn](/DeBruijn/), leads to a more compact formulation. Nonetheless, we begin with named variables and extrinsically-typed terms, partly because names are easier than indices to read, @@ -143,7 +143,7 @@ plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒ ``` The recursive definition of addition is similar to our original definition of `_+_` for naturals, as given in -Chapter [Naturals]({{ site.baseurl }}/Naturals/#plus). +Chapter [Naturals](/Naturals/#plus). Here variable "m" is bound twice, once in a lambda abstraction and once in the successor branch of the case; the first use of "m" refers to the former and the second to the latter. Any use of "m" in the successor branch @@ -392,7 +392,7 @@ to treat variables as values, and to treat `ƛ x ⇒ N` as a value only if `N` is a value. Indeed, this is how Agda normalises terms. We consider this approach in -Chapter [Untyped]({{ site.baseurl }}/Untyped/). +Chapter [Untyped](/Untyped/). ## Substitution @@ -697,7 +697,7 @@ the reflexive and transitive closure `—↠` of the step relation `—→`. We define reflexive and transitive closure as a sequence of zero or more steps of the underlying relation, along lines similar to that for reasoning about chains of equalities in -Chapter [Equality]({{ site.baseurl }}/Equality/): +Chapter [Equality](/Equality/): ``` infix 2 _—↠_ infix 1 begin_ @@ -1098,7 +1098,7 @@ _ : ∅ , "x" ⦂ `ℕ ⇒ `ℕ , "y" ⦂ `ℕ , "z" ⦂ `ℕ ∋ "x" ⦂ `ℕ _ = S (λ()) (S (λ()) Z) ``` -Instead, we'll use a "smart constructor", which uses [proof by reflection]({{ site.baseurl }}/Decidable/#proof-by-reflection) to check the inequality while type checking: +Instead, we'll use a "smart constructor", which uses [proof by reflection](/Decidable/#proof-by-reflection) to check the inequality while type checking: ``` S′ : ∀ {Γ x y A B} @@ -1327,7 +1327,7 @@ We can fill in `Z` by hand. If we type C-c C-space, Agda will confirm we are don The entire process can be automated using Agsy, invoked with C-c C-a. -Chapter [Inference]({{ site.baseurl }}/Inference/) +Chapter [Inference](/Inference/) will show how to use Agda to compute type derivations directly. diff --git a/src/plfa/part2/More.lagda.md b/src/plfa/part2/More.lagda.md index 0ed573ac..e9144dfa 100644 --- a/src/plfa/part2/More.lagda.md +++ b/src/plfa/part2/More.lagda.md @@ -31,10 +31,10 @@ informal. We show how to formalise the first four constructs and leave the rest as an exercise for the reader. Our informal descriptions will be in the style of -Chapter [Lambda]({{ site.baseurl }}/Lambda/), +Chapter [Lambda](/Lambda/), using extrinsically-typed terms, while our formalisation will be in the style of -Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/), +Chapter [DeBruijn](/DeBruijn/), using intrinsically-typed terms. By now, explaining with symbols should be more concise, more precise, @@ -1236,7 +1236,7 @@ side to be well typed. ## Test examples -We repeat the [test examples]({{ site.baseurl }}/DeBruijn/#examples) from Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/), +We repeat the [test examples](/DeBruijn/#examples) from Chapter [DeBruijn](/DeBruijn/), in order to make sure we have not broken anything in the process of extending our base calculus. ``` two : ∀ {Γ} → Γ ⊢ `ℕ diff --git a/src/plfa/part2/Subtyping.lagda.md b/src/plfa/part2/Subtyping.lagda.md index f19a00e7..38de189f 100644 --- a/src/plfa/part2/Subtyping.lagda.md +++ b/src/plfa/part2/Subtyping.lagda.md @@ -503,7 +503,7 @@ Id = ℕ ``` Our terms are extrinsic, so we define a `Term` data type similar to -the one in the [Lambda]({{ site.baseurl }}/Lambda/) chapter, but adapted for de +the one in the [Lambda](/Lambda/) chapter, but adapted for de Bruijn indices. The two new term constructors are for record creation and field access. @@ -594,7 +594,7 @@ data _⊢*_⦂_ where → Γ ⊢* (M ∷ Ms) ⦂ (A ∷ As) ``` -Most of the typing rules are adapted from those in the [Lambda]({{ site.baseurl }}/Lambda/) +Most of the typing rules are adapted from those in the [Lambda](/Lambda/) chapter. Here we discuss the three new rules. * Rule `⊢rcd`: A record is well-typed if the field initializers `Ms` @@ -613,7 +613,7 @@ chapter. Here we discuss the three new rules. In preparation of defining the reduction rules for this language, we define simultaneous substitution using the same recipe as in the -[DeBruijn]({{ site.baseurl }}/DeBruijn/) chapter, but adapted to extrinsic +[DeBruijn](/DeBruijn/) chapter, but adapted to extrinsic terms. Thus, the `subst` function is split into two parts: a raw `subst` function that operators on terms and a `subst-pres` lemma that proves that substitution preserves types. We define `subst` in this @@ -784,7 +784,7 @@ We have just two new reduction rules: ## Canonical Forms -As in the [Properties]({{ site.baseurl }}/Properties/) chapter, we +As in the [Properties](/Properties/) chapter, we define a `Canonical V ⦂ A` relation that characterizes the well-typed values. The presence of the subsumption rule impacts its definition because we must allow the type of the value `V` to be a subtype of `A`. @@ -883,7 +883,7 @@ typed (C-rcd ⊢Ms dks As<:Bs) = ⊢<: (⊢rcd ⊢Ms dks) As<:Bs The Progress theorem states that a well-typed term may either take a reduction step or it is already a value. The proof of Progress is like -the one in the [Properties]({{ site.baseurl }}/Properties/); it +the one in the [Properties](/Properties/); it proceeds by induction on the typing derivation and most of the cases remain the same. Below we discuss the new cases for records and subsumption. @@ -961,7 +961,7 @@ As mentioned earlier, we need to prove that substitution preserve types, which in turn requires that renaming preserves types. The proofs of these lemmas are adapted from the intrinsic versions of the `ext`, `rename`, `exts`, and `subst` functions in the -[DeBruijn]({{ site.baseurl }}/DeBruijn/) chapter. +[DeBruijn](/DeBruijn/) chapter. We define the following abbreviation for a *well-typed renaming* from Γ to Δ, that is, a renaming that sends variables in Γ to variables in Δ diff --git a/src/plfa/part2/Untyped.lagda.md b/src/plfa/part2/Untyped.lagda.md index 33a76ffb..a4683ea6 100644 --- a/src/plfa/part2/Untyped.lagda.md +++ b/src/plfa/part2/Untyped.lagda.md @@ -67,7 +67,7 @@ open import Relation.Nullary.Product using (_×-dec_) ## Untyped is Uni-typed Our development will be close to that in -Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/), +Chapter [DeBruijn](/DeBruijn/), save that every term will have exactly the same type, written `★` and pronounced "any". This matches a slogan introduced by Dana Scott @@ -769,7 +769,7 @@ Confirm that two times two is four. #### Exercise `encode-more` (stretch) Along the lines above, encode all of the constructs of -Chapter [More]({{ site.baseurl }}/More/), +Chapter [More](/More/), save for primitive numbers, in the untyped lambda calculus. ``` @@ -812,7 +812,7 @@ L —↠⟨ L—↠M ⟩ M—↠N = —↠-trans L—↠M M—↠N ## Multi-step reduction is a congruence -Recall from Chapter [Induction]({{ site.baseurl }}/Induction/) that a +Recall from Chapter [Induction](/Induction/) that a relation `R` is a _congruence_ for a given function `f` if it is preserved by that function, i.e., if `R x y` then `R (f x) (f y)`. The term constructors `ƛ_` and `_·_` are functions, and so diff --git a/src/plfa/part3/Adequacy.lagda.md b/src/plfa/part3/Adequacy.lagda.md index a80acb9f..d88154a6 100644 --- a/src/plfa/part3/Adequacy.lagda.md +++ b/src/plfa/part3/Adequacy.lagda.md @@ -1,5 +1,5 @@ --- -title : "Adequacy: Adequacy of denotational semantics with respect to operational semantics 🚧" +title : "Adequacy: Adequacy of denotational semantics with respect to operational semantics" layout : page prev : /Soundness/ permalink : /Adequacy/ @@ -36,7 +36,7 @@ multi-step reduction a lambda abstraction. The recursive structure of the derivations for `γ ⊢ M ↓ (v ↦ w)` are completely different from the structure of multi-step reductions, so a direct proof would be challenging. However, The structure of `γ ⊢ M ↓ (v ↦ w)` closer to -that of [BigStep]({{ site.baseurl }}/BigStep/) call-by-name +that of [BigStep](/BigStep/) call-by-name evaluation. Further, we already proved that big-step evaluation implies multi-step reduction to a lambda (`cbn→reduce`). So we shall prove that `γ ⊢ M ↓ (v ↦ w)` implies that `γ' ⊢ M ⇓ c`, where `c` is a @@ -619,7 +619,7 @@ adequacy{M}{N} eq As promised, we return to the question of whether call-by-name evaluation is equivalent to beta reduction. In chapter -[BigStep]({{ site.baseurl }}/BigStep/) we established the forward +[BigStep](/BigStep/) we established the forward direction: that if call-by-name produces a result, then the program beta reduces to a lambda abstraction (`cbn→reduce`). We now prove the backward direction of the if-and-only-if, leveraging our results about the diff --git a/src/plfa/part3/Compositional.lagda.md b/src/plfa/part3/Compositional.lagda.md index 51d168a1..3ac341cc 100644 --- a/src/plfa/part3/Compositional.lagda.md +++ b/src/plfa/part3/Compositional.lagda.md @@ -1,5 +1,5 @@ --- -title : "Compositional: The denotational semantics is compositional 🚧" +title : "Compositional: The denotational semantics is compositional" layout : page prev : /Denotational/ permalink : /Compositional/ diff --git a/src/plfa/part3/ContextualEquivalence.lagda.md b/src/plfa/part3/ContextualEquivalence.lagda.md index 91496570..f49dacc1 100644 --- a/src/plfa/part3/ContextualEquivalence.lagda.md +++ b/src/plfa/part3/ContextualEquivalence.lagda.md @@ -1,5 +1,5 @@ --- -title : "ContextualEquivalence: Denotational equality implies contextual equivalence 🚧" +title : "ContextualEquivalence: Denotational equality implies contextual equivalence" layout : page prev : /Adequacy/ permalink : /ContextualEquivalence/ @@ -94,7 +94,7 @@ Putting these two facts together gives us ℰ (plug C N) ≃ ℰ (ƛN′). -We then apply `↓→⇓` from Chapter [Adequacy]({{ site.baseurl }}/Adequacy/) to deduce +We then apply `↓→⇓` from Chapter [Adequacy](/Adequacy/) to deduce ∅' ⊢ plug C N ⇓ clos (ƛ N′′) δ). diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index 66c4f2cb..8ba89a45 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/src/plfa/part3/Denotational.lagda.md @@ -1,5 +1,5 @@ --- -title : "Denotational: Denotational semantics of untyped lambda calculus 🚧" +title : "Denotational: Denotational semantics of untyped lambda calculus" layout : page prev : /BigStep/ permalink : /Denotational/ diff --git a/src/plfa/part3/Soundness.lagda.md b/src/plfa/part3/Soundness.lagda.md index 0915beae..3975bf56 100644 --- a/src/plfa/part3/Soundness.lagda.md +++ b/src/plfa/part3/Soundness.lagda.md @@ -1,5 +1,5 @@ --- -title : "Soundness: Soundness of reduction with respect to denotational semantics 🚧" +title : "Soundness: Soundness of reduction with respect to denotational semantics" layout : page prev : /Compositional/ permalink : /Soundness/ diff --git a/src/plfa/toc.metadata b/src/plfa/toc.metadata new file mode 100644 index 00000000..1d486af5 --- /dev/null +++ b/src/plfa/toc.metadata @@ -0,0 +1,45 @@ +--- +parts: +- title: "Front matter" + sections: + - src/plfa/frontmatter/dedication.md + - src/plfa/frontmatter/preface.md + - README.md +- title: "Part 1: Logical Foundations" + sections: + - src/plfa/part1/Naturals.lagda.md + - src/plfa/part1/Induction.lagda.md + - src/plfa/part1/Relations.lagda.md + - src/plfa/part1/Equality.lagda.md + - src/plfa/part1/Isomorphism.lagda.md + - src/plfa/part1/Connectives.lagda.md + - src/plfa/part1/Negation.lagda.md + - src/plfa/part1/Quantifiers.lagda.md + - src/plfa/part1/Decidable.lagda.md + - src/plfa/part1/Lists.lagda.md +- title: "Part 2: Programming Language Foundations" + sections: + - src/plfa/part2/Lambda.lagda.md + - src/plfa/part2/Properties.lagda.md + - src/plfa/part2/DeBruijn.lagda.md + - src/plfa/part2/More.lagda.md + - src/plfa/part2/Bisimulation.lagda.md + - src/plfa/part2/Inference.lagda.md + - src/plfa/part2/Untyped.lagda.md + - src/plfa/part2/Confluence.lagda.md + - src/plfa/part2/BigStep.lagda.md +- title: "Part 3: Denotational Semantics" + sections: + - src/plfa/part3/Denotational.lagda.md + - src/plfa/part3/Compositional.lagda.md + - src/plfa/part3/Soundness.lagda.md + - src/plfa/part3/Adequacy.lagda.md + - src/plfa/part3/ContextualEquivalence.lagda.md +- title: "Appendix" + sections: + - src/plfa/part2/Substitution.lagda.md +- title: "Back matter" + sections: + - src/plfa/backmatter/acknowledgements.md + - src/plfa/backmatter/Fonts.lagda.md +--- \ No newline at end of file diff --git a/stack.yaml b/stack.yaml new file mode 100644 index 00000000..3086cc57 --- /dev/null +++ b/stack.yaml @@ -0,0 +1,25 @@ +resolver: lts-16.16 +compiler: ghc-8.8.4 + +flags: + pandoc: + embed_data_files: true + +packages: +- . + +extra-deps: +# Sass dependencies: +- hsass-0.8.0@sha256:05fb3d435dbdf9f66a98db4e1ee57a313170a677e52ab3a5a05ced1fc42b0834,2899 +- hlibsass-0.1.10.1@sha256:08db56c633e9a83a642d8ea57dffa93112b092d05bf8f3b07491cfee9ee0dfa5,2565 +# Agda dependencies: +- Agda-2.6.1.1@sha256:d0f5051ae56de8417dc202cd7a8e23c9f21a75c69b44afb856b66b87ca8d54c4,32315 +- data-hash-0.2.0.1@sha256:0277d99cb8b535ecc375c59e55f1c91faab966d9167a946ef18445dd468ba727,1135 +- equivalence-0.3.5@sha256:aedbd070b7ab5e58dd1678cd85607bc33cb9ff62331c1fa098ca45063b3072db,1626 +- geniplate-mirror-0.7.7@sha256:6a698c1bcec25f4866999001c4de30049d4f8f00ec83f8930cda2f767489c637,1106 +- STMonadTrans-0.4.4@sha256:437eec4fdf5f56e9cd4360e08ed7f8f9f5f02ff3f1d634a14dbc71e890035387,1946 +# GitHub API dependencies: +- github-0.26@sha256:a9d4046325c3eb28cdc7bef2c3f5bb213328caeae0b7dce6f51de655f0bffaa1,7162 +- binary-instances-1.0.0.1@sha256:e234be994da675479a3661f050d4a1d53565c9ed7786d9a68b7a29ba8b54b5a7,2659 +# Regex dependencies: +- text-regex-replace-0.1.1.3@sha256:e7f612df671c93ced54a3d26528db37852069884e5cb67d5afbb49d3defb5eb9,1627 diff --git a/standard-library b/standard-library new file mode 160000 index 00000000..9f929b4f --- /dev/null +++ b/standard-library @@ -0,0 +1 @@ +Subproject commit 9f929b4fe28bb7ba74b6b95d01ed0958343f3451 diff --git a/templates/custom-head.html b/templates/custom-head.html new file mode 100755 index 00000000..e69de29b diff --git a/templates/default.html b/templates/default.html new file mode 100755 index 00000000..124e83f2 --- /dev/null +++ b/templates/default.html @@ -0,0 +1,13 @@ + + + $partial("templates/head.html")$ + + $partial("templates/header.html")$ +
    +
    + $body$ +
    +
    + $partial("templates/footer.html")$ + + diff --git a/templates/epub.html b/templates/epub.html new file mode 100644 index 00000000..4ee72389 --- /dev/null +++ b/templates/epub.html @@ -0,0 +1,26 @@ + + + + + + $pagetitle$ + + + + +
    +

    $pagetitle$

    +$for(authors)$ +

    $name$

    +$endfor$ +$if(rights)$ +
    $rights$
    + $endif$ +
    + + + +$$body$$ + + + diff --git a/templates/footer.html b/templates/footer.html new file mode 100755 index 00000000..0bde5163 --- /dev/null +++ b/templates/footer.html @@ -0,0 +1,31 @@ +
    + +
    + + $if(authors)$ + $for(authors)$ + + $endfor$ + $endif$ + This work is licensed under a $rights$ +
    +
    diff --git a/templates/google-analytics.html b/templates/google-analytics.html new file mode 100755 index 00000000..fec204df --- /dev/null +++ b/templates/google-analytics.html @@ -0,0 +1,8 @@ + + diff --git a/templates/head.html b/templates/head.html new file mode 100755 index 00000000..087d3547 --- /dev/null +++ b/templates/head.html @@ -0,0 +1,10 @@ + + + + + + $if(google-analytics)$ + $partial("templates/google-analytics.html")$ + $endif$ + $partial("templates/custom-head.html")$ + diff --git a/_includes/header.html b/templates/header.html old mode 100644 new mode 100755 similarity index 58% rename from _includes/header.html rename to templates/header.html index 40bfb117..b1786cc6 --- a/_includes/header.html +++ b/templates/header.html @@ -1,9 +1,6 @@ -