Literate Agda in Org mode documents

Instructions.org

Literate Agda in Org mode documents

Note: These instructions will be unnecessary after Agda 2.6.0 is released.

PR agda/adga#3548.

1. Clone the Agda repository.

   git clone https://github.com/agda/agda.git
   cd agda
       

2. Fetch and checkout the patch.

   git fetch origin pull/3548/head:fork
   git checkout fork
       

3. Build Agda in a new sandbox (to avoid conflicts with your existing Agda installation).

   cabal sandbox init
   make
       

4. Get the path to the new agda compiler executable. You should get something like dist/dist-sandbox-d54e9136/build/Agda/agda.

   find dist -type f -name agda
       

5. Get the path to the new agda-mode executable. You should get something like dist/dist-sandbox-d54e9136/build/agda-mode/agda-mode.

   find dist -type f -name agda-mode
       

6. Get the result of agda-mode locate. You should get something like /Users/emily/src/agda/.cabal-sandbox/share/x86_64-osx-ghc-8.4.3/Agda-2.6.0/emacs-mode/agda2.el

   /path/to/dist/dist-sandbox-d54e9136/build/agda-mode/agda-mode locate
       

7. Modify your Emacs configuration. When installing Agda you probably ran agda-mode setup and this placed the following lines your configuration.

   (load-file (let ((coding-system-for-read 'utf-8))
   	     (shell-command-to-string "agda-mode locate")))
       

   Replace that expression with the following

   (load-file "/Users/emily/src/agda/.cabal-sandbox/share/x86_64-osx-ghc-8.4.3/Agda-2.6.0/emacs-mode/agda2.el")
       

   Be sure to use the result you got from step 6.

8. Set some environment variables in your shell. Use the results you got from step 4 for this. Note that the PATH does not include the final /agda (it should be the directory containing the agda executable).

   export AGDA_BIN=/Users/emily/src/agda/dist/dist-sandbox-d54e9136/build/Agda/agda
   export PATH=/Users/emily/src/agda/dist/dist-sandbox-d54e9136/build/Agda $PATH
       

9. Voila! Run Emacs on a .lagda.org file.

   emacs Test.lagda.org
       

Use #+begin_src agda2 source blocks.