Software Foundations in Idris

📖 Download the PDF

Building

To rebuild the PDF, ensure the prerequisites are installed, then:

make pdf

Prerequisites

Others may work, but here are the versions I'm using.

Installing prerequisites

• macOS

Contributing

TBD (see issue #4 for discussion)

General Workflow

1. Fork the repository if you haven't already.
2. Check the open pull requests for any related work in progress (WIP).
3. Check out a new branch based on develop.
4. Push some commits to your fork.
   • The general workflow here is as follows:
     • Copy/paste the original text, reformatting as appropriate.
     • Translate Coq code into (idiomatic) Idris.
     • Edit, augment and delete text as appropriate. N.B. This can be done in subsequent pull requests.
5. Open a pull request (as soon as possible).
   • If it's not ready to be merged, but you want to claim a particular task, prefix the pull request with WIP:.
   • Make a comment and remove the WIP: when it's ready to be reviewed and merged. Remember: formatting the text and taking a first pass at translating the Coq to Idris is enough for an initial pull request.
6. Open subsequent pull requests following a similar pattern for and edits or other updates

The develop branch is the working branch and master is for releases, i.e. rebuilt PDFs and website updates.

Formatting

When formatting the Literate Idris source, we use bird tracks for code meant to be compiled and a combination of Markdown and LaTeX for commentary and illustrative examples that aren't meant to be compiled.

= Example

This is some commentary with **bold** and _italicized_ text.

```idris
-- This is an Idris code block which won't be read when compiling the file.
foo : Nat
foo = 42
```


== Code to Compile

The following, however, will be compiled:

> module Example
>
> %access public export
>
> foo : String
> foo = "bar"


== Other Notes

- We can also highlight code inline, e.g. \idr{primes : Inf (List Nat)}.
- To refer to glossary entries, use e.g. \mintinline[]{latex}{\gls{term}}.

Chapters, Sections, et al.

To denote chapters, sections, and other subdivisions, use = as follows:

= Chapter
== Section
=== Subsection
==== Subsubsection

Bold and Italicized Text

We use the succinct Markdown syntax...

... to format **bold** and _italicized_ text.

Lists

We prefer the Markdown syntax here too, e.g.

- foo
- bar
- baz

Code Blocks

Just as with bold and italicized text, we favor the more succinct Markdown syntax for (fenced) code blocks:

```idris
addTwo : Nat -> Nat
addTwo x = x + 2
```

For more information, refer to the relevant GitHub Help document.

Inline Code

For inline Idris code, use the custom \mintinline shortcut \idr, e.g.

To print ``Hello World!'' in Idris, write \idr{putStrLn "Hello, World!"}.

For convenience, we've also defined the shortcut \el for inline Emacs Lisp code, e.g.

Set the value of \el{foo} to \el{42}: \el{(setq foo 42)}.

Otherwise, use single backticks for inline monospace text, e.g.

This is some `inline monospaced text`.

In a certain cases, we might want syntax highlighting for a language other than Idris or Emacs Lisp. For such cases, use the standard \mintinline command, e.g.

To declare a theorem in Coq, use \mintinline[]{coq}{Theorem}.

Glossary

We use the glossaries package for defining terms (in src/glossary.tex) and including a glossary in the generated PDF. See the package documentation for more information, but here's a quick example:

What is the \gls{meaning of life}?


\newglossaryentry{meaning of life}{
  description={42}
}

Generating the PDF

To generate the PDF we use Pandoc and latexmk. For more details, check out the all.pdf, all.tex and %.tex rules in src/Makefile.