Agda installation instructions

README.md

@@ -159,6 +159,7 @@ The deadline is **Friday, February 16, 2018**.
 
 ### Dependently-typed Functional Programming
 
+* [Guidelines](agda/Index.lagda.rst)
 * [Effectful functional programming](slides/pedagand-01.pdf) ([Source](agda/01-effectful/Monad.lagda.rst)).
 * Dependent functional programming.
 * Total functional programming.
@@ -256,6 +257,9 @@ Enable ProofGeneral by adding the following line to your `.emacs` file:
 If desired, ProofGeneral can be further
 [customized](https://proofgeneral.github.io/doc/userman/ProofGeneral_9/).
 
+To install and familiarize yourself with Agda, please follow the
+[instructions](agda/00-agda/Warmup.lagda.rst).
+
 ## Bibliography
 
 [Types and Programming Languages](https://mitpress.mit.edu/books/types-and-programming-languages),

agda/00-agda/Warmup.lagda.rst

+..
+  ::
+  module 00-agda.Warmup where
+
+================================================================
+Warming up
+================================================================
+
+
+Cheatsheets:
+  - `Install Agda`_
+  - `Retrieve the Agda Standard Library <https://github.com/agda/agda-stdlib/archive/v0.14.tar.gz>`_
+  - `Setup the Standard Library`_
+  - Get used to the `Emacs mode`_
+  - RTF `Agda Manual`_ if necessary
+
+************************************************
+Agda in a Nutshell
+************************************************
+
+First, check that the Agda mode is properly configured in your Emacs
+session: if it does, you should see ``(Agda)`` in the status bar of this
+buffer. You can try to manually load it by typing
+
+    ``M-x agda2-mode``
+
+To check that Agda is properly configured, load this buffer by typing
+
+    ``C-c C-l``
+
+If everything works fine, then the following definition should color
+itself properly::
+
+    data World : Set where
+      hello : World
+
+and the status bar of this buffer should become ``(Agda:Checked)``.
+
+We use the Agda Standard Library, which is developed separately from
+the core language and must therefore be installed independantly. The
+previous step may have failed, indicating an error here::
+
+    open import Data.Nat
+    open import Relation.Binary.PropositionalEquality
+
+    foo : 0 ≡ 0
+    foo = refl
+
+If so, then there is something wrong with your setup of the standard
+library. You can look at the buffer ``*agda2*`` to get some info about
+the internal state of the Agda mode, which might help you in
+troubleshooting any issue you encounter during the setup:
+
+    ``C-x b *agda2*``
+
+At this point, everything should be in working order.
+
+************************************************
+Motivating example: evolution of a type-checker
+************************************************
+
+To understand the dynamics and idiosyncrasies of an Agda programmer,
+we suggest that you study the Git history of the mock project
+`Evolution of a Typechecker`_. Use 
+
+    ``git log --graph --all`` 
+
+to begin your exploration with a bird-eye view of the project.
+
+.. References:
+
+.. _`Install Agda`: http://agda.readthedocs.io/en/v2.5.3/getting-started/installation.html
+.. _`Setup the Standard Library`: http://agda.readthedocs.io/en/v2.5.2/tools/package-system.html#example-using-the-standard-library
+.. _`Emacs mode`: http://agda.readthedocs.io/en/latest/tools/emacs-mode.html
+.. _`Agda manual`: https://agda.readthedocs.io/en/v2.5.3/
+.. _`Evolution of a Typechecker`: https://github.com/pedagand/typechecker-evolution
+.. TODO: any other useful resources for setting things up?
+
+.. Local Variables:
+.. mode: agda2
+.. End:

agda/Index.lagda.rst

+================================================================
+MPRI 2.4 : Dependently-typed Functional Programming
+================================================================
+
+
+
+..
+  Make sure that everything compiles::
+
+  open import 00-agda.Warmup
+  open import 01-effectful.Monad
+
+
+This course is organized as follows:
+
+.. toctree::
+   :maxdepth: 1
+
+   00-agda/Warmup
+   01-effectful/Monad
+   02-dependent/Indexed
+   03-total/Recursion
+   04-generic/Desc
+   05-open/Problems
+
+************************************************
+Build
+************************************************
+
+You will need 
+  * Agda (tested with version 2.5.3)
+  * Sphinx (tested with version 1.6.4)
+
+Type:
+
+    ``make html``
+
+which will produce the lecture notes in ``build/html/index.html``.
+
+************************************************
+Contributing
+************************************************
+
+Feel free to submit a PR if you spot any typo, have comments or think
+of any way to improve the material. For instance, if some resource
+available on the web were useful to you during this course, please add
+a link to this resource where you see fit.
+
+I also welcome alternative implementations in other dependently-typed
+(or almost) languages (OCaml or Haskell with GADTs, vanilla Coq,
+Coq/Equations, etc.).
+
+I am also eager to replace references to papers behind paywalls by
+freely accessible (but legal and stable) links. Please keep the `doi`_
+links in comments nonetheless.
+
+************************************************
+Author
+************************************************
+
+The lecture notes have been written by `Pierre-Évariste Dagand`_.
+
+************************************************
+License
+************************************************
+
+These lecture notes are available under an `MIT License`_.
+
+
+.. References:
+
+.. _`doi`: https://www.doi.org/
+.. _`Pierre-Évariste Dagand`: https://pages.lip6.fr/Pierre-Evariste.Dagand/
+.. _`MIT License`: https://tldrlegal.com/license/mit-license
+
+.. Local Variables:
+.. mode: agda2
+.. End: