--- Day changed Fri Jan 19 2018
byorgeyhi all, today I tried to create a .agda file named (say) Foo.agda, containing 'module Foo where ...' but when I try to load it in emacs with C-c C-l, I get an error "The name of the top level module does not match the file name."19/01 18:17
byorgeyIt then lists a bunch of directories that do not include the current working directory.  I am quite sure I spelled the module name and file name correctly, it seems it is just not looking in the working directory, but only in library locations.19/01 18:18
byorgeyAny ideas?  It's not like this is the first time I've written an Agda program, so I'm not sure what has changed.  I have Agda 2.5.3 installed with version 0.14 of the standard library.  I upgraded a while ago, but it's possible I upgraded but didn't actually try loading an Agda module until now?  I'm not sure.19/01 18:19
pgiarrussobyorgey: on the command line I sometimes end up having to add `-i .`19/01 19:49
pgiarrussobut it might depend on the folder19/01 19:49
pgiarrussois there a `.agda-lib` file in `Foo`’s directory?19/01 19:49
pgiarrussoI had that kind of error when loading README.agda from the stdlib with 2.5.3, because the stdlib has such a file19/01 19:50
pgiarrussobyorgey: ^^19/01 19:50
byorgeypgiarrusso: there is not an .agda-lib file.  But the hint about -i . helped --- I am explicitly setting some command-line args to agda in my emacs config, and adding "-i ." to that list fixed the problem 19/01 19:53
byorgeymaybe -i .  used to be implicit but now it has to be explicit or something?19/01 19:54
pgiarrussobyorgey: possibly? I’ve also been confused like you, so maybe something changed19/01 19:59
pgiarrussoconjecture: `.` is now used as include path *unless* there is *any* source of include paths (.agda-lib or -i)19/01 20:00
pgiarrussoin that case you need it explicitly19/01 20:00
pgiarrussoI don’t know, but this working hypothesis might explain symptoms from you and me19/01 20:00
tomjackSweet, I have just been creating agda-lib files all the time19/01 20:02
byorgeypgiarrusso: oh! I figured it out.  Maybe it has always been required?  It turns out you no longer need to point to the standard library by setting the agda2-include-dirs variable in emacs, so I commented out that line.  But I just noticed that it also had "."19/01 20:08
byorgeyactually, no, I take it back, apparently I do still need the -i .19/01 20:09
byorgeywell, I got it to work now, which is what really matters =)19/01 20:09

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!