[Agda] How to get rid of warning

Andreas Abel abela at chalmers.se
Thu Dec 21 05:33:30 CET 2017


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


More information about the Agda mailing list