From 590961679c83fdb93eae772adf8abd16556dd71c Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Mon, 4 Jun 2018 13:17:37 +0100 Subject: [PATCH] Generate correct links in index.md; added 'make test' option which runs htmlproofer; excluded a number of files from the _site directory; these should've all been seperate commits, shouldn't they have? --- .travis.yml | 2 +- Gemfile | 1 + Gemfile.lock | 13 +++++++++++++ Makefile | 8 ++++++-- _config.yml | 10 +++++++--- index.md | 36 ++++++++++++++++++------------------ 6 files changed, 46 insertions(+), 24 deletions(-) diff --git a/.travis.yml b/.travis.yml index ff368391..d09aabdd 100644 --- a/.travis.yml +++ b/.travis.yml @@ -6,7 +6,7 @@ language: ruby # Caching so the next build will be fast too. cache: bundler: true - timeout: 1200 + timeout: 1500 directories: - $HOME/.stack - $HOME/.agda diff --git a/Gemfile b/Gemfile index 09c6b5ad..844813d5 100644 --- a/Gemfile +++ b/Gemfile @@ -2,3 +2,4 @@ source "https://rubygems.org" gem "minima", "~> 2.4.0" gem "github-pages", group: :jekyll_plugins +gem "html-proofer" diff --git a/Gemfile.lock b/Gemfile.lock index b786c42d..a8ccf1f1 100644 --- a/Gemfile.lock +++ b/Gemfile.lock @@ -13,6 +13,7 @@ GEM execjs coffee-script-source (1.11.1) colorator (1.1.0) + colorize (0.8.1) commonmarker (0.17.9) ruby-enum (~> 0.5) concurrent-ruby (1.0.5) @@ -83,6 +84,15 @@ GEM html-pipeline (2.8.0) activesupport (>= 2) nokogiri (>= 1.4) + html-proofer (3.9.1) + activesupport (>= 4.2, < 6.0) + addressable (~> 2.3) + colorize (~> 0.8) + mercenary (~> 0.3.2) + nokogiri (~> 1.8.1) + parallel (~> 1.3) + typhoeus (~> 1.3) + yell (~> 2.0) http_parser.rb (0.6.0) i18n (0.9.5) concurrent-ruby (~> 1.0) @@ -210,6 +220,7 @@ GEM mini_portile2 (~> 2.3.0) octokit (4.9.0) sawyer (~> 0.8.0, >= 0.5.3) + parallel (1.12.1) pathutil (0.16.1) forwardable-extended (~> 2.6) public_suffix (2.0.5) @@ -238,12 +249,14 @@ GEM tzinfo (1.2.5) thread_safe (~> 0.1) unicode-display_width (1.3.2) + yell (2.0.7) PLATFORMS ruby DEPENDENCIES github-pages + html-proofer minima (~> 2.4.0) BUNDLED WITH diff --git a/Makefile b/Makefile index c93c08a0..c6bc8062 100644 --- a/Makefile +++ b/Makefile @@ -2,7 +2,11 @@ agda := $(wildcard src/*.lagda) $(wildcard src/**/*.lagda) agdai := $(wildcard src/*.agdai) $(wildcard src/**/*.agdai) markdown := $(subst src/,out/,$(subst .lagda,.md,$(agda))) -all: bugfix $(markdown) +all: $(markdown) + +test: $(markdown) + ruby -S bundle exec jekyll build -d _site/sf/ + ruby -S bundle exec htmlproofer _site out/%.md: src/%.lagda mkdir -p out @@ -68,7 +72,7 @@ $(HOME)/agda2html-master/: cd $(HOME)/agda2html-master;\ stack install -.phony: serve build clean clobber macos-setup travis-setup +.phony: serve build test clean clobber macos-setup travis-setup # workaround for a bug in agda2html bugfix: diff --git a/_config.yml b/_config.yml index 44377bd6..cb7dcf29 100644 --- a/_config.yml +++ b/_config.yml @@ -28,6 +28,10 @@ url: "https://wenkokke.github.io/sf" markdown: kramdown theme: minima exclude: - - src/ - - Gemfile - - Gemfile.lock + - "src/" + - "extra/" + - "README.md" + - "Notes.md" + - "*.lagda" + - "Gemfile" + - "Gemfile.lock" diff --git a/index.md b/index.md index a38d0fb0..65cf767f 100644 --- a/index.md +++ b/index.md @@ -18,38 +18,38 @@ fixes are encouraged. ## Front matter - - [Preface](Preface) + - [Preface]({{ site.baseurl }}{% link out/Preface.md %}) ## Part 1: Logical Foundations (This part is ready for review. Please comment!) - - [Naturals: Natural numbers](Naturals) + - [Naturals: Natural numbers]({{ site.baseurl }}{% link out/Naturals.md %}) - [Properties: Proof by induction](Properties) - - [Relations: Inductive definition of relations](Relations) - - [Equality: Equality and equational reasoning](Equality) - - [Isomorphism: Isomorphism and embedding](Isomorphism) - - [Connectives: Conjunction, disjunction, and implication](Connectives) - - [Negation: Negation, with intuitionistic and classical Logic](Negation) - - [Quantifiers: Universals and existentials](Quantifiers) - - [Lists: Lists and higher-order functions](Lists) - - [Decidable: Booleans and decision procedures](Decidable) + - [Relations: Inductive definition of relations]({{ site.baseurl }}{% link out/Relations.md %}) + - [Equality: Equality and equational reasoning]({{ site.baseurl }}{% link out/Equality.md %}) + - [Isomorphism: Isomorphism and embedding]({{ site.baseurl }}{% link out/Isomorphism.md %}) + - [Connectives: Conjunction, disjunction, and implication]({{ site.baseurl }}{% link out/Connectives.md %}) + - [Negation: Negation, with intuitionistic and classical Logic]({{ site.baseurl }}{% link out/Negation.md %}) + - [Quantifiers: Universals and existentials]({{ site.baseurl }}{% link out/Quantifiers.md %}) + - [Lists: Lists and higher-order functions]({{ site.baseurl }}{% link out/Lists.md %}) + - [Decidable: Booleans and decision procedures]({{ site.baseurl }}{% link out/Decidable.md %}) ## Part 2: Programming Language Foundations (This part is not yet ready for review.) - - [Lambda: Lambda: Introduction to Lambda Calculus](Lambda) - - [LambdaProp: Properties of Simply-Typed Lambda Calculus](LambdaProp) - - [DeBruijn: Inherently typed De Bruijn representation](DeBruijn) - - [Extensions: Extensions to simply-typed lambda calculus](Extensions) - - [Inference: Bidirectional type inference](Inference) - - [Untyped: Untyped lambda calculus with full normalisation](Untyped) + - [Lambda: Lambda: Introduction to Lambda Calculus]({{ site.baseurl }}{% link out/Lambda.md %}) + - [LambdaProp: Properties of Simply-Typed Lambda Calculus]({{ site.baseurl }}{% link out/LambdaProp.md %}) + - [DeBruijn: Inherently typed De Bruijn representation]({{ site.baseurl }}{% link out/DeBruijn.md %}) + - [Extensions: Extensions to simply-typed lambda calculus]({{ site.baseurl }}{% link out/Extensions.md %}) + - [Inference: Bidirectional type inference]({{ site.baseurl }}{% link out/Inference.md %}) + - [Untyped: Untyped lambda calculus with full normalisation]({{ site.baseurl }}{% link out/Untyped.md %}) ## Backmatter - - [Acknowledgements](Acknowledgements) - - [Fonts: Test page for fonts](Fonts) + - [Acknowledgements]({{ site.baseurl }}{% link out/Acknowledgements.md %}) + - [Fonts: Test page for fonts]({{ site.baseurl }}{% link out/Fonts.md %}) [sf]: https://softwarefoundations.cis.upenn.edu/ [wen]: https://github.com/wenkokke