Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Add flag to print AGDA_DIR and exit #5005

Closed
wenkokke opened this issue Oct 23, 2020 · 5 comments
Closed

Add flag to print AGDA_DIR and exit #5005

wenkokke opened this issue Oct 23, 2020 · 5 comments
Assignees
@andreasabel
Labels
ux: options Issues relating to Agda's command line options ux: packaging Distribution of, and packaging of, Agda itself
Milestone
2.6.2

Comments

@wenkokke
Copy link
Contributor

We should add a flag to Agda which just prints the path to AGDA_DIR and exits.

The location of the AGDA_DIR is somewhat predictable on UNIX systems, but I think such a flag would really help our Windows users. Furthermore, it would really help with the automation of Agda package management, since that way we only implement the logic of figuring out the AGDA_DIR once.

I suggest agda --agda-dir.
@andreasabel
Copy link
Member

I was trying to google if there is a convention for such command line flags, but wasn't very successful.
Alternatives:

  • --print-agda-dir
  • --dump-agda-dir (but this sounds like writing (a large amount of stuff) to disk)

@andreasabel andreasabel added ux: options Issues relating to Agda's command line options ux: packaging Distribution of, and packaging of, Agda itself labels Oct 27, 2020
@andreasabel andreasabel added this to the 2.6.2 milestone Oct 27, 2020
@UlfNorell
Copy link
Member

👍 for --print-agda-dir. --agda-dir suggests to me I should give it an argument to change the agda-dir and --dump-agda-dir does sound more like it would write the contents of the agda-dir somewhere.

@wenkokke
Copy link
Contributor Author

The --print-agda-dir flag sounds good!

@andreasabel andreasabel self-assigned this Nov 6, 2020
@andreasabel
Copy link
Member

Consequently, I will change Agda's help output to say "print version number" instead of "show version number".

andreasabel added a commit that referenced this issue Nov 6, 2020
@andreasabel
[ refactor re #5005 ] simplify Main.hs
793d425 
- superfluous liftIO s
- use Utils.Null
- use mapM on Maybe
- factor out some cut&paste code

Some lines are still overly long.
@andreasabel
Copy link
Member

You can now:

$ ls `agda --print-agda-dir`

@andreasabel andreasabel mentioned this issue Sep 14, 2021
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andreasabel andreasabel

Labels
ux: options Issues relating to Agda's command line options ux: packaging Distribution of, and packaging of, Agda itself
Projects
None yet
Milestone
2.6.2
Development

No branches or pull requests
3 participants
@UlfNorell @andreasabel @wenkokke