We say Idris has strict evaluation, but this is for its run-time semantics.
Being a fully dependently typed language, Idris has two phases where it evaluates things, compile-time and run-time. At compile-time it will only evaluate things which it knows to be total (i.e. terminating and covering all possible inputs) in order to keep type checking decidable. The compile-time evaluator is part of the Idris kernel, and is implemented in Haskell using a HOAS (higher order abstract syntax) style representation of values. Since everything is known to have a normal form here, the evaluation strategy doesn't actually matter because either way it will get the same answer, and in practice it will do whatever the Haskell run-time system chooses to do.
The REPL, for convenience, uses the compile-time notion of evaluation. So, your 'spin 1000' is never actually getting evaluated. If you make an executable with the same code, I would expect to see very different behaviour.
As well as being easier to implement (because we have the evaluator available) this can be very useful to show how terms evaluate in the type checker. So you can see the difference between:
Idris> \n, m => (S n) + m
\n => \m => S (plus n m) : Nat -> Nat -> Nat
Idris> \n, m => n + (S m)
\n => \m => plus n (S m) : Nat -> Nat -> Nat
This would be harder (though not impossible) if we used the run-time evaluation at the REPL, which doesn't reduce under lambdas.