Naïm Camille Favier
Naïm Camille Favier
> Can the non-default location simply be specified by a command-line option? Would this work for Nix? No: consider building a program that uses Agda as a library. The program...
> Would it work for your purposes if Agda retained its current default, but there was a build flag that allowed you to override the data directory at build time,...
Well, that's the current state before this PR. See [this previous comment](https://github.com/agda/agda/pull/7932#issuecomment-2957122287) for why that's not good enough.
> Why is disabling locking required? The idea is that in "standard" mode there is no need for locking since the data files should be installed once, at build time.
> For the purposes of distribution, Agda does not and cannot know where its data files will be at build time. Yet it has done that for the past two...
Because, just like you want to be able to distribute self-contained Agda binaries, I want to be able to package Agda in a convention-abiding way that doesn't require jumping through...
> What are the conventions? https://cabal.readthedocs.io/en/stable/cabal-package-description-file.html#accessing-data-files-from-package-code https://specifications.freedesktop.org/basedir-spec/latest/ (compare `XDG_DATA_HOME` and `XDG_DATA_DIRS`) > What issues do you run into with the current mechanism? See https://github.com/agda/agda/pull/7818#issuecomment-2927697982, https://github.com/agda/agda/pull/7932#issuecomment-2957122287 (To be clear, it should...
Yes: the generic Haskell builder [tells Cabal](https://github.com/NixOS/nixpkgs/blob/eac1306829168b0240317efb1038bf1cd57eceaf/pkgs/development/haskell-modules/generic-builder.nix#L308-L312) that Agda's data files should live in the Nix store, so Cabal installs them there and `getDataDir` returns their location in the Nix...
I'm happy with `use-system-datadir`. What do the others think?