[Agda] Agda with GHC-6.10.4, continued...

kahl at cas.mcmaster.ca kahl at cas.mcmaster.ca
Fri Apr 9 22:58:03 CEST 2010


On 2010-04-03, Nils Anders Danielsson wrote:
 > On 2010-04-02 12:09, James Chapman wrote:
 > >> Darin introduced a dependency on recent versions of Cabal in his work on
 > >> Cabal support for Agda.
 > >
 > > Is it possible to turn this off temporarily?
 > 
 > You could try the following command:
 > 
 >   darcs obliterate --match='author dwm at cs.nott.ac.uk'

I succeeded to get Agda installed with GHC-6.10.4 after that,
but now pattern matching on pairs does not work anymore
(it is used also in the standard library):


   /export/home/kahl/doc/Lang/Agda/lib/src/Data/List.agda:150,7-19
   Not implemented: Pattern matching for records
   when checking that the pattern just (x , s') has type


The missing patches are:

 $ darcs pull --dry-run
Would pull from "http://code.haskell.org/Agda"...
Would pull the following changes:
Wed Feb  3 11:30:05 EST 2010  dwm at cs.nott.ac.uk
  * initial commit for cabal stuff

Wed Feb  3 12:20:50 EST 2010  Nils Anders Danielsson
<nils.anders.danielsson at gmail.com>
  * Removed a hard-coded version number.

Wed Feb  3 12:27:38 EST 2010  Nils Anders Danielsson
<nils.anders.danielsson at gmail.com>
  * Made the build dependency constraints stricter.

Wed Feb  3 12:28:34 EST 2010  Nils Anders Danielsson
<nils.anders.danielsson at gmail.com>
  * Switched to warning flags which are accepted by cabal check.

Wed Feb  3 12:34:02 EST 2010  Nils Anders Danielsson
<nils.anders.danielsson at gmail.com>
  * Various changes and fixes.

Fri Feb  5 08:27:23 EST 2010  dwm at cs.nott.ac.uk
  * cleanup

Mon Feb  8 08:57:26 EST 2010  dwm at cs.nott.ac.uk
  * Fix package DB reading to work with new DB format (Cabal >= 1.8.0.2 &&
GHC >= 6.12)

Mon Feb  8 09:10:41 EST 2010  dwm at cs.nott.ac.uk
  * Basic error handling

Mon Feb  8 12:43:31 EST 2010  dwm at cs.nott.ac.uk
  * Ported some parts other parts of the package handling code to the new
format.  Incomplete and untested.

Making no changes:  this is a dry run.



It is not obvious where the problem might be hiding,
and quite surprising that it depends on the ``initial commit for cabal
stuff'' --- is there an easy way to get pattern matching for pairs back?



Wolfram



More information about the Agda mailing list