Any chance of getting a PDF version?

[roman-kashitsyn]

First, thank you so much, the book looks extremely useful!

The online version looks amazing, but there's one minor issue: I prefer reading books away from computer, using my E-Ink device. I can imaging that a lot of people have similar preferences.

So a PDF version of the book (or at least instructions how to make one) would be very helpful.

[wenkokke]

This should be possible, and I have created similar setups in the past – where .lagda source compiles to a website and to a PDF – but we're not currently working on this.

[wadler]

Roman, As Wen says, we're not working on this currently. If you would like to add a way to do this to the repository, that would be most welcome.

[Kwezan]

Ways to do this are relatively simple. You can use ready-made applications such as a Adobe Acrobat DC, which quickly and easy translates HTML pages into pdf files or even the PdfCrowd tool (https://pdfcrowd.com).

[wenkokke]

@Kwezan Those tools might work, but they'll be translating the HTML to a PDF. Since we have Markdown source for the book, and we can translate the literate Agda parts to LaTeX using agda, I feel we can do much better if we set up a script which runs the book through LaTeX.

[ice1000]

FYI the 2.6.0 release of Agda will bring a new feature that translates the Agda codes in .lagda.md files into HTML and leave other parts preserved (so the output file can be post-processed by a markdown renderer and become nice HTML. Example: https://ice1000.org/lagda/MuGenHackingToTheGate.html).

[wenkokke]

@ice1000 Awesome news! That'll be very useful! Unfortunately, at this point, there's a couple of other features of agda2html that we've come to depend on, but we might be able to switch over to just using Agda in time!

[ice1000]

Wow, you have agda2html. I didn't know about that.
What features? Can you elaborate?

Maybe it'll be helpful for improving Agda's HTML backend, too.

[wenkokke]

@ice1000 Sorry, it's not exceedingly well-documented. It has the ability to:

• strip implicit arguments from Agda code,
  to make the code more readable and look more like Haskell or Idris
• whenever Agda inserts a link to the definition of a symbol,
  if it's a symbol from the standard library,
  create a link to the online HTML documentation of the Agda standard library
• resolve custom Markdown links to Agda modules which are in scope, e.g., [...][DeBruijn],
  to the appropriate url, based on the local filesystem

[ice1000]

strip implicit arguments from Agda code, to make the code more readable and look more like Haskell or Idris

In Agda 2.6.0 you'll have

variable
 i : Level
 A : Set i

id : A -> A -- A is generalized according to the variable definitions above
id a = a

Related docs: https://people.inf.elte.hu/divip/AIMXXVIII.pdf

[ice1000]

whenever Agda inserts a link to the definition of a symbol,
if it's a symbol from the standard library,
create a link to the online HTML documentation of the Agda standard library

This is interesting! We haven't thought about that yet. Good idea!

[ice1000]

resolve custom Markdown links to Agda modules which are in scope, e.g., [...][DeBruijn],
to the appropriate url, based on the local filesystem

Modules! Why not use import TargetModule using () as a "link"? 😉

[isovector]

I'd love a PDF version of this!