Hi,
On Fri, Nov 10, 2017 at 01:18:07AM +0200, Adrian Bunk wrote:
> Source: agda-stdlib
> Version: 0.13-1
> Severity: serious
>
> Some recent change in unstable makes agda-stdlib FTBFS:
>
> https://tests.reproducible-builds.org/debian/history/agda-stdlib.html
> https://tests.reproducible-builds.org/debian/rb-pkg/unstable/amd64/agda-stdlib.html
>
> ...
> debian/rules override_dh_auto_build
> make[1]: Entering directory '/build/1st/agda-stdlib-0.13'
> ghc --make GenerateEverything.hs
> [1 of 1] Compiling Main ( GenerateEverything.hs,
> GenerateEverything.o )
> Linking GenerateEverything ...
> ./GenerateEverything
> agda +RTS -K1G -RTS -i /build/1st/agda-stdlib-0.13 -i
> /build/1st/agda-stdlib-0.13/src /build/1st/agda-stdlib-0.13/Everything.agda
> Checking Everything (/build/1st/agda-stdlib-0.13/Everything.agda).
> Checking Algebra (/build/1st/agda-stdlib-0.13/src/Algebra.agda).
> Checking Relation.Binary
> (/build/1st/agda-stdlib-0.13/src/Relation/Binary.agda).
> Checking Data.Product (/build/1st/agda-stdlib-0.13/src/Data/Product.agda).
> Checking Function (/build/1st/agda-stdlib-0.13/src/Function.agda).
> Checking Level (/build/1st/agda-stdlib-0.13/src/Level.agda).
> Finished Level.
> Finished Function.
> Checking Relation.Nullary
> (/build/1st/agda-stdlib-0.13/src/Relation/Nullary.agda).
> Checking Data.Empty (/build/1st/agda-stdlib-0.13/src/Data/Empty.agda).
> /build/1st/agda-stdlib-0.13/src/Data/Empty.agda:13,1-31
> The HASKELL pragma has been deprecated. Use
> {-# FOREIGN GHC data AgdaEmpty #-} instead. This will be an error
> in Agda 2.6.
> when scope checking the declaration
> {-# HASKELL
> data AgdaEmpty
> #-}
> /build/1st/agda-stdlib-0.13/src/Data/Empty.agda:14,1-58
> The COMPILED_DATA pragma has been deprecated. Use
> {-# COMPILE GHC /build/1st/agda-stdlib-0.13/src/Relation/Nullary.agda:11,13-23
> <stdout>: commitBuffer: invalid argument (invalid character)
> debian/rules:13: recipe for target 'override_dh_auto_build' failed
> make[1]: *** [override_dh_auto_build] Error 1
This seems to be related to
https://github.com/commercialhaskell/stack/issues/793 and setting
LC_ALL=C.UTF-8 makes the build continue, but the agda-stdlib is no
longer compatible with present agda and thus fails with a type check
error:
| Checking Data.Nat.LCM (/<<PKGBUILDDIR>>/src/Data/Nat/LCM.agda).
| /<<PKGBUILDDIR>>/src/Data/Nat/LCM.agda:119,1-125,23
| q₁ * q₂ * d′ !=
| proj₁
| (lcm (q₁ * d′) (q₂ * d′)
| | proj₁
| (gcd (q₁ * d′) (q₂ * d′)
| | .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (q₁ * d′ , q₂ * d′)
| ((λ y y<x →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (q₁ * d′ , y)
| (.Induction.WellFounded.Some.wfRec-builder (Bézout.Lemma (q₁ * d′))
| (λ y₁ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (q₁ * d′ , y₁)
| (y-rec ,
| (λ y₂ y<x₁ y₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₂ , y₃)
| ((λ y₄ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₂ , y₄)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma y₂)
| (λ y₅ y-rec₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₂ ,
y₅)
| (y-rec₁ ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₆ : ℕ) → Bézout.Lemma x y₆)
| (λ x x-rec y₆ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x
, y₆)
| ((λ y₇ y<x₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ *
d′) (x , y₇)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₈ y-rec₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂
* d′) (x , y₈)
| (y-rec₂ , x-rec))
| y₇ (.Induction.Nat.<-well-founded′ y₆ y₇
y<x₃)
| , x-rec))
| , x-rec))
| y₂ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₂
y<x₁)))
| y₄ (.Induction.Nat.<-well-founded′ y₃ y₄ y<x₂)
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₅ : ℕ) → Bézout.Lemma x y₅)
| (λ x x-rec y₅ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₅)
| ((λ y₆ y<x₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x
, y₆)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₇ y-rec₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ *
d′) (x , y₇)
| (y-rec₁ , x-rec))
| y₆ (.Induction.Nat.<-well-founded′ y₅ y₆ y<x₃)
| , x-rec))
| , x-rec))
| y₂ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₂ y<x₁)))
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₄ : ℕ) → Bézout.Lemma x y₄)
| (λ x x-rec y₄ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₄)
| ((λ y₅ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₅)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₆ y-rec₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x
, y₆)
| (y-rec₁ , x-rec))
| y₅ (.Induction.Nat.<-well-founded′ y₄ y₅ y<x₂)
| , x-rec))
| , x-rec))
| y₂ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₂ y<x₁)))))
| y (.Induction.Nat.<-well-founded′ (q₂ * d′) y y<x)
| ,
| (λ y₁ y<x₁ y₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₁ , y₂)
| ((λ y₃ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₁ , y₃)
| (.Induction.WellFounded.Some.wfRec-builder (Bézout.Lemma y₁)
| (λ y₄ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₁ , y₄)
| (y-rec ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₅ : ℕ) → Bézout.Lemma x y₅)
| (λ x x-rec y₅ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₅)
| ((λ y₆ y<x₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x
, y₆)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₇ y-rec₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ *
d′) (x , y₇)
| (y-rec₁ , x-rec))
| y₆ (.Induction.Nat.<-well-founded′ y₅ y₆ y<x₃)
| , x-rec))
| , x-rec))
| y₁ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₁ y<x₁)))
| y₃ (.Induction.Nat.<-well-founded′ y₂ y₃ y<x₂)
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₄ : ℕ) → Bézout.Lemma x y₄)
| (λ x x-rec y₄ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₄)
| ((λ y₅ y<x₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₅)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₆ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x
, y₆)
| (y-rec , x-rec))
| y₅ (.Induction.Nat.<-well-founded′ y₄ y₅ y<x₃)
| , x-rec))
| , x-rec))
| y₁ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₁ y<x₁)))
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₃ : ℕ) → Bézout.Lemma x y₃)
| (λ x x-rec y₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₃)
| ((λ y₄ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₄)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₅ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₅)
| (y-rec , x-rec))
| y₄ (.Induction.Nat.<-well-founded′ y₃ y₄ y<x₂)
| , x-rec))
| , x-rec))
| y₁ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₁ y<x₁)))))
| ,
| (λ y y<x y₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y , y₁)
| ((λ y₂ y<x₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y , y₂)
| (.Induction.WellFounded.Some.wfRec-builder (Bézout.Lemma y)
| (λ y₃ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y , y₃)
| (y-rec ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₄ : ℕ) → Bézout.Lemma x y₄)
| (λ x x-rec y₄ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₄)
| ((λ y₅ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₅)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₆ y-rec₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x
, y₆)
| (y-rec₁ , x-rec))
| y₅ (.Induction.Nat.<-well-founded′ y₄ y₅ y<x₂)
| , x-rec))
| , x-rec))
| y (.Induction.Nat.<-well-founded′ (q₁ * d′) y y<x)))
| y₂ (.Induction.Nat.<-well-founded′ y₁ y₂ y<x₁)
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₃ : ℕ) → Bézout.Lemma x y₃)
| (λ x x-rec y₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₃)
| ((λ y₄ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₄)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₅ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₅)
| (y-rec , x-rec))
| y₄ (.Induction.Nat.<-well-founded′ y₃ y₄ y<x₂)
| , x-rec))
| , x-rec))
| y (.Induction.Nat.<-well-founded′ (q₁ * d′) y y<x)))
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₂ : ℕ) → Bézout.Lemma x y₂)
| (λ x x-rec y₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₂)
| ((λ y₃ y<x₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₃)
| (.Induction.WellFounded.Some.wfRec-builder (Bézout.Lemma x)
| (λ y₄ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₄)
| (y-rec , x-rec))
| y₃ (.Induction.Nat.<-well-founded′ y₂ y₃ y<x₁)
| , x-rec))
| , x-rec))
| y (.Induction.Nat.<-well-founded′ (q₁ * d′) y y<x)))))
| ,
| (gcd-gcd′
| (proj₂
| (gcd (q₁ * d′) (q₂ * d′)
| | .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (q₁ * d′ , q₂ * d′)
| ((λ y y<x →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (q₁ * d′ , y)
| (.Induction.WellFounded.Some.wfRec-builder (Bézout.Lemma (q₁ *
d′))
| (λ y₁ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (q₁ * d′ , y₁)
| (y-rec ,
| (λ y₂ y<x₁ y₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₂ , y₃)
| ((λ y₄ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₂ , y₄)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma y₂)
| (λ y₅ y-rec₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₂
, y₅)
| (y-rec₁ ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₆ : ℕ) → Bézout.Lemma x y₆)
| (λ x x-rec y₆ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′)
(x , y₆)
| ((λ y₇ y<x₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ *
d′) (x , y₇)
|
(.Induction.WellFounded.Some.wfRec-builder (Bézout.Lemma x)
| (λ y₈ y-rec₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′)
(q₂ * d′) (x , y₈)
| (y-rec₂ , x-rec))
| y₇ (.Induction.Nat.<-well-founded′ y₆ y₇
y<x₃)
| , x-rec))
| , x-rec))
| y₂ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₂
y<x₁)))
| y₄ (.Induction.Nat.<-well-founded′ y₃ y₄ y<x₂)
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₅ : ℕ) → Bézout.Lemma x y₅)
| (λ x x-rec y₅ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₅)
| ((λ y₆ y<x₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′)
(x , y₆)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₇ y-rec₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ *
d′) (x , y₇)
| (y-rec₁ , x-rec))
| y₆ (.Induction.Nat.<-well-founded′ y₅ y₆
y<x₃)
| , x-rec))
| , x-rec))
| y₂ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₂
y<x₁)))
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₄ : ℕ) → Bézout.Lemma x y₄)
| (λ x x-rec y₄ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₄)
| ((λ y₅ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₅)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₆ y-rec₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′)
(x , y₆)
| (y-rec₁ , x-rec))
| y₅ (.Induction.Nat.<-well-founded′ y₄ y₅ y<x₂)
| , x-rec))
| , x-rec))
| y₂ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₂ y<x₁)))))
| y (.Induction.Nat.<-well-founded′ (q₂ * d′) y y<x)
| ,
| (λ y₁ y<x₁ y₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₁ , y₂)
| ((λ y₃ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₁ , y₃)
| (.Induction.WellFounded.Some.wfRec-builder (Bézout.Lemma
y₁)
| (λ y₄ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₁ , y₄)
| (y-rec ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₅ : ℕ) → Bézout.Lemma x y₅)
| (λ x x-rec y₅ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₅)
| ((λ y₆ y<x₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′)
(x , y₆)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₇ y-rec₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ *
d′) (x , y₇)
| (y-rec₁ , x-rec))
| y₆ (.Induction.Nat.<-well-founded′ y₅ y₆
y<x₃)
| , x-rec))
| , x-rec))
| y₁ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₁
y<x₁)))
| y₃ (.Induction.Nat.<-well-founded′ y₂ y₃ y<x₂)
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₄ : ℕ) → Bézout.Lemma x y₄)
| (λ x x-rec y₄ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₄)
| ((λ y₅ y<x₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₅)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₆ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′)
(x , y₆)
| (y-rec , x-rec))
| y₅ (.Induction.Nat.<-well-founded′ y₄ y₅ y<x₃)
| , x-rec))
| , x-rec))
| y₁ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₁ y<x₁)))
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₃ : ℕ) → Bézout.Lemma x y₃)
| (λ x x-rec y₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₃)
| ((λ y₄ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₄)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₅ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₅)
| (y-rec , x-rec))
| y₄ (.Induction.Nat.<-well-founded′ y₃ y₄ y<x₂)
| , x-rec))
| , x-rec))
| y₁ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₁ y<x₁)))))
| ,
| (λ y y<x y₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y , y₁)
| ((λ y₂ y<x₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y , y₂)
| (.Induction.WellFounded.Some.wfRec-builder (Bézout.Lemma y)
| (λ y₃ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y , y₃)
| (y-rec ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₄ : ℕ) → Bézout.Lemma x y₄)
| (λ x x-rec y₄ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₄)
| ((λ y₅ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₅)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₆ y-rec₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′)
(x , y₆)
| (y-rec₁ , x-rec))
| y₅ (.Induction.Nat.<-well-founded′ y₄ y₅ y<x₂)
| , x-rec))
| , x-rec))
| y (.Induction.Nat.<-well-founded′ (q₁ * d′) y y<x)))
| y₂ (.Induction.Nat.<-well-founded′ y₁ y₂ y<x₁)
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₃ : ℕ) → Bézout.Lemma x y₃)
| (λ x x-rec y₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₃)
| ((λ y₄ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₄)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₅ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₅)
| (y-rec , x-rec))
| y₄ (.Induction.Nat.<-well-founded′ y₃ y₄ y<x₂)
| , x-rec))
| , x-rec))
| y (.Induction.Nat.<-well-founded′ (q₁ * d′) y y<x)))
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₂ : ℕ) → Bézout.Lemma x y₂)
| (λ x x-rec y₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₂)
| ((λ y₃ y<x₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₃)
| (.Induction.WellFounded.Some.wfRec-builder (Bézout.Lemma
x)
| (λ y₄ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₄)
| (y-rec , x-rec))
| y₃ (.Induction.Nat.<-well-founded′ y₂ y₃ y<x₁)
| , x-rec))
| , x-rec))
| y (.Induction.Nat.<-well-founded′ (q₁ * d′) y y<x))))))
| | GCD.commonDivisor
| (proj₂
| (gcd (q₁ * d′) (q₂ * d′)
| | .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (q₁ * d′ , q₂ * d′)
| ((λ y y<x →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (q₁ * d′ , y)
| (.Induction.WellFounded.Some.wfRec-builder (Bézout.Lemma (q₁ *
d′))
| (λ y₁ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (q₁ * d′ , y₁)
| (y-rec ,
| (λ y₂ y<x₁ y₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₂ , y₃)
| ((λ y₄ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₂ ,
y₄)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma y₂)
| (λ y₅ y-rec₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′)
(y₂ , y₅)
| (y-rec₁ ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₆ : ℕ) → Bézout.Lemma x y₆)
| (λ x x-rec y₆ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ *
d′) (x , y₆)
| ((λ y₇ y<x₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂
* d′) (x , y₇)
|
(.Induction.WellFounded.Some.wfRec-builder (Bézout.Lemma x)
| (λ y₈ y-rec₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′)
(q₂ * d′) (x , y₈)
| (y-rec₂ , x-rec))
| y₇ (.Induction.Nat.<-well-founded′ y₆
y₇ y<x₃)
| , x-rec))
| , x-rec))
| y₂ (.Induction.Nat.<-well-founded′ (q₁ * d′)
y₂ y<x₁)))
| y₄ (.Induction.Nat.<-well-founded′ y₃ y₄ y<x₂)
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₅ : ℕ) → Bézout.Lemma x y₅)
| (λ x x-rec y₅ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x
, y₅)
| ((λ y₆ y<x₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ *
d′) (x , y₆)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₇ y-rec₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂
* d′) (x , y₇)
| (y-rec₁ , x-rec))
| y₆ (.Induction.Nat.<-well-founded′ y₅ y₆
y<x₃)
| , x-rec))
| , x-rec))
| y₂ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₂
y<x₁)))
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₄ : ℕ) → Bézout.Lemma x y₄)
| (λ x x-rec y₄ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₄)
| ((λ y₅ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x
, y₅)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₆ y-rec₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ *
d′) (x , y₆)
| (y-rec₁ , x-rec))
| y₅ (.Induction.Nat.<-well-founded′ y₄ y₅ y<x₂)
| , x-rec))
| , x-rec))
| y₂ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₂
y<x₁)))))
| y (.Induction.Nat.<-well-founded′ (q₂ * d′) y y<x)
| ,
| (λ y₁ y<x₁ y₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₁ , y₂)
| ((λ y₃ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₁ , y₃)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma y₁)
| (λ y₄ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y₁ ,
y₄)
| (y-rec ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₅ : ℕ) → Bézout.Lemma x y₅)
| (λ x x-rec y₅ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x
, y₅)
| ((λ y₆ y<x₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ *
d′) (x , y₆)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₇ y-rec₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂
* d′) (x , y₇)
| (y-rec₁ , x-rec))
| y₆ (.Induction.Nat.<-well-founded′ y₅ y₆
y<x₃)
| , x-rec))
| , x-rec))
| y₁ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₁
y<x₁)))
| y₃ (.Induction.Nat.<-well-founded′ y₂ y₃ y<x₂)
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₄ : ℕ) → Bézout.Lemma x y₄)
| (λ x x-rec y₄ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₄)
| ((λ y₅ y<x₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x
, y₅)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₆ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ *
d′) (x , y₆)
| (y-rec , x-rec))
| y₅ (.Induction.Nat.<-well-founded′ y₄ y₅ y<x₃)
| , x-rec))
| , x-rec))
| y₁ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₁ y<x₁)))
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₃ : ℕ) → Bézout.Lemma x y₃)
| (λ x x-rec y₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₃)
| ((λ y₄ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₄)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₅ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x
, y₅)
| (y-rec , x-rec))
| y₄ (.Induction.Nat.<-well-founded′ y₃ y₄ y<x₂)
| , x-rec))
| , x-rec))
| y₁ (.Induction.Nat.<-well-founded′ (q₁ * d′) y₁ y<x₁)))))
| ,
| (λ y y<x y₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y , y₁)
| ((λ y₂ y<x₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y , y₂)
| (.Induction.WellFounded.Some.wfRec-builder (Bézout.Lemma y)
| (λ y₃ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (y , y₃)
| (y-rec ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₄ : ℕ) → Bézout.Lemma x y₄)
| (λ x x-rec y₄ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₄)
| ((λ y₅ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x
, y₅)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₆ y-rec₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ *
d′) (x , y₆)
| (y-rec₁ , x-rec))
| y₅ (.Induction.Nat.<-well-founded′ y₄ y₅ y<x₂)
| , x-rec))
| , x-rec))
| y (.Induction.Nat.<-well-founded′ (q₁ * d′) y y<x)))
| y₂ (.Induction.Nat.<-well-founded′ y₁ y₂ y<x₁)
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₃ : ℕ) → Bézout.Lemma x y₃)
| (λ x x-rec y₃ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₃)
| ((λ y₄ y<x₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₄)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₅ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x
, y₅)
| (y-rec , x-rec))
| y₄ (.Induction.Nat.<-well-founded′ y₃ y₄ y<x₂)
| , x-rec))
| , x-rec))
| y (.Induction.Nat.<-well-founded′ (q₁ * d′) y y<x)))
| ,
| .Induction.WellFounded.Some.wfRec-builder
| (λ x → (y₂ : ℕ) → Bézout.Lemma x y₂)
| (λ x x-rec y₂ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₂)
| ((λ y₃ y<x₁ →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x , y₃)
| (.Induction.WellFounded.Some.wfRec-builder
(Bézout.Lemma x)
| (λ y₄ y-rec →
| .Data.Nat.GCD.Bézout.gcd (q₁ * d′) (q₂ * d′) (x ,
y₄)
| (y-rec , x-rec))
| y₃ (.Induction.Nat.<-well-founded′ y₂ y₃ y<x₁)
| , x-rec))
| , x-rec))
| y (.Induction.Nat.<-well-founded′ (q₁ * d′) y y<x))))))))
| of type ℕ
| when checking that the clause
| .Data.Nat.LCM.with-344 {.(q₁ * d′)} {.(q₂ * d′)}
| (d′ , gcd-* q₁ q₂ q₁-q₂-coprime)
| l
| {d}
| g
| with GCD.unique g (gcd′-gcd (gcd-* q₁ q₂ q₁-q₂-coprime))
| .Data.Nat.LCM.with-344 {.(q₁ * d)} {.(q₂ * d)}
| (.d , gcd-* q₁ q₂ q₁-q₂-coprime)
| l
| {d}
| g
| | refl
| = solve 3
| (λ q₁ q₂ d → q₁ :* d :* (q₂ :* d) := d :* (q₁ :* q₂ :* d)) refl q₁
| q₂ d
| has type
| {i j : ℕ} (w : Σ ℕ (GCD′ i j)) (l : LCM i j (proj₁ (lcm i j | w)))
| {d : ℕ} (g : GCD i j d) →
| i * j ≡ d * proj₁ (lcm i j | w)
| debian/rules:15: recipe for target 'override_dh_auto_build' failed
| make[1]: *** [override_dh_auto_build] Error 1
| make[1]: Leaving directory '/<<PKGBUILDDIR>>'
| debian/rules:29: recipe for target 'build' failed
| make: *** [build] Error 2
| dpkg-buildpackage: error: debian/rules build subprocess returned exit status 2
I guess we'll need a new upstream release here.
I'm attaching the patch I have, but it doesn't make it build.
Helmut
diff --minimal -Nru agda-stdlib-0.13/debian/changelog
agda-stdlib-0.13/debian/changelog
--- agda-stdlib-0.13/debian/changelog 2017-07-06 11:16:33.000000000 +0200
+++ agda-stdlib-0.13/debian/changelog 2017-11-17 15:14:14.000000000 +0100
@@ -1,3 +1,12 @@
+agda-stdlib (0.13-2) UNRELEASED; urgency=medium
+
+ * Team upload.
+ * Address FTBFS: export LC_ALL=C.UTF-8. (Addresses: #881307)
+ * Bump agda-bin Breaks due to agdai incompatibility.
+ * Tighten up agda relation ships to detect incompatibility next time.
+
+ -- Helmut Grohne <hel...@subdivi.de> Fri, 17 Nov 2017 15:14:14 +0100
+
agda-stdlib (0.13-1) unstable; urgency=medium
[ Gianfranco Costamagna ]
diff --minimal -Nru agda-stdlib-0.13/debian/control
agda-stdlib-0.13/debian/control
--- agda-stdlib-0.13/debian/control 2017-07-06 11:16:33.000000000 +0200
+++ agda-stdlib-0.13/debian/control 2017-11-17 15:14:14.000000000 +0100
@@ -4,10 +4,10 @@
Maintainer: Iain Lane <la...@debian.org>
Uploaders: Debian Haskell Group
<pkg-haskell-maintain...@lists.alioth.debian.org>
Build-Depends: debhelper (>= 10),
- agda-bin (>= 2.5.1),
- agda-bin (<< 2.6.0),
- libghc-agda-dev (>= 2.5.1),
- libghc-agda-dev (<< 2.6.0),
+ agda-bin (>= 2.5.3),
+ agda-bin (<< 2.5.4~),
+ libghc-agda-dev (>= 2.5.3),
+ libghc-agda-dev (<< 2.5.4~),
libghc-filemanip-dev
Standards-Version: 4.0.0
Vcs-Browser: https://anonscm.debian.org/cgit/collab-maint/agda-stdlib.git
@@ -17,9 +17,9 @@
Package: agda-stdlib
Architecture: all
Depends: ${misc:Depends},
- libghc-agda-dev (>= 2.5.1),
- libghc-agda-dev (<< 2.6.0)
-Breaks: agda-bin (<< 2.5.1)
+ libghc-agda-dev (>= 2.5.3),
+ libghc-agda-dev (<< 2.5.4~)
+Breaks: agda-bin (<< 2.5.3)
Enhances: elpa-agda2-mode
Description: standard library for Agda
Agda is a dependently typed functional programming language: It has inductive
diff --minimal -Nru agda-stdlib-0.13/debian/rules agda-stdlib-0.13/debian/rules
--- agda-stdlib-0.13/debian/rules 2017-07-06 11:16:33.000000000 +0200
+++ agda-stdlib-0.13/debian/rules 2017-11-17 15:14:14.000000000 +0100
@@ -1,5 +1,7 @@
#!/usr/bin/make -f
+export LC_ALL=C.UTF-8
+
override_dh_auto_clean:
find $(CURDIR) -name "*.agdai" -delete
rm -rf $(CURDIR)/html
