[Agda] Windows/Linux versions of Agda

Sam Staton sam.staton at cl.cam.ac.uk
Tue Sep 3 21:12:36 CEST 2013


Something I thought of in the past, as a way of getting people quickly 
using Agda on their own non-linux machines:

We could produce a disk image of a small linux distribution with Agda 
and emacs preinstalled. This could then be easily and quickly run within 
virtualbox (which is free) or alternatively booted from a usb stick or a 
CD.

I think it is quite easy to make a disk image like this.

Sam.

PS. By the way ... iOS? Do people run Agda on iOS?



> I am also entertaining the idea of using Agda in the second part of an
> undergrad functional programming course (in which traditionally we have
> done Haskell only). Our teaching labs have linux, but the students have
> Windows, iOS, and very few linux in their own machines. It would be
> great if installation was as easy for the other operating systems as it
> is for linux. I haven't tried anything different from linux myself
> regarding Agda, and I am not really tempted to, but I would like to be
> confident that my students won't give up. These are second-year
> students, who managed to install the Haskell platform in their own
> machines in the previous years. Will they manage to install (the latest
> version of) Agda? Thanks, Martin
> 
> On 03/09/13 17:47, Aaron Stump wrote:
>> 
>> 
>> 
>> On Tue, Sep 3, 2013 at 11:41 AM, Jason Dagit <dagitj at gmail.com
>> <mailto:dagitj at gmail.com>> wrote:
>> 
>> 
>> 
>> 
>>     On Tue, Sep 3, 2013 at 9:29 AM, Aaron Stump <aaron-stump at uiowa.edu
>>     <mailto:aaron-stump at uiowa.edu>> wrote:
>> 
>>         Hi, Jason.
>> 
>> 
>>         On Mon, Sep 2, 2013 at 3:06 PM, Jason Dagit <dagitj at gmail.com
>>         <mailto:dagitj at gmail.com>> wrote:
>> 
>> 
>> 
>> 
>>             On Mon, Sep 2, 2013 at 12:36 PM, Aaron Stump
>>             <aaron-stump at uiowa.edu <mailto:aaron-stump at uiowa.edu>> 
>> wrote:
>> 
>> 
>>                 This took about a day to do (with my light knowledge 
>> of
>>                 the Haskell platform), because I had to install an old
>>                 version of the Haskell platform
>>                 (haskell-platform-2012.4.0.0), which in turn required 
>> an
>>                 older ghc (7.4.2).
>> 
>> 
>>             Do you remember why you couldn't use the latest Haskell
>>             platform? Perhaps understanding this could turn into a
>>             valuable improvement for the HP.
>> 
>> 
>>         Yes, see the transcript below for what happens when I try to 
>> use
>>         Haskell Platform 2013.2.0.0 with GHC 7.6.3 to install Agda
>>         2.3.0.1 via cabal.  It seems the problem is that the installed
>>         base library (containing the Prelude, it seems) is too recent
>>         for Agda 2.3.0.1, and apparently the Haskell Platform is not
>>         allowing installation of a version of the base library that
>>         satisfies the constraints in Agda.cabal for 2.3.0.1.  As I 
>> said
>>         in my original email, I worked around this by installing an
>>         older Haskell Platform, but this took some effort.
>> 
>> 
>>     Thank you for providing more detailed information.
>> 
>>     I misunderstood before. I thought that there was an issue 
>> installing
>>     the HP 2013.2.0.0. I see now that the problem is with installing 
>> Agda.
>> 
>> 
>> Yes, exactly.
>> 
>> 
>>     For what it's worth, I bet you could `cabal unpack Agda` and edit
>>     the cabal file to relax the constraint on base. If that works you
>>     might be able to build your own windows installer.
>> 
>> 
>> I tried doing some of this, but ended up editing source files, and got
>> stuck at src/full/Agda/Interaction/Imports.hs with ClockTime versus
>> UTCTime.  So I gave up at that point -- not to say something along 
>> those
>> lines couldn't work out.
>> 
>> Aaron
>> 
>> 
>>     Thanks,
>>     Jason
>> 
>> 
>> 
>> 
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>> 
> 
> 
> ------------------------------
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 
> 
> End of Agda Digest, Vol 97, Issue 3
> ***********************************


More information about the Agda mailing list