Idris Developers Meeting, March 2015

There will be an Idris Developers Meeting in St Andrews, Scotland, from Monday 16th-Friday 20th March 2015. 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 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 (Most likely on Wednesday; please add to this list)
  • Idris quasiquotation (David Christiansen)
  • Guarded recursion in Idris (Sune Alkærsig and Thomas Didriksen)
  • A new tactic system (David Christiansen)
  • A library for command-line flags / options (Guillaume Allais)
  • Uniqueness types and communication protocols (Edwin Brady)
  • Progress on refactoring and dependent types (Andreas Reulaeux)
  • ...
• Discussion (Please add to this list)
  • Future funding sources
  • Website
    • Does the content of the website need updating/adjusting?
    • Is there content from the GitHub Wiki pages that should be on the Website, and vice-versa?
    • Does anyone want to volunteer to help maintain the website?
  • Documentation
    • Generation of new (and updated of) tutorial materials.
      • 10 minute and 30 minute guides...
      • Add beginner, intermediate, and advanced parts to the idris tutorial.
    • Generation of a language specification to describe:
      • Language constructs and their use.
      • Underlying implementation details such as elaborater operation, and FFI.
      • Design rationale and guidance.
    • Format and dissemination of documentation.
      • Keep on using the Wiki and LaTeX?
      • Standalone HTML idris-lang.org, or idris-dev.github.io?
      • Utilise read-the-docs, this requires the use of Sphinx.
      • Licensing of new (and old) documentation
    • API documentation.
      • Should the 'idrisdoc' for the libraries in libs be placed in a more accessible place?
      • Should documentation for libraries be generated in a single accessible place rather than a project's root?
  • Libraries
    • Does libs need sorting/pruning/adding?
  • The 'Idris Package Manager'.
  • Externally hosted Idris Backends.
    • Can we find maintainers?
  • Branding: We now have a logo and a re branded website.
    • Should we consider the creation on a lambda/pi Idris mark, for use alongside the logo? or is the 'dragon ear' the mark as well as the logo?
    • Should similar considerations be given to an Idris mascot, and also a colour scheme?
    • Should we outsource the above if required?
    • Should we consider authorised merch for Idris?
  • ...
• Focussed hacking sessions (Please add to this list)
  • Refactoring of Idris Internals
  • Tidying of IdrisMain
  • Things in the Issue Tracker marked as:
    • Feature Request
      • Deprecation Annotation
      • Packages and Options
      • Documentation Coverage
      • Literate Programming Support
    • Low Hanging Fruit
      • Package Import Case Sensitivity
  • Evaluate different components that were contributed by people as to whether they still work, should still be included, or removed and proposed as a future feature/project.
  • Improvements to Travis/CI: getting the issue found by #1907 fixed so we can merge it, consider adding Coverity scanning of the RTS, and Appveyor Windows testing if a Windows user shows up
  • Packaging: automated binary package and HTML doc builds from each commit would be wonderful
  • Reflection/Ring Solver: Finish FranckS's ring solver by adding reflection

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
• David Christiansen
• Andreas Reuleaux
• Thomas Didriksen (Monday-Thursday)
• Sune Alkærsig (Monday-Thursday)

Practicalities

There is a hostel

Progress Log

(Please fill this in as the meeting progresses!)