[Agda] release schedule, coding suggestions, book

[Aaron Stump]

Ok, thanks for the reply, Andreas.  We will wait to package Windows 
installers for Agda 2.4.2 until you do this, then.  I have some time 
pressure to work with our IT folks on this sufficiently in advance of 
the Spring semester, so it will be great it we can start working on this 
after this month (so early December).

Aaron

On 11/10/2014 04:50 PM, Andreas Abel wrote:
> That is very good news!
>
> Re 1.
>
> A release schedule for Agda does not exist, but I am planning to 
> release bug fixes for Agda-2.4.2 soon, hopefully before the end of 
> this month.
>
> Cheers,
> Andreas
>
> On 05.11.2014 18:56, Aaron Stump wrote:
>> Hello, Agda community.  I am teaching a class on functional programming
>> Spring 2015 using Agda (I did this Spring 2014, too).  I have a couple
>> of questions you can probably help me with:
>>
>> 1. Are there any planned new releases of Agda between now and, say,
>> mid-February?  I want to start the class off with the latest version of
>> Agda, but since we will be bundling Windows MSI files for Agda, I need
>> to plan ahead for what that release might be.  In general, is a planned
>> release schedule posted somewhere on the Wiki?  I did not notice it in a
>> quick inspection.
>>
>> 2. I am planning on turning the class into a lemma-proving factory. I
>> have always dreamed of doing this, and the results were pretty good
>> Spring '14.  Since we only care if lemmas type-check (unless time to
>> type check becomes an issue), student solutions can be incorporated into
>> a library without further scrutiny.  Do you have suggestions or requests
>> for reasonably basic FP algorithms or building blocks we could prove
>> properties of?  I will likely try to get inspiration from the Haskell
>> Prelude, just as an example, but I thought I would ask.  I will be
>> including whatever we develop as part of the "Iowa Agda Library", whose
>> current version is available here:
>>
>> https://svn.divms.uiowa.edu/repos/clc/projects/agda/lib
>>
>> Username and password are both "guest" (without the quotes) if prompted.
>>
>> 3. I am also writing a book called "Verified Functional Programming in
>> Agda".  I have a good bit more to go, but hope to be completing a draft
>> by the end of Spring '15.  I am currently talking with publishers, and
>> could publish with a company called Cognella, which focuses on niche
>> textbooks.  I am curious if others might possibly be interested in using
>> such a book for class.  The more copies I can assure the publisher would
>> be sold, the lower the price I can negotiate.  The current draft --
>> rather spotty currently -- is here
>>
>> https://svn.divms.uiowa.edu/repos/clc/projects/agda/book
>>
>> Again, username and password are guest if you are asked.  The focus is
>> on basic verification methods for pure functional programs, rather than
>> advanced Agda (which I do not know much of anyway).
>>
>> Thanks,
>> Aaron
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>