Getting Agda up and running

TLDR : Agda + VSCode for HoTT summer school.

Note: This is for the HoTT summer school. You can also use this for agda too, but its main purpose is different. Skip to step 5 to just run it.

My system is running Pop-Os 22.04, so I used the Ubuntu installation for everything. I cannot tell what errors might pop up in other OSes. Do take care.

For the two people in the universe who actually use Agda, here is a tutorial on how to get it up and running on VSCode. I know you can use emacs, but for now let’s not use it. (Could add later, leave me alone).

Step 1

Install Agda + agda-mode.

This link should get you started, but if you’d rather not wade through said installation……yeah you have to. Install it. It’s a few lines.

Step 2

Install VSCode. Since that’s what we’re using (presumably).

Step 3

Since this is specifically for the HoTT summer school, go clone the repo given below.

git clone https://github.com/martinescardo/HoTTEST-Summer-School.git

If you dont have git, download the file instead from here.

Note: This file is important to have for one reason. It contains certain libraries. You cannot run the exercises without these.

Step 4

Install the following 2 extensions on VSCode

Extension 1
Name: agda-mode
Id: banacorn.agda-mode
Description: agda-mode on vscode
Version: 0.3.9
Publisher: Ting-Gian LUA
VS Marketplace Link: https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
Extension 2
Name: language-agda
Id: j-mueller.agda
Description: Syntax highlighting and snippets for agda
Version: 0.1.7
Publisher: j-mueller
VS Marketplace Link: https://marketplace.visualstudio.com/items?itemName=j-mueller.agda

Note: Searching the term ‘agda’ in the extensions tab of VSCode should give you these both. Installing is a single button click.

Step 5

You can now use VSCode as you wish. However, here are a few points to keep in mind to actually run the programs. I will give an example below.

  1. (Ctrl-C + Ctrl-L) is your best friend (capital for emphasis. small c and small l will suffice). This actually runs through the file and executes it. It also restarts the agda process (apparently).
  2. {!!} are goals. (Ctrl-C + Ctrl-space) will fill these holes with your variables/outputs/whatever. You will have to type in them and then execute the shortcut. Empty holes become goals.
  3. (Ctrl-Shift-P + Agda:Case) :: This is not a shortcut, but will case split for you based on the variables in the holes (do not C-c C-space them if you wish to case split).

Note: VSCode does not operate like a normal text editor when editing the agda files. (I’ll assume that you’re editing 01-Exercises.lagda.md). There are special commands to use. Hence, it could be easy to screw up said file. Dont worry too much, let it be. (Redownload file if required).

Example

For 01-Exercises.lagda.md, open the file (within the previously downloaded folder) in VSCode. Run the first command (for testing).

All goals
C-c + C-l will give you either this or “All Done” (or something similar)

Case Splitting

To split case, look at the first problem.

_&&'_ : Bool → Bool → Bool
a &&' b = {!0!}

Change it to the below

_&&'_ : Bool → Bool → Bool
a &&' b = {!a b0!}

Now, put your cursor inside the brackets (between the exclamation points).

When you press Ctrl-Shift-P, that’ll open a text field at the top. Search Agda:case within said text field. You’ll find the option to split case.

It’ll come on top.

It will now change into the below.

Screenshot of my code

Note: You don't have to use this. A convenience rather than a necessity.

Solving goals

To solve goals, enter the values within the brackets.

Screenshot of my code

C-c + C-space will finish the goal (as seen below).

Screenshot of my code

Rerun C-c C-l to see results.

Happy solving (and not trying to fling your laptop) !

Note: VSCode can be really really picky about what commands it chooses to recognise. C-c C-space doesn't work for me sometimes and it only works again when I close VSCode and the terminal I launched it from.

As I mentioned before, take care. Worst case, restart system (Not ideal, but I have no solution for now).

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Aditya Sujith Gudimetla

I do stuff. Like stuff about policy. And book stuff. And gaming stuff. And stuff about life. And stuff about stuff.