diff --git a/.gitignore b/.gitignore index 213e92cf..2d7777f3 100644 --- a/.gitignore +++ b/.gitignore @@ -21,5 +21,8 @@ Gemfile.lock *.spl *.synctex.gz +## EPUB files +*.epub + ## Emacs files -auto/ \ No newline at end of file +auto/ diff --git a/.travis.yml b/.travis.yml index 562cb668..7269268f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -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: diff --git a/Makefile b/Makefile index 9f7b534f..1ec23e5c 100644 --- a/Makefile +++ b/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 diff --git a/default-code-class.lua b/default-code-class.lua new file mode 100644 index 00000000..adb4706e --- /dev/null +++ b/default-code-class.lua @@ -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}} diff --git a/epub.css b/epub.css new file mode 100644 index 00000000..1daa27a1 --- /dev/null +++ b/epub.css @@ -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; + } +} diff --git a/fonts/DejaVuSansMono.ttf b/fonts/DejaVuSansMono.ttf new file mode 100644 index 00000000..f5786022 Binary files /dev/null and b/fonts/DejaVuSansMono.ttf differ diff --git a/fonts/LICENSE_dejavu.txt b/fonts/LICENSE_dejavu.txt new file mode 100644 index 00000000..df52c170 --- /dev/null +++ b/fonts/LICENSE_dejavu.txt @@ -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$ diff --git a/fonts/LICENSE_mononoki.txt b/fonts/LICENSE_mononoki.txt new file mode 100644 index 00000000..6ef130c5 --- /dev/null +++ b/fonts/LICENSE_mononoki.txt @@ -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. diff --git a/fonts/LICENSE_source_code_pro.txt b/fonts/LICENSE_source_code_pro.txt new file mode 100755 index 00000000..11773304 --- /dev/null +++ b/fonts/LICENSE_source_code_pro.txt @@ -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. diff --git a/fonts/SourceCodePro-Regular.ttf b/fonts/SourceCodePro-Regular.ttf new file mode 100644 index 00000000..c5830033 Binary files /dev/null and b/fonts/SourceCodePro-Regular.ttf differ diff --git a/fonts/mononoki-Regular.ttf b/fonts/mononoki-Regular.ttf new file mode 100644 index 00000000..9510ac85 Binary files /dev/null and b/fonts/mononoki-Regular.ttf differ diff --git a/include-files.lua b/include-files.lua new file mode 100644 index 00000000..5d70c890 --- /dev/null +++ b/include-files.lua @@ -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 diff --git a/index_epub.md b/index_epub.md new file mode 100644 index 00000000..1124e8d0 --- /dev/null +++ b/index_epub.md @@ -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 +``` + + \ No newline at end of file