[Agda] Agda and GHC 7.8

Andreas Abel andreas.abel at ifi.lmu.de
Thu Sep 25 17:23:51 CEST 2014


On 25.09.2014 15:46, Jan Stolarek wrote:
>> Can you manually
>>
>>     src/full/Agda/Syntax/Parser$ alex Lexer.x
>>
>> ?
> I get no errors + Lexer.hs gets generated. But then trying `cabal install` or `make install-bin`
> (in hope that lexer generation will be skipped) still fails.

Ah no, as cabal builds into a different directory, dist/build/..., it 
would not take the Lexer.hs file from there, I guess.

Could it be that you have different version of alex somewhere which is 
mysteriously invoked by cabal?  There is something weird about the error

src/full/Agda/Syntax/Parser/Lexer.x:0:2:
     lexical error at character '\n'

If I introduce an error (like a ^G) in the first character of Lexer.x, 
alex-3.1.3 reports

Lexer.x:1:1: lexical error at '\a'

So, alex does not seem to know a line number 0, (at least not in the 
newer versions).

On 25.09.2014  Jan Stolarek wrote:

Building Agda-2.4.3...
Preprocessing library Agda-2.4.3...
Warning: trailing characters after #if directive in
file /dane/sandboxes/ghc/7.8.3//lib/ghc-7.8.3/include/ghcautoconf.h  at 
line 383 col 1:
AC_APPLE_UNIVERSAL_BUILD

src/full/Agda/Syntax/Parser/Lexer.x:0:2:
     lexical error at character '\n'
cabal: Error: some packages failed to install:
Agda-2.4.3 failed during the building phase. The exception was:
ExitFailure 1

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/


More information about the Agda mailing list