--sharing doesn't seem to work in emacs

[m0davis]

--sharing seems to not work in emacs (--interaction) mode. The code below runs fast when Agda is invoked from the command line with --sharing. Doing similarly from emacs is slow. (NB When testing, be sure to first remove all builtin *.agdai files.)

open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

-- M n k = n modulo k
M : Nat -> Nat -> Nat
M 0       k = 0
M (suc n) k
  with suc (M n k)
... | r
  with r < k
... | true = r
... | false = 0

test-M : M 100 10 ≡ 0
test-M = refl

[m0davis]

I guess this was already talked about here (#426 (comment)) and here (#1867).