[Agda] Windows/Linux versions of Agda

[Aaron Stump]

Hi, Jason.


On Mon, Sep 2, 2013 at 3:06 PM, Jason Dagit <dagitj at gmail.com> wrote:

>
>
>
> On Mon, Sep 2, 2013 at 12:36 PM, Aaron Stump <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.

Keeping the Windows installer in synch with Linux (and Mac, which is also
at the most recent version it seems) would really help for using Agda in
teaching, and thus promoting adoption of the tool!

Aaron
-----------------------------------------------------------------
ephesus:~$ cabal install Agda-2.3.0.1
Resolving dependencies...
cabal: Could not resolve dependencies:
rejecting: Agda-2.3.2.1, 2.3.2/installed-781..., 2.3.2 (global constraint
requires ==2.3.0.1)
trying: Agda-2.3.0.1
trying: Agda-2.3.0.1:+use-locale
rejecting: base-3.0.3.2, 3.0.3.1 (global constraint requires installed
instance)
rejecting: base-4.6.0.1/installed-8aa... (conflict: Agda-2.3.0.1:use-locale
=>
base>=4.2 && <4.6)
rejecting: base-4.6.0.1, 4.6.0.0, 4.5.1.0, 4.5.0.0, 4.4.1.0, 4.4.0.0,
4.3.1.0,
4.3.0.0, 4.2.0.2, 4.2.0.1, 4.2.0.0, 4.1.0.0, 4.0.0.0 (global constraint
requires installed instance)

ephesus:~$ ghc-pkg list
/usr/local/lib/ghc-7.6.3/package.conf.d:
Cabal-1.16.0
GLURaw-1.3.0.0
GLUT-2.4.0.0
HTTP-4000.2.8
HUnit-1.2.5.2
OpenGL-2.8.0.0
OpenGLRaw-1.3.0.0
QuickCheck-2.6
array-0.4.0.1
async-2.0.1.4
attoparsec-0.10.4.0
base-4.6.0.1
bin-package-db-0.0.0.0
binary-0.5.1.1
bytestring-0.10.0.2
case-insensitive-1.0.0.1
cgi-3001.1.7.5
containers-0.5.0.0
deepseq-1.3.0.1
directory-1.2.0.1
fgl-5.4.2.4
filepath-1.3.0.1
(ghc-7.6.3)
ghc-prim-0.3.0.0
hashable-1.1.2.5
haskell-platform-2013.2.0.0
haskell-src-1.0.1.5
(haskell2010-1.1.1.0)
(haskell98-2.0.0.2)
hoopl-3.9.0.0
hpc-0.6.0.0
html-1.0.1.2
integer-gmp-0.5.0.0
mtl-2.1.2
network-2.4.1.2
old-locale-1.0.0.5
old-time-1.1.0.1
parallel-3.2.0.3
parsec-3.1.3
pretty-1.1.1.0
primitive-0.5.0.1
process-1.1.0.2
random-1.0.1.1
regex-base-0.93.2
regex-compat-0.95.1
regex-posix-0.95.2
rts-1.0
split-0.2.2
stm-2.4.2
syb-0.4.0
template-haskell-2.8.0.0
text-0.11.3.1
time-1.4.0.1
transformers-0.3.0.0
unix-2.6.0.1
unordered-containers-0.2.3.0
vector-0.10.0.1
xhtml-3000.2.1
zlib-0.5.4.1

ephesus:~$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.6.3



>
> Jason
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130903/a3ac8360/attachment.html