Updated README
This commit is contained in:
parent
0c51f1069a
commit
1b59d9747e
2 changed files with 37 additions and 17 deletions
46
Makefile
46
Makefile
|
@ -4,65 +4,87 @@ markdown := $(subst tspl/,out/,$(subst src/,out/,$(subst .lagda,.md,$(agda))))
|
||||||
PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
|
PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
|
||||||
AGDA2HTML_FLAGS := --verbose --link-to-local-agda-names --use-jekyll=out/
|
AGDA2HTML_FLAGS := --verbose --link-to-local-agda-names --use-jekyll=out/
|
||||||
|
|
||||||
|
|
||||||
|
# Build PLFA and test hyperlinks
|
||||||
test: build
|
test: build
|
||||||
ruby -S bundle exec htmlproofer _site
|
ruby -S bundle exec htmlproofer _site
|
||||||
|
|
||||||
|
|
||||||
|
# Build PLFA and test hyperlinks offline
|
||||||
test-offline: build
|
test-offline: build
|
||||||
ruby -S bundle exec htmlproofer _site --disable-external
|
ruby -S bundle exec htmlproofer _site --disable-external
|
||||||
|
|
||||||
|
|
||||||
statistics:
|
statistics:
|
||||||
hs/agda-count
|
hs/agda-count
|
||||||
|
|
||||||
|
|
||||||
out/:
|
out/:
|
||||||
mkdir -p out/
|
mkdir -p out/
|
||||||
|
|
||||||
|
|
||||||
|
# Build PLFA pages
|
||||||
out/%.md: src/%.lagda | out/
|
out/%.md: src/%.lagda | out/
|
||||||
agda2html $(AGDA2HTML_FLAGS) -i $< -o $@ 2>&1 \
|
agda2html $(AGDA2HTML_FLAGS) -i $< -o $@ 2>&1 \
|
||||||
| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
|
| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
|
||||||
@sed -i '1 s|---|---\nsrc : $(<)|' $@
|
@sed -i '1 s|---|---\nsrc : $(<)|' $@
|
||||||
|
|
||||||
|
|
||||||
|
# Build TSPL pages
|
||||||
out/%.md: tspl/%.lagda | out/
|
out/%.md: tspl/%.lagda | out/
|
||||||
agda2html $(AGDA2HTML_FLAGS) -i $< -o $@ -- --include-path=$(realpath src) 2>&1 \
|
agda2html $(AGDA2HTML_FLAGS) -i $< -o $@ -- --include-path=$(realpath src) 2>&1 \
|
||||||
| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
|
| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
|
||||||
@sed -i '1 s|---|---\nsrc : $(<)|' $@
|
@sed -i '1 s|---|---\nsrc : $(<)|' $@
|
||||||
|
|
||||||
|
|
||||||
|
# Start server
|
||||||
serve:
|
serve:
|
||||||
ruby -S bundle exec jekyll serve --incremental
|
ruby -S bundle exec jekyll serve --incremental
|
||||||
|
|
||||||
# start server
|
|
||||||
|
# Start background server
|
||||||
server-start:
|
server-start:
|
||||||
ruby -S bundle exec jekyll serve --no-watch --detach
|
ruby -S bundle exec jekyll serve --no-watch --detach
|
||||||
|
|
||||||
# stop server
|
|
||||||
|
# Stop background server
|
||||||
server-stop:
|
server-stop:
|
||||||
pkill -f jekyll
|
pkill -f jekyll
|
||||||
|
|
||||||
# build website using jekyll (offline)
|
|
||||||
build-offline: $(markdown)
|
|
||||||
ruby -S bundle exec jekyll build
|
|
||||||
|
|
||||||
# build website using jekyll
|
# Build website using jekyll
|
||||||
build: AGDA2HTML_FLAGS += --link-to-agda-stdlib
|
build: AGDA2HTML_FLAGS += --link-to-agda-stdlib
|
||||||
build: $(markdown)
|
build: $(markdown)
|
||||||
ruby -S bundle exec jekyll build
|
ruby -S bundle exec jekyll build
|
||||||
|
|
||||||
# build website using jekyll incrementally
|
|
||||||
|
# Build website using jekyll offline
|
||||||
|
build-offline: $(markdown)
|
||||||
|
ruby -S bundle exec jekyll build
|
||||||
|
|
||||||
|
|
||||||
|
# Build website using jekyll incrementally
|
||||||
build-incremental: AGDA2HTML_FLAGS += --link-to-agda-stdlib
|
build-incremental: AGDA2HTML_FLAGS += --link-to-agda-stdlib
|
||||||
build-incremental: $(markdown)
|
build-incremental: $(markdown)
|
||||||
ruby -S bundle exec jekyll build --incremental
|
ruby -S bundle exec jekyll build --incremental
|
||||||
|
|
||||||
# remove all auxiliary files
|
|
||||||
|
# Remove all auxiliary files
|
||||||
clean:
|
clean:
|
||||||
ifneq ($(strip $(agdai)),)
|
ifneq ($(strip $(agdai)),)
|
||||||
rm $(agdai)
|
rm $(agdai)
|
||||||
endif
|
endif
|
||||||
|
|
||||||
# remove all generated files
|
|
||||||
|
# Remove all generated files
|
||||||
clobber: clean
|
clobber: clean
|
||||||
ruby -S bundle exec jekyll clean
|
ruby -S bundle exec jekyll clean
|
||||||
rm -rf out/
|
rm -rf out/
|
||||||
|
|
||||||
# install bundler, and gem dependencies
|
.phony: clobber
|
||||||
|
|
||||||
|
|
||||||
|
# MacOS Setup (install Bundler)
|
||||||
macos-setup:
|
macos-setup:
|
||||||
brew install libxml2
|
brew install libxml2
|
||||||
ruby -S gem install bundler --no-ri --no-rdoc
|
ruby -S gem install bundler --no-ri --no-rdoc
|
||||||
|
@ -70,12 +92,10 @@ macos-setup:
|
||||||
ruby -S bundle config build.nokogiri --use-system-libraries
|
ruby -S bundle config build.nokogiri --use-system-libraries
|
||||||
ruby -S bundle install
|
ruby -S bundle install
|
||||||
|
|
||||||
.phony: serve build test clean clobber macos-setup
|
.phony: macos-setup
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
# Travis Setup (install Agda, the Agda standard library, agda2html, acknowledgements, etc.)
|
# Travis Setup (install Agda, the Agda standard library, agda2html, acknowledgements, etc.)
|
||||||
|
|
||||||
travis-setup:\
|
travis-setup:\
|
||||||
$(HOME)/.local/bin/agda\
|
$(HOME)/.local/bin/agda\
|
||||||
$(HOME)/.local/bin/agda2html\
|
$(HOME)/.local/bin/agda2html\
|
||||||
|
|
|
@ -18,9 +18,7 @@ There are several tools you need to work with PLFA:
|
||||||
- [Agda standard library](https://github.com/agda/agda-stdlib)
|
- [Agda standard library](https://github.com/agda/agda-stdlib)
|
||||||
|
|
||||||
For most of the tools, you can simply follow their respective build instructions.
|
For most of the tools, you can simply follow their respective build instructions.
|
||||||
We aim to maintain compatibility with the latest release of Agda and the standard library,
|
We list the versions of our dependencies on the badges above.
|
||||||
but we maintain [a copy of the standard library which is guaranteed to work with the book](https://github.com/plfa/agda-stdlib).
|
|
||||||
If you use this copy, make sure to clone `plfa/agda-stdlib` instead of `agda/agda-stdlib`.
|
|
||||||
|
|
||||||
You can get the latest version of Programming Language Foundations in Agda from Github,
|
You can get the latest version of Programming Language Foundations in Agda from Github,
|
||||||
either by cloning the repository,
|
either by cloning the repository,
|
||||||
|
@ -63,10 +61,12 @@ You can host your copy of the book locally by running
|
||||||
|
|
||||||
The Makefile offers more than just these options:
|
The Makefile offers more than just these options:
|
||||||
|
|
||||||
make (builds lagda->markdown)
|
make (see make test)
|
||||||
make build (builds lagda->markdown and the website)
|
make build (builds lagda->markdown and the website)
|
||||||
|
make build-offline (builds lagda->markdown and the website offline)
|
||||||
make build-incremental (builds lagda->markdown and the website incrementally)
|
make build-incremental (builds lagda->markdown and the website incrementally)
|
||||||
make test (checks all links are valid)
|
make test (checks all links are valid)
|
||||||
|
make test-offline (checks all links are valid offline)
|
||||||
make serve (starts the server)
|
make serve (starts the server)
|
||||||
make server-start (starts the server in detached mode)
|
make server-start (starts the server in detached mode)
|
||||||
make server-stop (stops the server, uses pkill)
|
make server-stop (stops the server, uses pkill)
|
||||||
|
|
Loading…
Reference in a new issue