Skip to content

Idris Developers Meeting, Nov 2013

Jump to bottom Edit New page
Ahmad Salim Al-Sibahi edited this page Nov 23, 2013 · 57 revisions

There will be an Idris Developers Meeting in St Andrews, Scotland, from Monday 18th-Friday 22nd November 2013. 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

It will be hosted by the School of Computer Science at the University of St Andrews. (map)

  • We will be in room 1.04 in the Jack Cole Building all week, except:
    • 10-11 Monday 18th, Jack Cole 1.33b
    • 11-12 Monday 18th, John Honey Building, Goldfish Bowl
    • 11-1pm Wednesday 20th, Jack Cole 0.29
    • 11-12 Friday 22nd, Jack Cole 1.33a
    • 12-1pm Friday 22nd, Jack Cole 1.33b
  • We will begin at 9:30am on Monday, meeting in the coffee area in the Jack Cole Building
  • For those arriving on Sunday evening, we will meet at 8pm in Aikman's on Bell Street (map)

Content

Watch this space for updates as the week progresses. There will be:

  • Talks (Please add to this list)
    • An overview of Idris internals (Edwin Brady)
    • Idris type providers (David Christiansen)
    • Ideslave mode (structured input and output to idris, to be used by development environments) hannes
    • Abstraction classes (why they should be included, somewhat short presentation) - Ahmad Salim Al-Sibahi
    • Computational Mathematics and Idris/Dependent Types - Markus Pfeiffer
    • Idris and, Modern and Modern Modern Encryption - Jan de Muijnck-Hughes
    • ...
  • Discussion (Please add to this list)
    • Library design (class hierarchy, effects, ...)
      • In particular, what should be in the Prelude? A dependent Prelude?
    • Module system
    • Copatterns
    • Error reflection (might turn into talk by David Christiansen)
    • Interactive editing
    • Projects for GSoC, grants, funding, papers, ...
    • Generic programming, 'deriving'
    • What is required for version 1.0?
    • Abstraction classes
    • Computational Mathematics and Idris/Dependent Types
    • Crypto Bindings
    • ...
  • Focussed hacking sessions (Please add to this list)
    • Type classes as dependent records
    • Optimisation: better inlining, partial evaluation
    • Library optimisations: string processing is particularly bad
    • Bug squashing (from the issue tracker)
    • Improving laziness in executor (the thing that does :x)
    • Improving proof search
    • Making binary packages for various OSes
    • Std Library and Prelude Documentation
    • Tutorial Updates and Improvements
    • ...

Registration

Space will be fairly limited, so if you plan to attend, please send an email to Edwin Brady 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.

Attendees

  • Edwin Brady
  • Markus Pfeiffer
  • Simon Fowler
  • Franziska Schmidt
  • David Christiansen
  • Hannes Mehnert
  • Ahmad Salim Al-Sibahi
  • Jan de Muijnck-Hughes
  • Matúš Tejiščák

Practicalities

There is a hostel

Progress Log

18. November 2013

Markus

  • Added floating point primitives, and finally managed to open a proper pull request, #627
  • While being around tests, I patched test scripts to use #!/usr/bin/env.

Matúš

  • Figuring out collapsibility and forceable arguments of data constructors
  • Constructor disjointness check fully recursive now

Edwin

  • Talked about internals
  • Started work on reimplementing partial evaluation
  • Answered lots of questions :)

Jan

  • Started work on a logo.
  • Started working on tutorials, one result is Idris Koans.

David

  • Closed #607
  • Worked with Hannes on proper support for interactive editing in ideslave and the Emacs mode

Ahmad

  • Finishing eliminators (started to work)

Hannes

  • Worked with David on interactive editing and ideslave
  • started cleanups to support building on FreeBSD out of the box

19. November 2013

Markus

Matúš

  • extending forceability to recursive applications of a datatype

Hannes

  • polished patches for FreeBSD support

Jan

  • Worked more on Idris-Koans and improved tutorials using meta variables

Ahmad

  • Further development on eliminator generation
  • Cleaned up parsers, and rewrote package parser and ide-slave sexpr parsers to Trifecta
  • Removed C warnings (with help from Hannes)
  • Made proofs only work on meta variables

20. November 2013

Jan

  • Gave talk: Idris, Modern and Modern Modern Cryptography

Matúš

  • forceability check rewritten from the ground up (runtime reconstructing projections pending)

Markus

  • worked on libusb bindings, successfully opened usb devices

Ahmad

  • Finished up eliminators such that they work for most inductive types now (a bit of work is needed to merge with the upstream version)

21. November 2013

Jan

Edwin

  • Improved type class implementation using dependent records
  • Reorganisation of the libraries, separating the prelude from the base libraries

Matúš

  • Collapsibility check rewritten

Hannes

  • Implement logging for ideslave

22. November 2013

Edwin

  • Fixed space leak in elaborator and REPL
  • Closed some long-standing issues regarding matching on functions
  • Finished initial library reorganisation

Hannes

  • Wrote up documentation for ideslave and idris-mode here
  • Minor bug fixes for idris-mode
  • Error reporting in ideslave

Matúš

  • collapsibility and forceability seem to be recognised correctly, at last, including recursive disjointness and forceability of recursive occurrences
  • (runtime reconstruction functions still pending)
Add a custom footer

Home

Unofficial FAQ

External Resources

Installation Instructions

Binary Packages

Tool Support

Community

Development

Clone this wiki locally