-
Notifications
You must be signed in to change notification settings - Fork 340
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add XDG Base Directory support #6858
Conversation
Test plan: --------- ``` > mkdir ~/.agda > cabal run agda -- --print-agda-app-dir /home/pounce/.agda > rmdir ~/.agda > cabal run agda -- --print-agda-app-dir /home/pounce/.config/agda > AGDA_DIR=/tmp cabal run agda -- --print-agda-app-dir /tmp > cabal run agda -- --print-agda-data-dir /home/pounce/programming/agda/./src/data ``` fixes agda#6852
This commit also changes the documentation for --print-agda-dir, renaming it to --print-agda-data-dir. It also removes inconsistancies in naming between $AGDA_DIR and the agda data directory.
@wenkokke I think the renaming from |
Thanks for the heads up! I don't think it will, because I manually set the data directory through the environment, as the data directory set by cabal isn't reliable. |
With the proposed change, would Agda continue to respond to the |
it should, i didn't touch that at all (only app dir resolution) |
@wenkokke
|
Honestly, it may be easier to add code for resolving finding the Agda app and data directories based on configuration and environment variables, and work on phasing out the use of the Cabal-generated Paths module, given how much trouble it gives us. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Very welcome changes, thank you! For the sake of backwards compatibility, I don't think we should get rid of --print-agda-dir
just yet.
Test plan: --------- ``` > cabal run agda -- --print-agda-data-dir /home/pounce/programming/agda/./src/data > cabal run agda -- --print-agda-dir /home/pounce/programming/agda/./src/data ```
@andreasabel Do you think this needs a test case? If not, I'm merging it. (If so, how?) |
Is this going to make it into the 2.6.4 release? edit: no |
@plt-amy Is now a good time to merge this? |
I think so, yeah! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for this PR.
There seem to be some errors in the docs, partially old errors, partially introduced by this PR.
Also, a CHANGELOG entry is missing so far.
@@ -111,13 +111,26 @@ General options | |||
|
|||
Show just the version number. | |||
|
|||
.. option:: --print-agda-app-dir | |||
|
|||
.. versionadded:: 2.6.4 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This needs bumping to 2.6.4.1
|
||
.. option:: --print-agda-data-dir | ||
|
||
.. versionadded:: 2.6.4 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ditto
:samp:`cat $(agda --print-agda-dir)/html/Agda.css`. | ||
:file:`{${AGDA_DATA_DIR}}/html/Agda.css`. Since version 2.6.2, the | ||
Agda data directory is printed by option | ||
:option:`--print-agda-data-dir`. Thus, you can get hold of the CSS |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not entirely correct.
From 2.6.2, --print-agda-dir
, since 2.6.4.1, --print-agda-data-dir
.
:file:`{${AGDA_DIR}}/latex/agda. Since version 2.6.2, the | ||
Agda data directory is printed by option | ||
:option:`--print-agda-data-dir`. Thus, you can get hold of the class | ||
file via :samp:`cat $(agda --print-agda-data-dir)/latex/agda.sty`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ditto.
:envvar:`AGDA_DIR` is printed by option :option:`--print-agda-dir`. | ||
Thus, you can get hold of the CSS file via | ||
:samp:`cat $(agda --print-agda-dir)/latex/agda.sty`. | ||
:file:`{${AGDA_DIR}}/latex/agda. Since version 2.6.2, the |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This should also be Agda_datadir
, shouldn't it?
.. versionadded:: 2.6.4 | ||
|
||
Outputs the root of the directory structure holding Agda's data | ||
files such as core libraries, style files for the backends, etc. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should this mention the env var Agda_datadir
?
:envvar:`AGDA_DIR` is printed by option :option:`--print-agda-dir`. | ||
Thus, you can get hold of the CSS file via | ||
:samp:`cat $(agda --print-agda-dir)/html/Agda.css`. | ||
:file:`{${AGDA_DATA_DIR}}/html/Agda.css`. Since version 2.6.2, the |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the old docs AGDA_DIR
were wrong. The correct thing (now and then) should be Agda_datadir
.
overridden by setting the ``AGDA_DIR`` environment variable. | ||
overridden by setting the :envvar:``AGDA_DIR`` environment variable. | ||
|
||
The ``AGDA_DIR`` will fall-back to ``~/.agda``, if it exists, for |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Use :envvar:
here?
|
||
The ``AGDA_DIR`` will fall-back to ``~/.agda``, if it exists, for | ||
backward compatibility reasons. You can find the precise location of | ||
``AGDA_DIR`` by running ``agda --print-agda-app-dir``. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ditto.
@plt-amy agreed to write the changelog entry. |
* Add XDG Base Directory support
Test plan:
fixes #6852