Use reflection to generate injectivity proof for builtins#7746
Draft
ana-pantilie wants to merge 2 commits into
Draft
Use reflection to generate injectivity proof for builtins#7746ana-pantilie wants to merge 2 commits into
ana-pantilie wants to merge 2 commits into
IOG Hydra / ci/hydra-build:x86_64-darwin.ghc96:checks:plutus-executables:test:test-certifier
failed
Apr 29, 2026 in 0s
Build dependency failed
1 failed steps
Details
Failed Steps
Step 1
Derivation
/nix/store/73q9apq73c3743yli6g413jb933kgd1s-plutus-metatheory.drv
Log
Running phase: unpackPhase
unpacking source archive /nix/store/b6sa05px0nsi8ih0db9kj5h68fkiabd2-source
source root is source
Running phase: patchPhase
Running phase: configurePhase
no configure script, doing nothing
Running phase: buildPhase
Checking index (/nix/var/nix/builds/nix-36945-2695095188/source/src/index.lagda.md).
Checking Type (/nix/var/nix/builds/nix-36945-2695095188/source/src/Type.lagda.md).
Checking Utils (/nix/var/nix/builds/nix-36945-2695095188/source/src/Utils.lagda.md).
Checking Builtin.Constant.Type (/nix/var/nix/builds/nix-36945-2695095188/source/src/Builtin/Constant/Type.lagda.md).
Checking Builtin.Constant.AtomicType (/nix/var/nix/builds/nix-36945-2695095188/source/src/Builtin/Constant/AtomicType.lagda.md).
Checking Utils.Reflection (/nix/var/nix/builds/nix-36945-2695095188/source/src/Utils/Reflection.lagda.md).
/nix/var/nix/builds/nix-36945-2695095188/source/src/Builtin/Constant/AtomicType.lagda.md:20.1-44: error: [SolvedButOpenHoles]
Module cannot be imported since it has open interaction points
(consider adding {-# OPTIONS --allow-unsolved-metas #-} to this
module)
when scope checking the declaration
open import Utils.Reflection using (defDec)
Loading