Discussion:
[Agda] How to get rid of warning
Martín Hötzel Escardó
2017-12-16 11:06:03 UTC
Permalink
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.
Andreas Abel
2017-12-16 17:00:33 UTC
Permalink
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?
Post by Martín Hötzel Escardó
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
* 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
* 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
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

***@gu.se
http://www.cse.chalmers.se/~abela/
Martín Hötzel Escardó
2017-12-20 17:56:18 UTC
Permalink
Post by Andreas Abel
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
Post by Andreas Abel
Post by Martín Hötzel Escardó
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
* 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
* 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
https://lists.chalmers.se/mailman/listinfo/agda
--
http://www.cs.bham.ac.uk/~mhe
Andreas Abel
2017-12-21 04:33:30 UTC
Permalink
Post by Martín Hötzel Escardó
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
...
Post by Martín Hötzel Escardó
Post by Andreas Abel
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
Post by Andreas Abel
Post by Martín Hötzel Escardó
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
* 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
* 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
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

***@gu.se
http://www.cse.chalmers.se/~abela/
Sandro Stucki
2017-12-21 08:58:19 UTC
Permalink
Post by Martín Hötzel Escardó
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
Post by Martín Hötzel Escardó
Post by Martín Hötzel Escardó
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
...
Post by Martín Hötzel Escardó
Post by Andreas Abel
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
Post by Andreas Abel
Post by Martín Hötzel Escardó
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
* 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
* 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
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
http://www.cse.chalmers.se/~abela/
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Martin Escardo
2017-12-21 10:00:44 UTC
Permalink
Post by Sandro Stucki
Post by Martín Hötzel Escardó
How do I get rid of this warning?
I had the same problem and eventually "solved" it by putting the
(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
Post by Sandro Stucki
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
Post by Martín Hötzel Escardó
Post by Martín Hötzel Escardó
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
...
Post by Martín Hötzel Escardó
Post by Andreas Abel
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
Post by Andreas Abel
Post by Martín Hötzel Escardó
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
* 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
* 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
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
http://www.cse.chalmers.se/~abela/
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
Nils Anders Danielsson
2017-12-20 21:29:42 UTC
Permalink
Post by Martín Hötzel Escardó
This variable "agda2-include-dirs" is not in my .emacs. Where is it?
The following command might give you some useful information:

(find-lisp-object-file-name 'agda2-include-dirs 'defvar)
--
/NAD
Nils Anders Danielsson
2017-12-21 08:45:33 UTC
Permalink
Post by Nils Anders Danielsson
(find-lisp-object-file-name 'agda2-include-dirs 'defvar)
The methods described in the answers to the following Emacs Stack
Exchange question are perhaps more likely to work:

https://emacs.stackexchange.com/questions/27962/tracking-down-a-write-to-a-variable
--
/NAD
Loading...