nixpkgs/pkgs/build-support/agda/lib.nix

{ lib }:
{
  /* Returns the Agda interface file to a given Agda file.
  *
  * Examples:
  * interfaceFile "Everything.agda" == "Everything.agdai"
  * interfaceFile "src/Everything.lagda.tex" == "src/Everything.agdai"
  */
  interfaceFile = agdaFile: lib.head (builtins.match ''(.*\.)l?agda(\.(md|org|rst|tex|typ))?'' agdaFile) + "agdai";

  /* Takes an arbitrary derivation and says whether it is an agda library package
  *  that is not marked as broken.
  */
  isUnbrokenAgdaPackage = pkg: pkg.isAgdaDerivation or false && !pkg.meta.broken;
}
agdaPackages.mkDerivation: don't install Everything module The Everthing module is not part of a library and should therefore not be copied to the nix store. This is particularly bad, if the Everything module is defined in an agda library included directory, e.g. consider an agda-lib with include: . and Everything.agda in the project root (.), in which case the Everything module would become part of the library. If multiple such projects are in the dependency tree, the Everything module becomes ambiguous and the build would fail. 2021-01-18 19:01:31 +00:00			`{ lib }:`
			`{`
			`/* Returns the Agda interface file to a given Agda file.`
			`*`
			`* Examples:`
			`* interfaceFile "Everything.agda" == "Everything.agdai"`
			`* interfaceFile "src/Everything.lagda.tex" == "src/Everything.agdai"`
			`*/`
agdaPackages.*: support literate Typst files 2023-10-22 21:51:42 +00:00			`interfaceFile = agdaFile: lib.head (builtins.match ''(.*\.)l?agda(\.(md\|org\|rst\|tex\|typ))?'' agdaFile) + "agdai";`
agdaPackages: Build reverse dependencies on test 2021-01-26 12:01:48 +00:00
			`/* Takes an arbitrary derivation and says whether it is an agda library package`
			`* that is not marked as broken.`
			`*/`
			`isUnbrokenAgdaPackage = pkg: pkg.isAgdaDerivation or false && !pkg.meta.broken;`
agdaPackages.mkDerivation: don't install Everything module The Everthing module is not part of a library and should therefore not be copied to the nix store. This is particularly bad, if the Everything module is defined in an agda library included directory, e.g. consider an agda-lib with include: . and Everything.agda in the project root (.), in which case the Everything module would become part of the library. If multiple such projects are in the dependency tree, the Everything module becomes ambiguous and the build would fail. 2021-01-18 19:01:31 +00:00			`}`