[Agda] How to get rid of warning

[Sandro Stucki]

> 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)

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