Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Try reflection again #6716

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from

Manual Pointwise instance breaks meta

a743213
Select commit
Loading
Failed to load commit list.
Draft

Try reflection again #6716

Manual Pointwise instance breaks meta
a743213
Select commit
Loading
Failed to load commit list.
IOG Hydra / ci/hydra-build:x86_64-darwin.plutus-metatheory-site failed Nov 28, 2024 in 6m 1s

Build dependency failed

1 failed steps

Details

Failed Steps

Step 1

Derivation

/nix/store/yp4lrs5x45jqdg0fzwyv1aq5fylrrlqc-plutus-metatheory-doc.drv

Log

Running phase: unpackPhase
unpacking source archive /nix/store/bh6vlh1c3gwmayfgyc06pnm372cny30j-source
source root is source
Running phase: patchPhase
Running phase: configurePhase
no configure script, doing nothing
Running phase: buildPhase
Checking index (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/index.lagda.md).
 Checking Type (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Type.lagda.md).
  Checking Utils (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Utils.lagda.md).
  Checking Builtin.Constant.Type (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Builtin/Constant/Type.lagda.md).
   Checking Builtin.Constant.AtomicType (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Builtin/Constant/AtomicType.lagda.md).
    Checking Utils.Reflection (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Utils/Reflection.lagda.md).
 Checking Type.RenamingSubstitution (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Type/RenamingSubstitution.lagda.md).
 Checking Type.Equality (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Type/Equality.lagda.md).
 Checking Type.BetaNormal (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Type/BetaNormal.lagda.md).
 Checking Type.BetaNBE (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Type/BetaNBE.lagda.md).
 Checking Type.BetaNBE.Soundness (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Type/BetaNBE/Soundness.lagda.md).
 Checking Type.BetaNBE.Completeness (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Type/BetaNBE/Completeness.lagda.md).
  Checking Type.BetaNormal.Equality (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Type/BetaNormal/Equality.lagda.md).
 Checking Type.BetaNBE.Stability (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Type/BetaNBE/Stability.lagda.md).
 Checking Type.BetaNBE.RenamingSubstitution (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Type/BetaNBE/RenamingSubstitution.lagda.md).
 Checking Builtin (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Builtin.lagda.md).
  Checking Builtin.Signature (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Builtin/Signature.lagda.md).
 Checking Declarative (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Declarative.lagda.md).
  Checking Utils.List (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Utils/List.lagda.md).
  Checking Algorithmic (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic.lagda.md).
   Checking Algorithmic.Signature (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic/Signature.lagda.md).
  Checking RawU (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/RawU.lagda.md).
   Checking Utils.Decidable (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Utils/Decidable.lagda.md).
 Checking Declarative.RenamingSubstitution (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Declarative/RenamingSubstitution.lagda.md).
 Checking Declarative.Erasure (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Declarative/Erasure.lagda.md).
  Checking Untyped (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Untyped.lagda.md).
   Checking Scoped (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Scoped.lagda.md).
    Checking Raw (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Raw.lagda.md).
  Checking Untyped.RenamingSubstitution (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Untyped/RenamingSubstitution.lagda.md).
 Checking Declarative.Examples (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Declarative/Examples.lagda.md).
  Checking Declarative.Examples.StdLib.Function (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Declarative/Examples/StdLib/Function.lagda.md).
  Checking Declarative.Examples.StdLib.ChurchNat (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Declarative/Examples/StdLib/ChurchNat.lagda.md).
  Checking Declarative.Examples.StdLib.Nat (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Declarative/Examples/StdLib/Nat.lagda.md).
 Checking Algorithmic.RenamingSubstitution (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic/RenamingSubstitution.lagda.md).
 Checking Algorithmic.Reduction (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic/Reduction.lagda.md).
  Checking Algorithmic.ReductionEC (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic/ReductionEC.lagda.md).
   Checking Algorithmic.Properties (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic/Properties.lagda.md).
   Checking Algorithmic.CEK (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic/CEK.lagda.md).
  Checking Algorithmic.ReductionEC.Progress (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic/ReductionEC/Progress.lagda.md).
  Checking Algorithmic.ReductionEC.Determinism (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic/ReductionEC/Determinism.lagda.md).
 Checking Algorithmic.Evaluation (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic/Evaluation.lagda.md).
 Checking Algorithmic.Completeness (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic/Completeness.lagda.md).
 Checking Algorithmic.Soundness (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic/Soundness.lagda.md).
 Checking Algorithmic.Erasure (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic/Erasure.lagda.md).
 Checking Algorithmic.Erasure.RenamingSubstitution (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic/Erasure/RenamingSubstitution.lagda.md).
 Checking Algorithmic.CC (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic/CC.lagda.md).
 Checking Algorithmic.CK (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic/CK.lagda.md).
 Checking Algorithmic.Examples (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Algorithmic/Examples.lagda.md).
 Checking Scoped.RenamingSubstitution (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Scoped/RenamingSubstitution.lagda.md).
 Checking Scoped.Extrication (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Scoped/Extrication.lagda.md).
 Checking Scoped.Extrication.RenamingSubstitution (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Scoped/Extrication/RenamingSubstitution.lagda.md).
 Checking Untyped.CEK (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Untyped/CEK.lagda.md).
 Checking Check (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Check.lagda.md).
 Checking Main (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Main.lagda.md).
  Checking VerifiedCompilation (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/VerifiedCompilation.lagda.md).
   Checking VerifiedCompilation.UCaseOfCase (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/VerifiedCompilation/UCaseOfCase.lagda.md).
    Checking VerifiedCompilation.Equality (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/VerifiedCompilation/Equality.lagda.md).
    Checking VerifiedCompilation.UntypedViews (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/VerifiedCompilation/UntypedViews.lagda.md).
    Checking VerifiedCompilation.UntypedTranslation (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/VerifiedCompilation/UntypedTranslation.lagda.md).
    Checking Evaluator.Base (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/Evaluator/Base.lagda.md).
   Checking VerifiedCompilation.UForceDelay (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/VerifiedCompilation/UForceDelay.lagda.md).
   Checking VerifiedCompilation.UFloatDelay (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/VerifiedCompilation/UFloatDelay.lagda.md).
    Checking VerifiedCompilation.Purity (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/VerifiedCompilation/Purity.lagda.md).
   Checking VerifiedCompilation.UCSE (/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/VerifiedCompilation/UCSE.lagda.md).
/private/tmp/nix-build-plutus-metatheory-doc.drv-0/source/src/VerifiedCompilation.lagda.md:219,1-235,8
specializeType should never fail! This is a bug!
Error:
TC doesn't provide which error to catch
when scope checking the declaration
  import VerifiedCompilation
View more details on IOG Hydra