News forum

Welcome to the course and week 1 action items

Welcome to the course and week 1 action items

by Danel Ahman -
Number of replies: 0

Dear all,

Welcome to the Logika v računalništvu / Izbrana poglavja iz računalniške matematike course at UL FMF, both from me and Andrej!

Below is some basic information about the course and some action items to do before your first exercise class.

Check out the course website on Spletna učilnica (https://ucilnica.fmf.uni-lj.si/course/view.php?id=252).

This is where we gather links to all the course materials, such as lecture notes, exercises, instructions for installing the required software, etc.

The course website also includes an invitation link to the course Discord server. Please sign up if you haven't done so yet. Discord will be a good place to ask for help with various administrative and technological problems (e.g., installing and setting up Agda, interacting with Git, etc).

ACTION ITEMS (for you to do before the week 1 exercise classes)

1. Choosing which exercise class time slot you will attend.

On Spletna učilnica, there is a poll for you to indicate which of the two exercise class time slots you will be attending. Please fill this in if you haven't done so.

While the computer class has room for only 15 people, then still select your time slot even if >= 15 selections have been made. This overflow information will help give us an idea how to proceed in the coming weeks.

2. Forking and cloning the course GitHub repository (https://github.com/danelahman/lograc-2022).

Please fork and clone the course GitHub repository (see the instructions in the README.md file in the repository for help; or ask for help on Discord).

We will be using this repository to publish exercise sheets, sample solutions, and other course-related code.

3. Installing Agda

In this course we will be predominantly using the programming language and proof assistant Agda (https://wiki.portal.chalmers.se/agda/pmwiki.php). For instructions on how to install and set up Agda on your own computer, please again see the README.md file in the course GitHub repository (https://github.com/danelahman/lograc-2022).

While it will be possible to solve the exercises on the classroom computers, we recommend that, if possible, you bring and use your own laptop! While pre-installed on the classroom computers, Agda is not interacting well with the network-mounted user directories on the classroom computers. Further, installing and setting up the required software on your own computer will also simplify working on your chosen project in the second part of the course outside of the prescribed exercise class hours.

4. Setting up the interactive development environment for Agda

In order to get the most out of Agda, you should be using it through an interactive development environment. We suggest you use either:

  • Visual Studio Code with its agda-mode extension, or
  • Emacs with its agda-mode plugin.

Links and instructions on how to set either of these environments up can again be found in the README.md file in the course GitHub repository (https://github.com/danelahman/lograc-2022).

If you have any questions or get stuck with anything in these action items, feel free to ask for help (either by email or on the course Discord server; that latter is preferred, because other students might run into similar problems).

With best wishes,

Danel Ahman