Merge pull request #479 from mreed20/pandoc
Add EPUB creation to the build
This commit is contained in:
Wen Kokke
GitHub
commit
631798263e
13 changed files with 630 additions and 4 deletions
3
.gitignore
vendored
3
.gitignore
vendored
|
|
@ -21,5 +21,8 @@ Gemfile.lock
|
|||
*.spl
|
||||
*.synctex.gz
|
||||
|
||||
## EPUB files
|
||||
*.epub
|
||||
|
||||
## Emacs files
|
||||
auto/
|
||||
|
|
@ -39,6 +39,7 @@ script:
|
|||
- travis_retry curl -L https://raw.githubusercontent.com/plfa/git-tools/master/git-restore-mtime | python
|
||||
- agda --version
|
||||
- acknowledgements --version
|
||||
- pandoc --version
|
||||
- make test-offline # disable to only build cache
|
||||
|
||||
before_deploy:
|
||||
|
|
|
|||
46
Makefile
46
Makefile
|
|
@ -1,6 +1,7 @@
|
|||
SHELL := /usr/bin/env bash
|
||||
AGDA := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.lagda.md')
|
||||
AGDAI := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.agdai')
|
||||
LUA := $(shell find . -name '*.lua')
|
||||
MARKDOWN := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA))))
|
||||
PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
|
||||
|
||||
|
|
@ -12,7 +13,7 @@ endif
|
|||
|
||||
|
||||
# Build PLFA and test hyperlinks
|
||||
test: build
|
||||
test: build epub
|
||||
ruby -S bundle exec htmlproofer '_site'
|
||||
|
||||
|
||||
|
|
@ -35,6 +36,39 @@ statistics:
|
|||
out/:
|
||||
mkdir -p out/
|
||||
|
||||
# EPUB generation notes
|
||||
#
|
||||
# - The "Apple Books" app on Mac does not show syntax highlighting.
|
||||
# The Thorium app on Mac, however, does.
|
||||
#
|
||||
# - Regarding --epub-chapter-level, from the docs (https://pandoc.org/MANUAL.html):
|
||||
#
|
||||
# "Specify the heading level at which to split the EPUB into separate “chapter”
|
||||
# files. The default is to split into chapters at level-1 headings. This option
|
||||
# only affects the internal composition of the EPUB, not the way chapters and
|
||||
# sections are displayed to users. Some readers may be slow if the chapter
|
||||
# files are too large, so for large documents with few level-1 headings, one
|
||||
# might want to use a chapter level of 2 or 3."
|
||||
#
|
||||
#TODO: embedded fonts not working (path problem?)
|
||||
|
||||
epub: out/plfa.epub
|
||||
|
||||
out/plfa.epub: out/ $(AGDA) $(LUA) epub.css fonts/*.ttf
|
||||
pandoc --strip-comments \
|
||||
--css=epub.css \
|
||||
--epub-embed-font='fonts/*.ttf' \
|
||||
--lua-filter include-files.lua \
|
||||
--lua-filter default-code-class.lua -M default-code-class=agda \
|
||||
--standalone \
|
||||
--fail-if-warnings \
|
||||
--toc --toc-depth=2 \
|
||||
--epub-chapter-level=2 \
|
||||
-o "$@" \
|
||||
index_epub.md
|
||||
|
||||
|
||||
|
||||
|
||||
# Convert literal Agda to Markdown
|
||||
define AGDA_template
|
||||
|
|
@ -120,7 +154,8 @@ travis-setup:\
|
|||
$(HOME)/.local/bin/acknowledgements\
|
||||
$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src\
|
||||
$(HOME)/.agda/defaults\
|
||||
$(HOME)/.agda/libraries
|
||||
$(HOME)/.agda/libraries\
|
||||
/usr/bin/pandoc
|
||||
|
||||
.phony: travis-setup
|
||||
|
||||
|
|
@ -133,6 +168,11 @@ $(HOME)/.local/bin/acknowledgements:
|
|||
cd $(HOME)/acknowledgements-master;\
|
||||
stack install
|
||||
|
||||
# The version of pandoc on Xenial is too old.
|
||||
/usr/bin/pandoc:
|
||||
curl -L https://github.com/jgm/pandoc/releases/download/2.9.2.1/pandoc-2.9.2.1-1-amd64.deb -o $(HOME)/pandoc.deb
|
||||
dpkg -i $(HOME)/pandoc.deb
|
||||
|
||||
travis-uninstall-acknowledgements:
|
||||
rm -rf $(HOME)/acknowledgements-master/
|
||||
rm $(HOME)/.local/bin/acknowledgements
|
||||
|
|
@ -185,4 +225,4 @@ travis-uninstall-agda-stdlib:
|
|||
|
||||
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
|
||||
.phony: travis-install-agda-stdlib travis-uninstall-agda-stdlib travis-reinstall-agda-stdlib epub
|
||||
|
|
|
|||
26
default-code-class.lua
Normal file
26
default-code-class.lua
Normal file
|
|
@ -0,0 +1,26 @@
|
|||
-- Source:
|
||||
-- https://github.com/jgm/pandoc/issues/2104#issuecomment-595878750
|
||||
--
|
||||
-- Assign a code class to all code blocks lacking one. Unlike the
|
||||
-- command-line flag "--indented-code-classes", which only applies
|
||||
-- to indented code blocks, this lua filter applies to all inline
|
||||
-- code elements, including fenced code blocks.
|
||||
|
||||
local default_code_classes = {}
|
||||
|
||||
function add_default_code_class(el)
|
||||
if #(el.classes) == 0 then
|
||||
el.classes = default_code_classes
|
||||
return el
|
||||
end
|
||||
end
|
||||
|
||||
function get_default_code_class(meta)
|
||||
if meta['default-code-class'] then
|
||||
default_code_classes = {pandoc.utils.stringify(meta['default-code-class'])}
|
||||
end
|
||||
end
|
||||
|
||||
return {{Meta = get_default_code_class},
|
||||
{Code = add_default_code_class},
|
||||
{CodeBlock = add_default_code_class}}
|
||||
48
epub.css
Normal file
48
epub.css
Normal file
|
|
@ -0,0 +1,48 @@
|
|||
/* This is Pandoc's default ebook CSS, modified slightly. */
|
||||
/* https://github.com/jgm/pandoc/blob/master/data/epub.css */
|
||||
@font-face {
|
||||
font-family: 'mononoki';
|
||||
font-weight: normal;
|
||||
font-style: normal;
|
||||
src: url('../fonts/mononoki-Regular.ttf');
|
||||
}
|
||||
@font-face {
|
||||
font-family: 'DejaVu Sans Mono';
|
||||
font-weight: normal;
|
||||
font-style: normal;
|
||||
src: url('../fonts/DejaVuSansMono.ttf');
|
||||
}
|
||||
@font-face {
|
||||
font-family: 'Source Code Pro';
|
||||
font-weight: normal;
|
||||
font-style: normal;
|
||||
src: url('../fonts/SourceCodePro-Regular.ttf');
|
||||
}
|
||||
/* TODO: add freemono font from agda.css */
|
||||
body { margin: 5%; text-align: justify; font-size: medium; }
|
||||
code { font-family: 'mononoki', 'DejaVu Sans Mono', 'Source Code Pro', monospace; }
|
||||
h1 { text-align: left; }
|
||||
h2 { text-align: left; }
|
||||
h3 { text-align: left; }
|
||||
h4 { text-align: left; }
|
||||
h5 { text-align: left; }
|
||||
h6 { text-align: left; }
|
||||
nav#toc ol,
|
||||
nav#landmarks ol { padding: 0; margin-left: 1em; }
|
||||
nav#toc ol li,
|
||||
nav#landmarks ol li { list-style-type: none; margin: 0; padding: 0; }
|
||||
a.footnote-ref { vertical-align: super; }
|
||||
em, em em em, em em em em em { font-style: italic;}
|
||||
em em, em em em em { font-style: normal; }
|
||||
code{ white-space: pre-wrap; }
|
||||
span.smallcaps{ font-variant: small-caps; }
|
||||
span.underline{ text-decoration: underline; }
|
||||
q { quotes: "“" "”" "‘" "’"; }
|
||||
div.column{ display: inline-block; vertical-align: top; width: 50%; }
|
||||
div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
|
||||
@media screen { /* Workaround for iBooks issue; see #6242 */
|
||||
.sourceCode {
|
||||
overflow: visible !important;
|
||||
white-space: pre-wrap !important;
|
||||
}
|
||||
}
|
||||
BIN
fonts/DejaVuSansMono.ttf
Normal file
BIN
fonts/DejaVuSansMono.ttf
Normal file
Binary file not shown.
187
fonts/LICENSE_dejavu.txt
Normal file
187
fonts/LICENSE_dejavu.txt
Normal file
|
|
@ -0,0 +1,187 @@
|
|||
Fonts are (c) Bitstream (see below). DejaVu changes are in public domain.
|
||||
Glyphs imported from Arev fonts are (c) Tavmjong Bah (see below)
|
||||
|
||||
|
||||
Bitstream Vera Fonts Copyright
|
||||
------------------------------
|
||||
|
||||
Copyright (c) 2003 by Bitstream, Inc. All Rights Reserved. Bitstream Vera is
|
||||
a trademark of Bitstream, Inc.
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy
|
||||
of the fonts accompanying this license ("Fonts") and associated
|
||||
documentation files (the "Font Software"), to reproduce and distribute the
|
||||
Font Software, including without limitation the rights to use, copy, merge,
|
||||
publish, distribute, and/or sell copies of the Font Software, and to permit
|
||||
persons to whom the Font Software is furnished to do so, subject to the
|
||||
following conditions:
|
||||
|
||||
The above copyright and trademark notices and this permission notice shall
|
||||
be included in all copies of one or more of the Font Software typefaces.
|
||||
|
||||
The Font Software may be modified, altered, or added to, and in particular
|
||||
the designs of glyphs or characters in the Fonts may be modified and
|
||||
additional glyphs or characters may be added to the Fonts, only if the fonts
|
||||
are renamed to names not containing either the words "Bitstream" or the word
|
||||
"Vera".
|
||||
|
||||
This License becomes null and void to the extent applicable to Fonts or Font
|
||||
Software that has been modified and is distributed under the "Bitstream
|
||||
Vera" names.
|
||||
|
||||
The Font Software may be sold as part of a larger software package but no
|
||||
copy of one or more of the Font Software typefaces may be sold by itself.
|
||||
|
||||
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
|
||||
OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF MERCHANTABILITY,
|
||||
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT OF COPYRIGHT, PATENT,
|
||||
TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL BITSTREAM OR THE GNOME
|
||||
FOUNDATION BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, INCLUDING
|
||||
ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL DAMAGES,
|
||||
WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF
|
||||
THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM OTHER DEALINGS IN THE
|
||||
FONT SOFTWARE.
|
||||
|
||||
Except as contained in this notice, the names of Gnome, the Gnome
|
||||
Foundation, and Bitstream Inc., shall not be used in advertising or
|
||||
otherwise to promote the sale, use or other dealings in this Font Software
|
||||
without prior written authorization from the Gnome Foundation or Bitstream
|
||||
Inc., respectively. For further information, contact: fonts at gnome dot
|
||||
org.
|
||||
|
||||
Arev Fonts Copyright
|
||||
------------------------------
|
||||
|
||||
Copyright (c) 2006 by Tavmjong Bah. All Rights Reserved.
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining
|
||||
a copy of the fonts accompanying this license ("Fonts") and
|
||||
associated documentation files (the "Font Software"), to reproduce
|
||||
and distribute the modifications to the Bitstream Vera Font Software,
|
||||
including without limitation the rights to use, copy, merge, publish,
|
||||
distribute, and/or sell copies of the Font Software, and to permit
|
||||
persons to whom the Font Software is furnished to do so, subject to
|
||||
the following conditions:
|
||||
|
||||
The above copyright and trademark notices and this permission notice
|
||||
shall be included in all copies of one or more of the Font Software
|
||||
typefaces.
|
||||
|
||||
The Font Software may be modified, altered, or added to, and in
|
||||
particular the designs of glyphs or characters in the Fonts may be
|
||||
modified and additional glyphs or characters may be added to the
|
||||
Fonts, only if the fonts are renamed to names not containing either
|
||||
the words "Tavmjong Bah" or the word "Arev".
|
||||
|
||||
This License becomes null and void to the extent applicable to Fonts
|
||||
or Font Software that has been modified and is distributed under the
|
||||
"Tavmjong Bah Arev" names.
|
||||
|
||||
The Font Software may be sold as part of a larger software package but
|
||||
no copy of one or more of the Font Software typefaces may be sold by
|
||||
itself.
|
||||
|
||||
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
|
||||
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
|
||||
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
|
||||
OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL
|
||||
TAVMJONG BAH BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
|
||||
INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
|
||||
DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
|
||||
FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
|
||||
OTHER DEALINGS IN THE FONT SOFTWARE.
|
||||
|
||||
Except as contained in this notice, the name of Tavmjong Bah shall not
|
||||
be used in advertising or otherwise to promote the sale, use or other
|
||||
dealings in this Font Software without prior written authorization
|
||||
from Tavmjong Bah. For further information, contact: tavmjong @ free
|
||||
. fr.
|
||||
|
||||
TeX Gyre DJV Math
|
||||
-----------------
|
||||
Fonts are (c) Bitstream (see below). DejaVu changes are in public domain.
|
||||
|
||||
Math extensions done by B. Jackowski, P. Strzelczyk and P. Pianowski
|
||||
(on behalf of TeX users groups) are in public domain.
|
||||
|
||||
Letters imported from Euler Fraktur from AMSfonts are (c) American
|
||||
Mathematical Society (see below).
|
||||
Bitstream Vera Fonts Copyright
|
||||
Copyright (c) 2003 by Bitstream, Inc. All Rights Reserved. Bitstream Vera
|
||||
is a trademark of Bitstream, Inc.
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy
|
||||
of the fonts accompanying this license (“Fonts”) and associated
|
||||
documentation
|
||||
files (the “Font Software”), to reproduce and distribute the Font Software,
|
||||
including without limitation the rights to use, copy, merge, publish,
|
||||
distribute,
|
||||
and/or sell copies of the Font Software, and to permit persons to whom
|
||||
the Font Software is furnished to do so, subject to the following
|
||||
conditions:
|
||||
|
||||
The above copyright and trademark notices and this permission notice
|
||||
shall be
|
||||
included in all copies of one or more of the Font Software typefaces.
|
||||
|
||||
The Font Software may be modified, altered, or added to, and in particular
|
||||
the designs of glyphs or characters in the Fonts may be modified and
|
||||
additional
|
||||
glyphs or characters may be added to the Fonts, only if the fonts are
|
||||
renamed
|
||||
to names not containing either the words “Bitstream” or the word “Vera”.
|
||||
|
||||
This License becomes null and void to the extent applicable to Fonts or
|
||||
Font Software
|
||||
that has been modified and is distributed under the “Bitstream Vera”
|
||||
names.
|
||||
|
||||
The Font Software may be sold as part of a larger software package but
|
||||
no copy
|
||||
of one or more of the Font Software typefaces may be sold by itself.
|
||||
|
||||
THE FONT SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS
|
||||
OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF MERCHANTABILITY,
|
||||
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT OF COPYRIGHT, PATENT,
|
||||
TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL BITSTREAM OR THE GNOME
|
||||
FOUNDATION
|
||||
BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, INCLUDING ANY GENERAL,
|
||||
SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL DAMAGES, WHETHER IN AN
|
||||
ACTION
|
||||
OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF THE USE OR
|
||||
INABILITY TO USE
|
||||
THE FONT SOFTWARE OR FROM OTHER DEALINGS IN THE FONT SOFTWARE.
|
||||
Except as contained in this notice, the names of GNOME, the GNOME
|
||||
Foundation,
|
||||
and Bitstream Inc., shall not be used in advertising or otherwise to promote
|
||||
the sale, use or other dealings in this Font Software without prior written
|
||||
authorization from the GNOME Foundation or Bitstream Inc., respectively.
|
||||
For further information, contact: fonts at gnome dot org.
|
||||
|
||||
AMSFonts (v. 2.2) copyright
|
||||
|
||||
The PostScript Type 1 implementation of the AMSFonts produced by and
|
||||
previously distributed by Blue Sky Research and Y&Y, Inc. are now freely
|
||||
available for general use. This has been accomplished through the
|
||||
cooperation
|
||||
of a consortium of scientific publishers with Blue Sky Research and Y&Y.
|
||||
Members of this consortium include:
|
||||
|
||||
Elsevier Science IBM Corporation Society for Industrial and Applied
|
||||
Mathematics (SIAM) Springer-Verlag American Mathematical Society (AMS)
|
||||
|
||||
In order to assure the authenticity of these fonts, copyright will be
|
||||
held by
|
||||
the American Mathematical Society. This is not meant to restrict in any way
|
||||
the legitimate use of the fonts, such as (but not limited to) electronic
|
||||
distribution of documents containing these fonts, inclusion of these fonts
|
||||
into other public domain or commercial font collections or computer
|
||||
applications, use of the outline data to create derivative fonts and/or
|
||||
faces, etc. However, the AMS does require that the AMS copyright notice be
|
||||
removed from any derivative versions of the fonts which have been altered in
|
||||
any way. In addition, to ensure the fidelity of TeX documents using Computer
|
||||
Modern fonts, Professor Donald Knuth, creator of the Computer Modern faces,
|
||||
has requested that any alterations which yield different font metrics be
|
||||
given a different name.
|
||||
|
||||
$Id$
|
||||
94
fonts/LICENSE_mononoki.txt
Normal file
94
fonts/LICENSE_mononoki.txt
Normal file
|
|
@ -0,0 +1,94 @@
|
|||
Copyright (c) 2013, Matthias Tellen matthias.tellen@googlemail.com,
|
||||
with Reserved Font Name monoOne.
|
||||
|
||||
This Font Software is licensed under the SIL Open Font License, Version 1.1.
|
||||
This license is copied below, and is also available with a FAQ at:
|
||||
http://scripts.sil.org/OFL
|
||||
|
||||
|
||||
-----------------------------------------------------------
|
||||
SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
|
||||
-----------------------------------------------------------
|
||||
|
||||
PREAMBLE
|
||||
The goals of the Open Font License (OFL) are to stimulate worldwide
|
||||
development of collaborative font projects, to support the font creation
|
||||
efforts of academic and linguistic communities, and to provide a free and
|
||||
open framework in which fonts may be shared and improved in partnership
|
||||
with others.
|
||||
|
||||
The OFL allows the licensed fonts to be used, studied, modified and
|
||||
redistributed freely as long as they are not sold by themselves. The
|
||||
fonts, including any derivative works, can be bundled, embedded,
|
||||
redistributed and/or sold with any software provided that any reserved
|
||||
names are not used by derivative works. The fonts and derivatives,
|
||||
however, cannot be released under any other type of license. The
|
||||
requirement for fonts to remain under this license does not apply
|
||||
to any document created using the fonts or their derivatives.
|
||||
|
||||
DEFINITIONS
|
||||
"Font Software" refers to the set of files released by the Copyright
|
||||
Holder(s) under this license and clearly marked as such. This may
|
||||
include source files, build scripts and documentation.
|
||||
|
||||
"Reserved Font Name" refers to any names specified as such after the
|
||||
copyright statement(s).
|
||||
|
||||
"Original Version" refers to the collection of Font Software components as
|
||||
distributed by the Copyright Holder(s).
|
||||
|
||||
"Modified Version" refers to any derivative made by adding to, deleting,
|
||||
or substituting -- in part or in whole -- any of the components of the
|
||||
Original Version, by changing formats or by porting the Font Software to a
|
||||
new environment.
|
||||
|
||||
"Author" refers to any designer, engineer, programmer, technical
|
||||
writer or other person who contributed to the Font Software.
|
||||
|
||||
PERMISSION & CONDITIONS
|
||||
Permission is hereby granted, free of charge, to any person obtaining
|
||||
a copy of the Font Software, to use, study, copy, merge, embed, modify,
|
||||
redistribute, and sell modified and unmodified copies of the Font
|
||||
Software, subject to the following conditions:
|
||||
|
||||
1) Neither the Font Software nor any of its individual components,
|
||||
in Original or Modified Versions, may be sold by itself.
|
||||
|
||||
2) Original or Modified Versions of the Font Software may be bundled,
|
||||
redistributed and/or sold with any software, provided that each copy
|
||||
contains the above copyright notice and this license. These can be
|
||||
included either as stand-alone text files, human-readable headers or
|
||||
in the appropriate machine-readable metadata fields within text or
|
||||
binary files as long as those fields can be easily viewed by the user.
|
||||
|
||||
3) No Modified Version of the Font Software may use the Reserved Font
|
||||
Name(s) unless explicit written permission is granted by the corresponding
|
||||
Copyright Holder. This restriction only applies to the primary font name as
|
||||
presented to the users.
|
||||
|
||||
4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
|
||||
Software shall not be used to promote, endorse or advertise any
|
||||
Modified Version, except to acknowledge the contribution(s) of the
|
||||
Copyright Holder(s) and the Author(s) or with their explicit written
|
||||
permission.
|
||||
|
||||
5) The Font Software, modified or unmodified, in part or in whole,
|
||||
must be distributed entirely under this license, and must not be
|
||||
distributed under any other license. The requirement for fonts to
|
||||
remain under this license does not apply to any document created
|
||||
using the Font Software.
|
||||
|
||||
TERMINATION
|
||||
This license becomes null and void if any of the above conditions are
|
||||
not met.
|
||||
|
||||
DISCLAIMER
|
||||
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
|
||||
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
|
||||
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
|
||||
OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
|
||||
COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
|
||||
INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
|
||||
DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
|
||||
FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
|
||||
OTHER DEALINGS IN THE FONT SOFTWARE.
|
||||
93
fonts/LICENSE_source_code_pro.txt
Executable file
93
fonts/LICENSE_source_code_pro.txt
Executable file
|
|
@ -0,0 +1,93 @@
|
|||
Copyright 2010, 2012 Adobe Systems Incorporated (http://www.adobe.com/), with Reserved Font Name 'Source'. All Rights Reserved. Source is a trademark of Adobe Systems Incorporated in the United States and/or other countries.
|
||||
|
||||
This Font Software is licensed under the SIL Open Font License, Version 1.1.
|
||||
|
||||
This license is copied below, and is also available with a FAQ at: http://scripts.sil.org/OFL
|
||||
|
||||
|
||||
-----------------------------------------------------------
|
||||
SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
|
||||
-----------------------------------------------------------
|
||||
|
||||
PREAMBLE
|
||||
The goals of the Open Font License (OFL) are to stimulate worldwide
|
||||
development of collaborative font projects, to support the font creation
|
||||
efforts of academic and linguistic communities, and to provide a free and
|
||||
open framework in which fonts may be shared and improved in partnership
|
||||
with others.
|
||||
|
||||
The OFL allows the licensed fonts to be used, studied, modified and
|
||||
redistributed freely as long as they are not sold by themselves. The
|
||||
fonts, including any derivative works, can be bundled, embedded,
|
||||
redistributed and/or sold with any software provided that any reserved
|
||||
names are not used by derivative works. The fonts and derivatives,
|
||||
however, cannot be released under any other type of license. The
|
||||
requirement for fonts to remain under this license does not apply
|
||||
to any document created using the fonts or their derivatives.
|
||||
|
||||
DEFINITIONS
|
||||
"Font Software" refers to the set of files released by the Copyright
|
||||
Holder(s) under this license and clearly marked as such. This may
|
||||
include source files, build scripts and documentation.
|
||||
|
||||
"Reserved Font Name" refers to any names specified as such after the
|
||||
copyright statement(s).
|
||||
|
||||
"Original Version" refers to the collection of Font Software components as
|
||||
distributed by the Copyright Holder(s).
|
||||
|
||||
"Modified Version" refers to any derivative made by adding to, deleting,
|
||||
or substituting -- in part or in whole -- any of the components of the
|
||||
Original Version, by changing formats or by porting the Font Software to a
|
||||
new environment.
|
||||
|
||||
"Author" refers to any designer, engineer, programmer, technical
|
||||
writer or other person who contributed to the Font Software.
|
||||
|
||||
PERMISSION & CONDITIONS
|
||||
Permission is hereby granted, free of charge, to any person obtaining
|
||||
a copy of the Font Software, to use, study, copy, merge, embed, modify,
|
||||
redistribute, and sell modified and unmodified copies of the Font
|
||||
Software, subject to the following conditions:
|
||||
|
||||
1) Neither the Font Software nor any of its individual components,
|
||||
in Original or Modified Versions, may be sold by itself.
|
||||
|
||||
2) Original or Modified Versions of the Font Software may be bundled,
|
||||
redistributed and/or sold with any software, provided that each copy
|
||||
contains the above copyright notice and this license. These can be
|
||||
included either as stand-alone text files, human-readable headers or
|
||||
in the appropriate machine-readable metadata fields within text or
|
||||
binary files as long as those fields can be easily viewed by the user.
|
||||
|
||||
3) No Modified Version of the Font Software may use the Reserved Font
|
||||
Name(s) unless explicit written permission is granted by the corresponding
|
||||
Copyright Holder. This restriction only applies to the primary font name as
|
||||
presented to the users.
|
||||
|
||||
4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
|
||||
Software shall not be used to promote, endorse or advertise any
|
||||
Modified Version, except to acknowledge the contribution(s) of the
|
||||
Copyright Holder(s) and the Author(s) or with their explicit written
|
||||
permission.
|
||||
|
||||
5) The Font Software, modified or unmodified, in part or in whole,
|
||||
must be distributed entirely under this license, and must not be
|
||||
distributed under any other license. The requirement for fonts to
|
||||
remain under this license does not apply to any document created
|
||||
using the Font Software.
|
||||
|
||||
TERMINATION
|
||||
This license becomes null and void if any of the above conditions are
|
||||
not met.
|
||||
|
||||
DISCLAIMER
|
||||
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
|
||||
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
|
||||
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
|
||||
OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
|
||||
COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
|
||||
INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
|
||||
DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
|
||||
FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
|
||||
OTHER DEALINGS IN THE FONT SOFTWARE.
|
||||
BIN
fonts/SourceCodePro-Regular.ttf
Normal file
BIN
fonts/SourceCodePro-Regular.ttf
Normal file
Binary file not shown.
BIN
fonts/mononoki-Regular.ttf
Normal file
BIN
fonts/mononoki-Regular.ttf
Normal file
Binary file not shown.
61
include-files.lua
Normal file
61
include-files.lua
Normal file
|
|
@ -0,0 +1,61 @@
|
|||
--- include-files.lua – filter to include Markdown files
|
||||
---
|
||||
--- Copyright: © 2019–2020 Albert Krewinkel
|
||||
--- Copyright: © 2020 Michael Reed
|
||||
--- License: MIT – see LICENSE file for details
|
||||
---
|
||||
--- Created by Albert Krewinkel. Slightly modified by Michael Reed for use in
|
||||
--- generating the EPUB for "Programming Language Foundations in Agda".
|
||||
---
|
||||
--- For documentation, see: https://github.com/pandoc/lua-filters/tree/master/include-files
|
||||
|
||||
-- pandoc's List type
|
||||
local List = require 'pandoc.List'
|
||||
|
||||
--- Shift headings in block list by given number
|
||||
function shift_headings(blocks, shift_by)
|
||||
if not shift_by then
|
||||
return blocks
|
||||
end
|
||||
|
||||
local shift_headings_filter = {
|
||||
Header = function (header)
|
||||
header.level = header.level + shift_by
|
||||
return header
|
||||
end
|
||||
}
|
||||
|
||||
return pandoc.walk_block(pandoc.Div(blocks), shift_headings_filter).content
|
||||
end
|
||||
|
||||
--- Filter function for code blocks
|
||||
function CodeBlock(cb)
|
||||
-- ignore code blocks which are not of class "include".
|
||||
if not cb.classes:includes 'include' then
|
||||
return
|
||||
end
|
||||
|
||||
-- Markdown is used if this is nil.
|
||||
local format = cb.attributes['format']
|
||||
local shift_heading_level_by =
|
||||
tonumber(cb.attributes['shift-heading-level-by'])
|
||||
|
||||
|
||||
local blocks = List:new()
|
||||
for line in cb.text:gmatch('[^\n]+') do
|
||||
if line:sub(1,2) ~= '//' then
|
||||
-- Read in the document at the file path specified by `line`.
|
||||
local fh = io.open(line)
|
||||
local document = pandoc.read(fh:read '*a', format)
|
||||
-- Before shifting headings, add a title heading at the beginning of the chapter.
|
||||
local heading = pandoc.Header(1, pandoc.Str(pandoc.utils.stringify(document.meta.title)))
|
||||
document.blocks:insert(1, heading)
|
||||
-- Shift all headings by the user-specified amount, which is 0 by default.
|
||||
local chapter = shift_headings(document.blocks, shift_heading_level_by)
|
||||
-- Concatenate the chapter blocks (discarding the metadata) to the current document.
|
||||
blocks:extend(chapter)
|
||||
fh:close()
|
||||
end
|
||||
end
|
||||
return blocks
|
||||
end
|
||||
73
index_epub.md
Normal file
73
index_epub.md
Normal file
|
|
@ -0,0 +1,73 @@
|
|||
---
|
||||
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}
|
||||
src/plfa/acknowledgements.md
|
||||
src/plfa/Fonts.lagda.md
|
||||
src/plfa/statistics.md
|
||||
```
|
||||
|
||||
<!-- TODO: include the rest of the stuff on https://plfa.github.io/ -->
|
||||
Loading…
Reference in a new issue