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

Termination checking fails #2

Open
Fuuzetsu opened this issue Sep 27, 2014 · 0 comments
Open

Termination checking fails #2

Fuuzetsu opened this issue Sep 27, 2014 · 0 comments

Comments

@Fuuzetsu
Copy link

Using Agda 2.4.2, stdlib 0.8

[shana@lenalee:~]$ for i in agdaNplib; do nix-build ~/programming/nixpkgs -o /tmp/$i -A $i --arg config '{ allowUnfree = true; }'; done 
these derivations will be built:
  /nix/store/qln7qbb46j901jyzi2r4zk2ixbdk1ckf-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv
  /nix/store/yc1blnpp0i0yv5cmdn288rdvkm5acmy7-agda.drv
building path(s) `/nix/store/w38icp5xc4jn8s2164wg478bsyqq23bh-agda'
building /nix/store/w38icp5xc4jn8s2164wg478bsyqq23bh-agda
building path(s) `/nix/store/biskc5977f16sv5c6ym74jfm915935bl-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701'
building /nix/store/biskc5977f16sv5c6ym74jfm915935bl-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701
unpacking sources
unpacking source archive /nix/store/y6mpasaczwbshpcbfqr1zdjq29z8jqix-git-export
source root is git-export
patching sources
configuring
building
Checking agda-nplib (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/agda-nplib.agda).
 Checking Algebra.FunctionProperties.NP (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Algebra/FunctionProperties/NP.agda).
  Checking Relation.Binary.NP (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Relation/Binary/NP.agda).
   Skipping Level (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Level.agdai).
    Skipping Function (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Function.agdai).
         Skipping Data.Empty (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Empty.agdai).
        Skipping Relation.Nullary.Core (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Nullary/Core.agdai).
       Skipping Relation.Nullary (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Nullary.agdai).
        Skipping Data.Maybe.Core (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Maybe/Core.agdai).
       Skipping Data.Sum (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Sum.agdai).
       Skipping Data.Product (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Product.agdai).
      Skipping Relation.Binary.Core (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary/Core.agdai).
     Skipping Relation.Binary.Consequences.Core (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary/Consequences/Core.agdai).
    Skipping Relation.Binary.PropositionalEquality.Core (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary/PropositionalEquality/Core.agdai).
    Skipping Relation.Binary.Consequences (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary/Consequences.agdai).
    Skipping Relation.Binary.Indexed.Core (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary/Indexed/Core.agdai).
   Skipping Relation.Binary (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary.agdai).
    Skipping Relation.Binary.Indexed (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary/Indexed.agdai).
    Skipping Data.Unit.Core (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Unit/Core.agdai).
    Skipping Relation.Binary.HeterogeneousEquality.Core (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary/HeterogeneousEquality/Core.agdai).
     Skipping Relation.Binary.PreorderReasoning (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary/PreorderReasoning.agdai).
    Skipping Relation.Binary.EqReasoning (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary/EqReasoning.agdai).
    Skipping Function.Equality (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Function/Equality.agdai).
   Skipping Relation.Binary.PropositionalEquality (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary/PropositionalEquality.agdai).
  Finished Relation.Binary.NP.
  Checking Type (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Type.agda).
  Finished Type.
   Skipping Algebra.FunctionProperties.Core (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra/FunctionProperties/Core.agdai).
  Skipping Algebra.FunctionProperties (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra/FunctionProperties.agdai).
 Finished Algebra.FunctionProperties.NP.
 Checking Algebra.NP (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Algebra/NP.agda).
   Skipping Algebra.Structures (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra/Structures.agdai).
  Skipping Algebra (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra.agdai).
 Finished Algebra.NP.
 Checking Category (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Category.agda).
  Checking Function.NP (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Function/NP.agda).
    Skipping Function.Injection (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Function/Injection.agdai).
     Skipping Data.Unit (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Unit.agdai).
     Skipping Data.Bool (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Bool.agdai).
     Skipping Function.Equivalence (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Function/Equivalence.agdai).
    Skipping Relation.Nullary.Decidable (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Nullary/Decidable.agdai).
    Skipping Relation.Binary.PartialOrderReasoning (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary/PartialOrderReasoning.agdai).
   Skipping Data.Nat (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Nat.agdai).
       Skipping Relation.Unary (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Unary.agdai).
          Skipping Category.Functor (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Category/Functor.agdai).
         Skipping Category.Applicative.Indexed (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Category/Applicative/Indexed.agdai).
        Skipping Category.Monad.Indexed (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Category/Monad/Indexed.agdai).
       Skipping Category.Monad (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Category/Monad.agdai).
       Skipping Category.Monad.Identity (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Category/Monad/Identity.agdai).
      Skipping Data.Maybe (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Maybe.agdai).
     Skipping Data.List (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/List.agdai).
     Skipping Category.Applicative (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Category/Applicative.agdai).
     Skipping Data.Fin (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Fin.agdai).
    Skipping Data.Vec (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Vec.agdai).
   Skipping Data.Vec.N-ary (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Vec/N-ary.agdai).
   Checking Relation.Binary.PropositionalEquality.NP (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Relation/Binary/PropositionalEquality/NP.agda).
    Checking Data.One (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Data/One.agda).
    Finished Data.One.
    Checking Relation.Binary.Bijection (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Relation/Binary/Bijection.agda).
    Finished Relation.Binary.Bijection.
    Checking Relation.Binary.Logical (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Relation/Binary/Logical.agda).
     Checking Level.NP (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Level/NP.agda).
     Finished Level.NP.
     Checking Data.Zero (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Data/Zero.agda).
     Finished Data.Zero.
     Checking Relation.Unary.NP (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Relation/Unary/NP.agda).
     Finished Relation.Unary.NP.
    Finished Relation.Binary.Logical.
   Finished Relation.Binary.PropositionalEquality.NP.
   Checking Relation.Unary.Logical (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Relation/Unary/Logical.agda).
   Finished Relation.Unary.Logical.
  Finished Function.NP.
 Finished Category.
 Checking Category.Applicative.NP (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Category/Applicative/NP.agda).
 Finished Category.Applicative.NP.
 Checking Category.Functor.NP (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Category/Functor/NP.agda).
 Finished Category.Functor.NP.
 Checking Category.Kleisli (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Category/Kleisli.agda).
 Finished Category.Kleisli.
 Checking Category.Monad.Continuation.Alias (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Category/Monad/Continuation/Alias.agda).
 Finished Category.Monad.Continuation.Alias.
 Checking Category.Monad.Continuation.Record (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Category/Monad/Continuation/Record.agda).
 Finished Category.Monad.Continuation.Record.
 Checking Category.Monad.NP (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Category/Monad/NP.agda).
 Finished Category.Monad.NP.
 Checking Category.Monad.Partiality.NP (/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Category/Monad/Partiality/NP.agda).
  Skipping Coinduction (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Coinduction.agdai).
         Skipping Relation.Binary.Reflection (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary/Reflection.agdai).
         Skipping Algebra.Operations (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra/Operations.agdai).
            Skipping Algebra.Properties.Group (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra/Properties/Group.agdai).
           Skipping Algebra.Properties.AbelianGroup (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra/Properties/AbelianGroup.agdai).
          Skipping Algebra.Properties.Ring (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra/Properties/Ring.agdai).
          Skipping Algebra.Morphism (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra/Morphism.agdai).
         Skipping Algebra.RingSolver.AlmostCommutativeRing (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra/RingSolver/AlmostCommutativeRing.agdai).
         Skipping Algebra.RingSolver.Lemmas (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra/RingSolver/Lemmas.agdai).
        Skipping Algebra.RingSolver (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra/RingSolver.agdai).
       Skipping Algebra.RingSolver.Simple (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra/RingSolver/Simple.agdai).
         Skipping Algebra.Properties.Lattice (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra/Properties/Lattice.agdai).
        Skipping Algebra.Properties.DistributiveLattice (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra/Properties/DistributiveLattice.agdai).
       Skipping Algebra.Properties.BooleanAlgebra (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra/Properties/BooleanAlgebra.agdai).
      Skipping Data.Bool.Properties (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Bool/Properties.agdai).
       Skipping Data.Plus (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Plus.agdai).
          Skipping Data.Nat.Properties.Simple (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Nat/Properties/Simple.agdai).
         Skipping Data.Nat.Properties (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Nat/Properties.agdai).
        Skipping Data.Fin.Properties (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Fin/Properties.agdai).
          Skipping Function.LeftInverse (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Function/LeftInverse.agdai).
          Skipping Function.Surjection (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Function/Surjection.agdai).
         Skipping Function.Bijection (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Function/Bijection.agdai).
        Skipping Function.Inverse (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Function/Inverse.agdai).
        Skipping Data.Vec.Equality (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Vec/Equality.agdai).
         Skipping Relation.Binary.List.Pointwise (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary/List/Pointwise.agdai).
         Skipping Relation.Binary.InducedPreorders (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary/InducedPreorders.agdai).
         Skipping Function.Related (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Function/Related.agdai).
        Skipping Data.List.Any (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/List/Any.agdai).
        Skipping Relation.Binary.HeterogeneousEquality (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary/HeterogeneousEquality.agdai).
       Skipping Data.Vec.Properties (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Vec/Properties.agdai).
      Skipping Relation.Binary.Vec.Pointwise (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Binary/Vec/Pointwise.agdai).
      Skipping Algebra.Properties.BooleanAlgebra.Expression (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Algebra/Properties/BooleanAlgebra/Expression.agdai).
     Skipping Data.Fin.Subset (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Fin/Subset.agdai).
     Skipping Data.Fin.Subset.Properties (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Fin/Subset/Properties.agdai).
    Skipping Data.Fin.Dec (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Data/Fin/Dec.agdai).
   Skipping Relation.Nullary.Negation (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Relation/Nullary/Negation.agdai).
  Skipping Category.Monad.Partiality (/nix/store/m34l2znd0sm6y4na23rvpy5b9m6hzi44-Agda-stdlib/share/agda/Category/Monad/Partiality.agdai).
 Finished Category.Monad.Partiality.NP.
/tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/agda-nplib.agda:11,8-36
Termination checking failed for the following functions:
  Monad.Partiality.NP.Workaround.never
Problematic calls:
  .Category.Monad.Partiality.NP.Workaround.♯-0
    (at /tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Category/Monad/Partiality/NP.agda:16,18-19)
  never
    (at /tmp/nix-build-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv-0/git-export/lib/Category/Monad/Partiality/NP.agda:16,20-25)
when scope checking the declaration
  import Category.Monad.Partiality.NP
builder for `/nix/store/qln7qbb46j901jyzi2r4zk2ixbdk1ckf-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv' failed with exit code 1
error: build of `/nix/store/qln7qbb46j901jyzi2r4zk2ixbdk1ckf-agda-nplib-3f6b6acb36c7cfd7e3366e38d4d578835b574701.drv' failed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@Fuuzetsu