Ulf: Future of Agda
Ulf's job running out at the end of year. Grant app result on November.
Few other ppl know and can work e.g. Nisse, Andreas, Makoto, ...
Thorsten: Maybe a good time to reimplement Agda.
Ulf: Manpower problem
Th: Only Ulf knowing the detail is more expensive in medium term...
JP: The code is not that bad.
Andreas: re-implementation always promising just getting back where we were in 2years Bengt: Not true. We do have a better agda. Don't be too pesimistic. (re Ulf too)
Conor: On a positive note. Agda at a cross road.
Decide to fail, or, try to be successful in the already existing comm with Agda-habit. Compilation!
Th: We should take advantage of having ppl who know Haskell and Agda.
Difficult to get funding for maintaining software. Need to pretend
a blue-sky research
Bengt: It _is_ a blue-sky research, just different from writing papers.
Matter of how to describe.
Andreass: There are a lot of publishable issues re Agda implementation. JP: (Chalmers situation.) Peter's new student., Nisse,. Nisse: Strathclyde activities? Conor: No piece of code lasts more than 6 mo.(in Epigram 2)
Th: This is more like a funeral...
JP: More open process for development, Public review of patches, etc. Bengt: There' danger about it.. JP: The goal is more ppl start reading rather than writing just now.
Nisse: IRC shows some ppl tried and gave up, don't know why
Andreas: For Twelf, Frank Pfenning is writing all the pre/post conditions etc. for each function.
Novice developer needs such security
Th: Last AIM's 'quoteGoal' was done by Ulf showing how to Th, and that was a non-trivial process. Needs those things are documented.
JP: We should be insisting on commenting code, recording Ulf's wisdom.
Conor: I suggest Complete ban on Ulf implementing Agda! New features should be implemented by somebody else; then more ppl start learning the code.
an:XXX
Conor: Recollection of AIM1... Catarina giving several lectures and then a lot of ppl working on the internal... Maybe that style could be revived...
Ulf: Summarising
Th: About indoctrinating Phd students. Ulf saw Agda1, was too complicated, started writing Agda-Light, ...
... More and more ppl worldwide are using Agda... It would be a scandal if Ulf doesn't get a job at Chalmers after this sort of success.
Try to encourage students to become a heroe of Type Theory like Ulf.
Conor: ICFP this year has noticeable Agda presence.
Andreas: Over three hundred issues in tracker.
Ulf: Important thing is to get more ppl involved
JP: Documenting and Commenting. Public patch submission/review.
Nisse: Agda-mailing list can be used.
Conor: Attraction more valuable than revulsion. If it becomes necessary(too much dev traffic/chatting), fork off a new mailing list.
XX, U-Penn, Iowa ppl could study the Agda code before re-implementing.
JP: Can I send the patch to Agda-mailing list? Nisse: Sure.
Conor: The right kind of traffic on Agda list would XXX
Summary:
Th:
- Nisse could be the chief maintainer of Agda (in case Ulf's gone)
- Hope to recruite more ppl get involved and inpart more knowledge about the code published.
- Make the dev process more public. Use Agda-mailing list for this purpose too. If a problem occurs, fork-off.
JP:
- Overview of the code structure on the Wiki 'How to add X' etc.
Th:
- Ulf giving a public lecture on 'How to XXX Agda". Next AIM.
Conor: it has to be combined with a sprint, otherwise ppl just forget.