Idris Developers Meeting, April May 2014

There will be an Idris Developers Meeting at Chalmers in Gothenburg, Sweden from Tuesday 29th April - Friday 2nd May 2014. The meeting is open to anyone who is interested in contributing to Idris, implementing libraries or applications in Idris, or just interested in watching progress.

Location

The meeting will take place in the D&IT building at Rännvägen 6 on the Jonhanneberg campus. Watch this space for specific details about room bookings.

Content

Tuesday, 29 April

We will begin at 9:30 in the lunchroom in the D&IT building (all the way up on the top floor) for a half-hour coffee meetup and check-in. Someone will be down in the building lobby to collect new arrivals at 9:30 and at 10:00.

9:30-10:00	Hello and coffee break		D&IT lunchroom
10:00-12:00	Intro to dependent types and Idris for functional programmers	David Christiansen	8103
12:00-13:30	Lunch on our own
13:30-14:00	Idris in the browser	raichoo	8103
14:00-15:30	Intro to Idris for Agda users	Andrea Vezzosi and David Christiansen	8103

Room 8103 is directly attached to the lunchroom. Assume unplanned time (15:30 onwards) is for working together on projects and perhaps going out for some food.

Progress:

@david-christiansen fixed bugs in idris-mode and the compiler that made interactive editing of .lidr files more painful than necessary, and made idris-mode use .ipkg files to get the working directory
https://github.com/idris-hackers/idris-mode/pull/120
https://github.com/idris-lang/Idris-dev/pull/1125
https://github.com/idris-hackers/idris-mode/pull/119
@paulkoerbitz did his first changes to the main idris code base (#1155, #1159, #1164, #1165) which hopefully fixed #1047, #1154 and #1158 (which was introduced by #1155).

Wednesday, 30 April

Talks: 10:00 - 12:00 in 8103
- Idris and formalization: a practitioner's account - Nicola Botta
- Idris, Cryptography, and Provable Cryptography - Jan de Muijnck-Hughes
Day: We have room 8103 from 8:00-13:00, and rooms 4128 and 6128 for the whole day. 4128 and 6128 can only hold about half of us, so we'll have to be on IRC.
Evening: Walpurgis Night celebration in Gothenburg - go out and join the festivities Swedish description

Thursday, 1 May

Note that 1 May is a holiday in Sweden. We have access to the building, but doors will be locked, so someone with a Chalmers key will have to let you in. We will arrange the practicalities of this once everyone has arrived.

Activities:

Additional talks and demos:
- Edwin presented protocols and neweffects
- David presented error reflection (Demo code)
- Ahmad presented ongoing work on fast levitation

Rooms:

We will be in 8103 - the ones who booked it don't need it.
EDIT-room (3364) is booked 8-12
Group rooms 4128 and 6128 are booked all day

Friday, 2 May

We have room 8103 all day Friday.

Registration

Space will be fairly limited, so if you plan to attend, please send an email to David Christiansen stating:

Which days you will be attending
Whether you'd like to give a talk (please also add this to the list above)

Optionally, you can also add your name to the list below.

There is no fee for participation, but you will be responsible for your own food and lodging.

Attendees

David Christiansen
Andrea Vezzosi (Saizan)
Víctor López Juan
Baldur Blöndal
Jean-Louis Giordano
Tim Dysinger (hopeful)
Edwin Brady (not Tuesday)
Jan de Muijnck-Hughes (Not Tuesday, Friday Morning maybe...)
Cezar Ionescu
raichoo (Hopefully this time!)
Andreas Reuleaux
Daniel Öberg (Tuesday and Wednesday)
Ahmad Salim Al-Sibahi (Wednesday-Thursday)
Paul Koerbitz
Evgeny Kotelnikov
Carlo Hamalainen (Tuesday to Thursday)
Patrik Jansson (Wednesday-Friday)
Nicola Botta
Andreas Abel
Thomas Didriksen (Wednesday, Thursday)
Sune Alkærsig (Wednesday, Thursday)
Niklas Larsson
Mort Yao
Francesco Mazzoli (Thursday evening, Friday)

Community Discussions

What is 1.0? (revisit from last meeting)
How can we get better documentation?
How can we de-bottleneck Edwin?
Release cadence for Idris and important related tooling and documentation.

Aims and Objectives

High level goals for the Hackathon.

New community led document that presents Idris in styles similar to that of both the Hutton and LYAH books.

Practicalities

If you don't have access to Eduroam, then we will need to create a guest account for you here at Chalmers so that you can access the wireless Internet. Please write to David if you need this.

Inexpensive places to stay that are close to Chalmers include: