Apia doesn't support Agda "dead code" new feature

[asr]

From @asr on September 30, 2015 15:46

Agda is using a dead code analysis for reducing the interfaces file. Apia currently doesn't support this "feature".

At the moment, we removed the dead code analysis from eagda (see asr/eagda@3dbd2a6).

[asr]

I revert the eagda commit asr/eagda@3dbd2a6 in asr/eagda@7f8ce15.

[asr]

module Bug where

postulate
  D   : Set
  _≡_ : D → D → Set
  d e : D

foo : ∀ x → x ≡ x
foo x = bar
  where
  postulate
    d≡e : d ≡ e

  postulate
    bar : x ≡ x
  {-# ATP prove bar d≡e #-}

-- $ apia Bug.agda
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/Apia/Utils/AgdaAPI/Interface.hs:307

-- The error occurs because the dead code analysis removes `d≡e` from
-- the interface file.

[asr]

I revert the revert of asr/eagda@3dbd2a6 in asr/eagda@75f338a.