Installation instructions for Agda 2.6.1.1 on Windows 10.
=========================================================

Note: it has been found that the installation will fail if your
Windows username contains a space. If this is the case, create a new
user, make them an admin user, and then follow the below instructions
as that user.

1. Install Emacs. Emacs is a text editor and Agda requires it. 

   * Download the emacs-27-x86_64 installer
     (http://mirror.team-cymru.com/gnu/emacs/windows/).  Once the
     downloading is finished, you can install Emacs by double clicking
     the executable file and following the instruction.

2. Install the Haskell platform and Agda. Agda runs on the Haskell
platform.

  (1) Type "powershell" in the Windows search prompt, and right
      click on the Powershell app and "run as administrator".

  (2) Copy and paste the following command to the Powershell and type return.

     Set-ExecutionPolicy Bypass -Scope Process -Force; [System.Net.ServicePointManager]::SecurityProtocol = [System.Net.ServicePointManager]::SecurityProtocol -bor 3072; iex ((New-Object System.Net.WebClient).DownloadString('https://chocolatey.org/install.ps1'))

     The above command will install the "choco" command. If the
     installation went well, you can type "choco" in the commandline
     and you should see something like "Chocolatey v0.10.15"

    (3) Type "choco install haskell-dev" and hit enter. This will
    install the Haskell platform.  You may be asked for permission to
    run some scripts, just type "A" to say yes to all.  It may take
    several minutes to finish the installation.  Then type
    "refreshenv" and hit enter.

    (4) Now you have installed the Haskell platform. Now close the Powershell. 

    (5) Open the Powershell again (do not run it as administrator this
    time).  You can type "ghc -v" and hit enter. You should see
    something like "Glasgow Haskell Compiler, version 8.10.3"

    (6) Enter "cabal update". 

    (7) Enter "cabal install Agda-2.6.1.1" to install Agda.
    This will take 30 minutes or so. 

3. Configure Emacs and Agda mode.

   (1) In the Powershell, enter the following command (please replace
   'name' with your own username):

   $env:Path += ";C:\Users\name\AppData\Roaming\cabal\bin"

   Then follow with the following command:

   [Environment]::SetEnvironmentVariable("INCLUDE", $env:INCLUDE, [System.EnvironmentVariableTarget]::User)

   (2) Now if you enter "agda" in the Powershell, you should see
   something like "Agda version 2.6.1.1".

   (3) Enter the following command (please replace 'name' with your
   own username).

    echo "" >> C:\Users\name\AppData\Roaming\.emacs

   The above will create an empty file with the name ".emacs" under
   the specified directory.

   (4) Open the above ".emacs" file using the installed Emacs editor.
   Paste the following code to the file, save it and closed Emacs.
   (Use Ctrl-X Ctrl-S to save, and Ctrl-X Ctrl-C to close Emacs).

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

   (5) Create an empty file called "nat.agda" and
   open it in Emacs. Paste the following Agda code to the file.

   data Nat : Set where
     Z : Nat
     S : Nat -> Nat

   Notice that there is no color for the above Agda code after you
   pasted it.  Now type Ctrl-C, followed by Ctrl-L in Emacs. This will
   color the above Agda code. If you see the colored code,
   congratulation, you have managed to set up Agda!  If not, don't
   worry. Come to ask us for help.