generics
generics copied to clipboard
Published
1 year ago
•
flupe
flupe
README.agda does not build (with standard library 1.7.1?)
I'm trying to build as part of https://github.com/NixOS/nixpkgs/pull/153757:
Checking README (/build/source/README.agda).
Checking Generics.Prelude (/build/source/src/Generics/Prelude.agda).
Checking Generics.Telescope (/build/source/src/Generics/Telescope.agda).
Checking Generics.Desc (/build/source/src/Generics/Desc.agda).
Checking Generics.HasDesc (/build/source/src/Generics/HasDesc.agda).
Checking Generics.Accessibility (/build/source/src/Generics/Accessibility.agda).
Checking Generics.All (/build/source/src/Generics/All.agda).
Checking Generics.Mu (/build/source/src/Generics/Mu.agda).
Checking Generics.Reflection (/build/source/src/Generics/Reflection.agda).
Checking Generics.Constructions.Show (/build/source/src/Generics/Constructions/Show.agda).
Checking Generics.Helpers (/build/source/src/Generics/Helpers.agda).
Checking Generics.Constructions.Case (/build/source/src/Generics/Constructions/Case.agda).
Checking Generics.Constructions.DecEq (/build/source/src/Generics/Constructions/DecEq.agda).
/build/source/README.agda:40,1-40
Failed to find source of module Generics.Constructions.Induction in
any of the following locations:
/nix/store/zyjqnb0ab30pnzmpcxrph6a468scwb02-standard-library-1.7.1/src/Generics/Constructions/Induction.agda
/nix/store/zyjqnb0ab30pnzmpcxrph6a468scwb02-standard-library-1.7.1/src/Generics/Constructions/Induction.lagda
/build/source/examples/Generics/Constructions/Induction.agda
/build/source/examples/Generics/Constructions/Induction.lagda
/build/source/src/Generics/Constructions/Induction.agda
/build/source/src/Generics/Constructions/Induction.lagda
/build/source/Generics/Constructions/Induction.agda
/build/source/Generics/Constructions/Induction.lagda
/nix/store/mxd6b9c8fgnv3qq34jly0bsq513b111v-Agda-2.6.2.1-data/share/ghc-8.10.7/x86_64-linux-ghc-8.10.7/Agda-2.6.2.1/lib/prim/Generics/Constructions/Induction.agda
/nix/store/mxd6b9c8fgnv3qq34jly0bsq513b111v-Agda-2.6.2.1-data/share/ghc-8.10.7/x86_64-linux-ghc-8.10.7/Agda-2.6.2.1/lib/prim/Generics/Constructions/Induction.lagda
when scope checking the declaration
import Generics.Constructions.Induction
Bisecting gives:
commit d02f9c2ea12c2c824f98e1a0369314a2c3dc99b4
Author: flupe <[email protected]>
Date: Thu Oct 28 02:20:23 2021 +0200
implemented generic fold on mu types