Commit Graph

12 Commits

Author SHA1 Message Date
Manuel Bärenz
8c0be16075 adga: Add test for all packages 2021-08-03 13:33:59 +02:00
Manuel Bärenz
c84b60b2a9 agda.section.md: Lay out Agda maintenance guidelines 2021-08-03 13:33:59 +02:00
Jan Tojnar
6ecc641d08
doc: prepare for commonmark
We are still using Pandoc’s Markdown parser, which differs from CommonMark spec slightly.

Notably:
- Line breaks in lists behave differently.
- Admonitions do not support the simpler syntax https://github.com/jgm/commonmark-hs/issues/75
- The auto_identifiers uses a different algorithm – I made the previous ones explicit.
- Languages (classes) of code blocks cannot contain whitespace so we have to use “pycon” alias instead of Python “console” as GitHub’s linguist

While at it, I also fixed the following issues:
- ShellSesssion was used
- Removed some pointless docbook tags.
2021-06-07 06:34:59 +02:00
Alexander Ben Nasrallah
4e8641a415 agda: extend agda language frameworks manual section
- add code snippets
- be more detailed on some aspects
2021-04-23 18:31:04 +02:00
Sandro Jäckel
2c143a4614 doc/languages-frameworks/*: add missing languages to code fences
convert shell -> ShellSession
2021-04-05 05:23:19 +02:00
Alexander Ben Nasrallah
b4b4e36921
agda.withPackages: use GHC with ieee754 as default
As mentioned in the package description of ieee on Hackage,
ieee is deprecated in favor of ieee754.
2021-01-22 16:13:46 +01:00
Ryan Mulligan
b8344f9e5c doc: explicit Markdown anchors for top-level headings; remove metadata
I used the existing anchors generated by Docbook, so the anchor part
should be a no-op. This could be useful depending on the
infrastructure we choose to use, and it is better to be explicit than
rely on Docbook's id generating algorithms.

I got rid of the metadata segments of the Markdown files, because they
are outdated, inaccurate, and could make people less willing to change
them without speaking with the author.
2021-01-01 10:02:57 -08:00
Manuel Bärenz
87cab901a3 agda.section.md: Fix header, enumerations, capitalisation 2020-09-18 12:42:06 +02:00
Cole Helbling
5baa7541d7
agda: fix manual build
/build/doc/manual-full.xml:12764:35: error: ID "build-phase" has already been defined
    /build/doc/manual-full.xml:9029:33: error: first occurrence of ID "build-phase"
2020-06-17 13:51:43 -07:00
Alex Rice
e215c3bcac
agda: install literate files 2020-06-01 13:59:20 +01:00
Uma Zalakain
196cc47005 agda: fix typo in library management documentation
Agda expects a "depend" (not "depends") field in the library description.
2020-05-24 14:20:05 +02:00
Alex Rice
d30e2468e0
agda: rework builder 2020-05-14 20:54:11 +01:00