[Agda] How to get rid of warning

[Martin Escardo]

On 21/12/17 08:58, sandro.stucki at gmail.com wrote:
>> How do I get rid of this warning?
> 
> I had the same problem and eventually "solved" it by putting the
> following in my .emacs file:
> 
>    (makunbound 'agda2-include-dirs)

This black magic does work for me. Thanks.

What is more strange is this, without makunbound.

If I do

~/xxx$ emacs black.agda

I don't get the error. However, if I do

~/yyy$ emacs white.agda

and then ctrl-c ctrl-f ../xxx/black.agda, then I do get the error.

There is nothing in xxx that binds any variable. Also a recursive grep 
in .emacs.d for "agda" finds nothing, and a grep in .emacs finds
'(shell-command-to-string "agda-mode locate")))' only.

I couldn't make the suggestions by other people work because I have 
emacs 25.2.2 which doesn't support them.

As I write, this happens in a machine running ubuntu 17.10,
Agda version 2.6.0-75c88fa

NB. I do have a ~/.agda/ directory, but with empty files "defaults" and 
"libraries". It doesn't help if I get rid of this directory.

For the moment I am adopting the solution by Sandro.

Martin

> 
> Of course that doesn't solve the mystery of why the warning appears in
> the first place (I also don't see where this variable is bound in any
> of my config files either), but if you don't care about that and just
> want the warning gone, it should do the trick.
> 
> Cheers
> /Sandro
> 
> 
> 
> On Thu, Dec 21, 2017 at 5:33 AM, Andreas Abel <abela at chalmers.se> wrote:
>>> Could that be the culprit?
>>
>> Not unless you believe in black magic.
>>
>> The warning is produced by the following code in agda2-mode.el
>>
>> ...
>>   (if (boundp 'agda2-include-dirs)
>>       (display-warning 'agda2 "Note that the variable agda2-include-dirs is
>> no longer used. You may want to update your configuration. You
>> ...
>>
>>
>> On 20.12.2017 18:56, Martín Hötzel Escardó wrote:
>>>
>>>
>>>
>>> On 16/12/17 17:00, abela at chalmers.se wrote:
>>>>
>>>> Mmh, are you sure it is not in any of your emacs configuration files,
>>>> like
>>>>
>>>>     .emacs
>>>>     .emacs.d/init.el
>>>>
>>>> or other configuration files along that line, or any file you include?
>>>
>>>
>>> Absolutely sure. This has just happened again (Agda version
>>> 2.6.0-3b39f0f). The only occurrence of "agda" in .emacs* is in agda-mode
>>> locate. I am now suspecting that this may be because in ~/agda (from github)
>>> I have a directory "std-lib". Could that be the culprit?
>>>
>>> Martin
>>>
>>>
>>>
>>>>
>>>>
>>>> On 16.12.2017 12:06, Martín Hötzel Escardó wrote:
>>>>>
>>>>> How do I get rid of this warning?
>>>>>
>>>>> "
>>>>> Warning (agda2): Note that the variable agda2-include-dirs is
>>>>> no longer used. You may want to update your configuration. You
>>>>> have at least two choices:
>>>>> * Use the library management system.
>>>>> * Set the include path using agda2-program-args.
>>>>>
>>>>> One way to avoid seeing this warning is to make sure that
>>>>> agda2-include-dirs is not bound.
>>>>> Warning (agda2): Note that the variable agda2-include-dirs is
>>>>> no longer used. You may want to update your configuration. You
>>>>> have at least two choices:
>>>>> * Use the library management system.
>>>>> * Set the include path using agda2-program-args.
>>>>>
>>>>> One way to avoid seeing this warning is to make sure that
>>>>> agda2-include-dirs is not bound.
>>>>> "
>>>>>
>>>>> I don't want to use any library, mine or somebody else's.
>>>>>
>>>>> I don't have a .agda directory, deliberately. (In another computer, I
>>>>> have it, with the path files empty, but I still get the above warning.)
>>>>>
>>>>> This variable "agda2-include-dirs" is not in my .emacs. Where is it? How
>>>>> do I "update my configuration" to get rid of this warning?
>>>>>
>>>>> Thanks.
>>>>> _______________________________________________
>>>>> Agda mailing list
>>>>> Agda at lists.chalmers.se
>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>
>>>>
>>>>
>>>
>>
>> --
>> Andreas Abel  <><      Du bist der geliebte Mensch.
>>
>> Department of Computer Science and Engineering
>> Chalmers and Gothenburg University, Sweden
>>
>> andreas.abel at gu.se
>> http://www.cse.chalmers.se/~abela/
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe