create Moment.now

src/Sand/SandClient.lean

@@ -179,7 +179,7 @@ def handleCmd (server : Socket) (cmd : Command) : IO Unit := do
  | .timerNotFound => timerNotFound timerId
  | Command.list => do
  let .ok timers := resp
- let now ← Moment.mk <$> IO.monoMsNow
+ let now ← Moment.now
  IO.println <| showTimers timers.data now
  | Command.pauseTimer which => match resp with
  | .ok =>

src/Sand/SandDaemon.lean

@@ -63,6 +63,6 @@ def SandDaemon.main (_args : List String) : IO α := do
  forever do
  let (client, _clientAddr) ← sock.accept
  let _tsk ← IO.asTask (prio := .dedicated) <| do
- let clientConnectedTime ← Moment.mk <$> IO.monoMsNow
+ let clientConnectedTime ← Moment.now
  let env := {state, client, clientConnectedTime, soundPath?}
  handleClient env

src/Sand/SandDaemon/HandleCommand.lean

@@ -69,7 +69,7 @@ private partial def countdown (id : TimerId) (due : Moment) : CmdHandlerT IO Uni
  loop
  where
  loop := do
- let now ← Moment.mk <$> IO.monoMsNow
+ let now ← Moment.now
  let remaining := due - now
  -- This task will be cancelled if the timer is cancelled or paused.
  -- in case of resumed, a new separate task will be spawned.

src/Sand/Time.lean

@@ -8,6 +8,8 @@ structure Moment where
  millis : Nat
  deriving Repr, ToJson, FromJson, BEq
 
+def Moment.now : IO Moment := Moment.mk <$> IO.monoMsNow
+
 structure Duration where
  millis : Nat
  deriving Repr, ToJson, FromJson, BEq