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-modeExtension 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.
- (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).
- {!!} 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.
- (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).
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 will now change into the below.
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.
C-c + C-space will finish the goal (as seen below).
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).
