Agda: How to get Agda to ignore `~/.agda`?

[juhp]

I have ~/.agda/ setup for stdlib, but when I "build' a new version of stdlib and do:

agda -i. -isrc Everything.agda

It complains

/home/user/.agda/libraries:1:  Failed to read library file /usr/share/Agda-stdlib/standard-library.agda-lib.
Reason: /usr/share/Agda-stdlib/standard-library.agda-lib: openFile: does not exist (No such file or directory)

However even with --no-libraries or --no-default-libraries I get the same error.
The old workarounds I know are to change HOME or move/delete ~/.agda/.
Does Agda support a way to do this?

(This is not a new issue at all - though today I trying with Agda-2.6.0.1.)

[juhp]

(Okay maybe if I had Agda-stdlib installed, the --no-*libraries options would work?? Even so it is kind of annoying. -- Also the old stdlib would be for an older version of Agda.)

[gallais]

The documentation states that Agda looks into AGDA_DIR so by locally overriding
this environment variable you should be able to point to a directory that does not
matter.

On my machine, I can typecheck an empty module m.agda using this technique by
writing: AGDA_DIR=/tmp/ agda m.agda even if my ~/.agda/libraries file is broken.

That being said, I would call the fact that Agda requires a well-formed ~/.agda/libraries
file even when the --no-libraries option was passed a bug.

Edit: congratulations on bug number 4000! :fireworks:

[juhp]

Thanks
Yeah happy to get #4k :smile: