michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
2262 commits 2 branches 4 tags 85 MiB
Commit graph

2262 commits

This branch
This branch
All branches
Author Message Date
Wen Kokke
9dad13717d Fix pandoc install on Travis 2020-06-16 11:12:50 +01:00
Wen Kokke
631798263e
Merge pull request #479 from mreed20/pandoc 
Add EPUB creation to the build
 2020-06-16 11:06:44 +01:00
Michael Reed
5857550a43 Revert "Add internal link checker" 
This reverts commit dbed30c659.
For whatever reason, some erroneous links are not detected with
this script, but are detected with epubchecker. So let's just use
epubchecker when the time comes.
 2020-06-15 18:42:39 -04:00
Michael Reed
e790ed3b92 Fail on pandoc warnings 2020-06-15 18:32:34 -04:00
Michael Reed
1d6a0c3ca3 Review: Hook the EPUB build up to Travis 2020-06-15 18:32:31 -04:00
Michael Reed
75c6db936b epub.css: Remove false note. 
The warning is not related to the contents of `epub.css`.
See https://github.com/jgm/pandoc/pull/6464 for more info.
 2020-06-15 17:49:43 -04:00
Michael Reed
dbed30c659 Add internal link checker 
This should make the link rewriting process easier. As this does
the same job as epubChecker, it can probably be removed once
epubChecker is integrated into the build process.
 2020-06-15 14:24:29 -04:00
Michael Reed
02bf885d6b epub.css: Remove empty rules 
This quells some VSCode warnings
 2020-06-15 14:21:56 -04:00
Michael Reed
ed33201f61 epub.css: Fix path to embedded fonts 
Found with the help of Calibre.
 2020-06-15 12:34:06 -04:00
Michael Reed
031ad315b3 Review: Cleanup epub target 
- List all dependencies of the `epub` target
- Create non-phony `out/plfa.epub` target, which the phony target `epub`
  is a synonym of.
 2020-06-15 11:36:49 -04:00
Michael Reed
feea0a57d2 Review: Makefile: "make clean" should not remove the .epub 
Note that clobber already removes the `out` directory.
 2020-06-15 11:19:53 -04:00
Michael Reed
3a9845dd3c Review: Makefile: Embed all fonts in fonts directory 2020-06-15 11:16:38 -04:00
Michael Reed
a045f2f8a8 Review: Remove stray copy of DejaVuSansMono.ttf 
There's already a copy in the `fonts` directory.
 2020-06-15 11:15:08 -04:00
Michael Reed
55c7a10e23 Add EPUB creation to the build 
The EPUB is created with `pandoc` in combination with Lua filters, which
rewrite the abstract syntax tree to be more suitable for EPUB creation.
In particular all headings in the markdown files `part[123]/*.lagda.md`
are shifted up by 1 (e.g., level 1 heading -> level 2 heading), so that
we can make a level 1 heading for Appendix, Frontmatter, and different
parts of the book. This is done to match the structure on the website [1].

Syntax highlighting is done using pandoc's builtin syntax highlighter
(which uses the Haskell library `skylighting`). In other words, we do
not use `highlight.sh`, so the syntax highlighting is slightly different
than the website version of the book. This could certainly be dealt with
later.

What follows is a list of things that are currently broken, which is
probably not exhaustive:
- The `Acknowledgements` section is broken.
- Embedded fonts don't work. They're necessary for some ereaders, like my old Sony PRS-300.
- All inline links are broken. I could rewrite them with a Lua filter
  and some regex, although that's not very nice :)
- `epubcheck` validation fails for a variety of reasons.

Closes #112.

[1]: https://plfa.github.io/
[2]: https://github.com/w3c/epubcheck
 2020-06-14 21:28:56 -04:00
Philip Wadler
44fb26193f
Merge pull request #478 from mdimjasevic/lambda-highlighting-1 
Lambda: fix highlighting of bindings in the text
 2020-06-08 08:43:25 +01:00
Marko Dimjašević
3673bc8d26
Lambda: fix highlighting of bindings in the text 2020-06-07 22:38:34 +02:00
Philip Wadler
2b0f229c93
Merge pull request #477 from mdimjasevic/prop-line-break 
Properties: fix the rendering of a highlighted expression
 2020-06-07 10:23:55 +01:00
Marko Dimjašević
fed1bc2610
Properties: fix the rendering of a highlighted expression by removing a line break in the expression 2020-06-06 21:04:25 +02:00
Jeremy Siek
47cb1433db new verion of the book! beta.md -> index.md 2020-06-04 09:57:27 -04:00
Wen Kokke
8013d91afb
Pragmatic note on matching against decidable equality 2020-06-02 10:33:48 +01:00
wadler
406918768d more publishing stuff 2020-05-29 10:17:50 -03:00
wadler
07934be2b5 merge 2020-05-29 10:17:10 -03:00
wadler
23a84b75d3 publishing info and final pdf 2020-05-29 10:16:30 -03:00
Wen Kokke
eb6e9d93c5 Fix small error 2020-05-22 20:46:40 +01:00
Wen Kokke
5ae6438e8f Restructured Getting Started. 2020-05-22 20:45:35 +01:00
Wen Kokke
6700cf597d Rewrote Getting Started to provide instructions for installing a specific version of Agda. 2020-05-22 18:21:25 +01:00
Wen Kokke
8d59de6394 Added rewrite of Inference by Prabhakar 2020-05-22 15:50:50 +01:00
Wen Kokke
7eea42d370 Minor changes in highlight script. 2020-05-22 15:46:54 +01:00
Jeremy Siek
5bfc503eec remove second premise from cong-rename 2020-05-20 09:05:06 -04:00
Jeremy G. Siek
bfff5d01cb
Merge pull request #474 from L-TChen/patch-1 
Fix cong-rename
 2020-05-20 09:03:04 -04:00
Liang-Ting Chen
33f0f64624
Fix cong-rename 
M on the right hand side of ≡ should be M′
 2020-05-20 16:12:54 +08:00
wadler
0a99b734ba added line about imports for exercises to preface 2020-05-11 12:17:04 -03:00
Jeremy Siek
fcf981cfec added explanation to exercise 2020-05-06 15:01:41 -04:00
Jeremy Siek
3d614523dc fix mixup regarding former/later and description of import 2020-05-03 15:16:41 -04:00
wadler
6a3fec78b6 updates to index page 2020-04-30 15:23:40 -03:00
wadler
f2cb91fc30 added Levy suggestion to extra 2020-04-30 08:36:48 -03:00
Philip Wadler
77499be10c
Modified Peter's proposed text on argument order 2020-04-21 15:42:33 -03:00
Philip Wadler
8da824a96a
Add paragraph about order of arguments to x ≟ y 
Thank you to Peter Thiemann for suggesting a paragraph on this subject.
 2020-04-21 10:50:41 -03:00
Peter Thiemann
8b9fc489c3 pragmatic note on matching against decidable equality 2020-04-21 15:05:52 +02:00
Peter Thiemann
6ba26bbfc8 Agda 2.6.1 doesn't recognize it's terminating 2020-04-21 14:55:12 +02:00
wadler
6428b87def added import to Qualifiers 2020-04-18 12:20:03 -03:00
wadler
c76da31328 merge 2020-04-17 12:16:18 -03:00
wadler
29157501d4 added proj_2 to imports in Qualifiers 2020-04-17 12:14:55 -03:00
Jeremy Siek
963fc985b0 moved exercise to come later 2020-04-10 13:55:52 -04:00
Jeremy Siek
09a91451b2 fix links 2020-04-09 09:27:24 -04:00
Jeremy Siek
433587bc61 more edits 2020-04-09 09:18:30 -04:00
Jeremy Siek
2afe5706a1 some edits 2020-04-09 09:15:25 -04:00
Jeremy Siek
2dc431121e simplified D^c 2020-04-07 08:19:03 -04:00
Jeremy Siek
3ab180ad8d tweak 2020-04-01 09:30:52 -04:00
Jeremy Siek
d1f628ceae changed the denot-church exercise 2020-03-31 16:07:45 -04:00