Would it be better to manually list the different extensions for literate agda files (.lagda.org, .lagda.md, and .lagda.rst) rather than using .lagda.*?

Would it be better to manually list the different extensions for literate agda files (.lagda.org, .lagda.md, and .lagda.rst) rather than using .lagda.*?

How about having an option for a list of extension to search for, and append that to a conservative whitelist? As example value, you can then give .lagda.*.

Would it be better to manually list the different extensions for literate agda files (.lagda.org, .lagda.md, and .lagda.rst) rather than using .lagda.*?

How about having an option for a list of extension to search for, and append that to a conservative whitelist? As example value, you can then give .lagda.*.

There are already quite a few options and I think the list I have put in now should cover everything for now

It would be very easy to add, I am more worried about making the documentation not confusing

It would be very easy to add, I am more worried about making the documentation not confusing

I suppose a line could be put in saying these can be overriden by an extensions attribute. lmk if you think this would be useful. It's still possible to use a custom installPhase in edge cases

There are already quite a few options and I think the list I have put in now should cover everything for now

It's just a hunch that it might be useful to leave this configurable. Sometimes a new markdown format pops up, and people start using it before these settings are adjusted. For example in Haskell it's annoying that literate programming in *.md is so poorly supported.

I have added the extraExtensions tag

Thanks for the catches

This pull request has been mentioned on NixOS Discourse. There might be relevant details there:

https://discourse.nixos.org/t/prs-already-reviewed/2617/169

not sure if this is a regression:

builder for '/nix/store/g959q8d44jds9vz6jmxvknvqasbspmb5-agda-prelude-compat-2.6.0.drv' failed with exit code 1; last 10 log lines:
    /build/source/src/Builtin/Reflection.agda:113,21-24
    /build/source/src/Builtin/Reflection.agda:118,16-23
    /build/source/src/Builtin/Reflection.agda:124,17-20
    /build/source/src/Builtin/Reflection.agda:128,16-23
    /build/source/src/Builtin/Reflection.agda:224,44-45
    /build/source/src/Builtin/Reflection.agda:227,44-45
    /build/source/src/Builtin/Reflection.agda:236,44-45
    /build/source/src/Builtin/Reflection.agda:239,44-45
  when scope checking the declaration
    open import Builtin.Reflection
builder for '/nix/store/61z839518w39acsyplahb0ikm3qjhsvy-iowa-stdlib-1.5.0.drv' failed with exit code 2; last 10 log lines:
  agda  -v 0 negation.agda
  agda  -v 0 neq.agda
  agda  -v 0 nat-thms.agda
  agda  -v 0 braun-tree.agda
  /build/source/braun-tree.agda:34,1-50,75
  Termination checking failed for the following functions:
    bt-replace-min
  Problematic calls:
    bt-replace-min A _<A_ a
    (bt-node a' (bt-node x l r u) bt-empty (injmake: *** [Makefile:35: braun-tree.agdai] Error 1
cannot build derivation '/nix/store/7kikqifn9n2x7a699irg9mzjcw07c5f3-env.drv': 2 dependencies couldn't be built
[4 built (2 failed), 166 copied (4111.6 MiB), 321.3 MiB DL]
error: build of '/nix/store/7kikqifn9n2x7a699irg9mzjcw07c5f3-env.drv' failed
https://github.com/NixOS/nixpkgs/pull/89245
2 packages failed to build:
agdaPackages.agda-prelude agdaPackages.iowa-stdlib

2 packages built:
agdaPackages.cubical agdaPackages.standard-library

@Lassulus those two packages were already broken as they have not been updated to work with (/ do not have a release for) Agda-2.6.1

Just for the record, this broke the nixpkgs manual, fix is in #90689.