From da96a88e39dec4df77064618509f49f39f2525c3 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 16 Apr 2024 11:58:50 +0100
Subject: [PATCH 01/11] [ new ] IO conditionals & loops

---
 CHANGELOG.md     | 14 +++++++++++++-
 src/IO/Base.agda | 43 +++++++++++++++++++++++++++++++++++++++----
 2 files changed, 52 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 469c926af8..21e67a6080 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -54,6 +54,11 @@ Deprecated names
   *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
   ```
 
+* In `IO.Base`:
+  ```agda
+  untilRight  ↦  untilInj₂
+  ```
+
 New modules
 -----------
 
@@ -378,9 +383,16 @@ Additions to existing modules
 * Added new functions in `Data.String.Base`:
   ```agda
   map : (Char → Char) → String → String
+  ```
 
-* Added new definition in `Relation.Binary.Construct.Closure.Transitive`
+* Added new functions in `IO.Base`:
+  ```agda
+  whenInj₂ : E ⊎ A → (A → IO ⊤) → IO ⊤
+  forever : IO ⊤ → IO ⊤
   ```
+
+* Added new definition in `Relation.Binary.Construct.Closure.Transitive`
+  ```agda
   transitive⁻ : Transitive _∼_ → TransClosure _∼_ ⇒ _∼_
   ```
 
diff --git a/src/IO/Base.agda b/src/IO/Base.agda
index 8c44474935..ef264d3aae 100644
--- a/src/IO/Base.agda
+++ b/src/IO/Base.agda
@@ -20,9 +20,10 @@ import IO.Primitive as Prim
 
 private
   variable
-    a b : Level
+    a b e : Level
     A : Set a
     B : Set b
+    E : Set e
 
 ------------------------------------------------------------------------
 -- The IO monad
@@ -106,18 +107,37 @@ lift′ io = lift (io Prim.>>= λ _ → Prim.pure _)
 ignore : IO A → IO ⊤
 ignore io = io >> pure _
 
+
+------------------------------------------------------------------------
 -- Conditional executions
+
+-- Only run the action if the boolean is true
 when : Bool → IO {a} ⊤ → IO ⊤
 when true m = m
 when false _ = pure _
 
+-- Only run the action if the boolean is false
 unless : Bool → IO {a} ⊤ → IO ⊤
 unless = when ∘′ not
 
+-- Run the action if the `Maybe` computation was successful
 whenJust : Maybe A → (A → IO {a} ⊤) → IO ⊤
 whenJust (just a) k = k a
 whenJust nothing  _ = pure _
 
+-- Run the action if the `E ⊎_` computation was successful
+whenInj₂ : E ⊎ A → (A → IO {a} ⊤) → IO ⊤
+whenInj₂ (inj₂ a) k = k a
+whenInj₂ (inj₁ _) _ = pure _
+
+
+------------------------------------------------------------------------
+-- Loops
+
+-- Keep running the action forever
+forever : IO {a} ⊤ → IO {a} ⊤
+forever act = seq (♯ act) (♯ forever act)
+
 -- Keep running an IO action until we get a value. Convenient when user
 -- input is involved and it may be malformed.
 untilJust : IO (Maybe A) → IO A
@@ -127,7 +147,22 @@ untilJust m = bind (♯ m) λ where
   nothing  → ♯ untilJust m
   (just a) → ♯ pure a
 
-untilRight : {A B : Set a} → (A → IO (A ⊎ B)) → A → IO B
-untilRight f x = bind (♯ f x) λ where
-  (inj₁ x′) → ♯ untilRight f x′
+untilInj₂ : {A B : Set a} → (A → IO (A ⊎ B)) → A → IO B
+untilInj₂ f x = bind (♯ f x) λ where
+  (inj₁ x′) → ♯ untilInj₂ f x′
   (inj₂ y) → ♯ pure y
+
+
+
+
+
+
+
+------------------------------------------------------------------------
+-- DEPRECATIONS
+
+untilRight = untilInj₂
+{-# WARNING_ON_USAGE untilRight
+"Warning: untilRight was deprecated in v2.1.
+Please use untilInj₂ instead."
+#-}

From a8be23162f72fa0410ebe82ebe1604f2a12f9aac Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 16 Apr 2024 12:58:44 +0100
Subject: [PATCH 02/11] [ new ] stdin, stdout, stderr, buffering, etc.

---
 CHANGELOG.md                                  |  7 +++
 GenerateEverything.hs                         |  4 +-
 src/IO.agda                                   |  3 +-
 src/IO/Base.agda                              |  2 +-
 src/IO/Finite.agda                            |  2 +-
 src/IO/Handle.agda                            | 41 +++++++++++++
 src/IO/Infinite.agda                          |  2 +-
 .../{Primitive.agda => Primitive/Core.agda}   |  2 +-
 src/IO/Primitive/Handle.agda                  | 61 +++++++++++++++++++
 9 files changed, 118 insertions(+), 6 deletions(-)
 create mode 100644 src/IO/Handle.agda
 rename src/IO/{Primitive.agda => Primitive/Core.agda} (96%)
 create mode 100644 src/IO/Primitive/Handle.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 21e67a6080..fc530458b7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -26,6 +26,7 @@ Non-backwards compatible changes
   parametrized by _raw_ bundles, and as such take a proof of transitivity.
 * The definitions in `Algebra.Module.Morphism.Construct.Identity` are now
   parametrized by _raw_ bundles, and as such take a proof of reflexivity.
+* The module `IO.Primitive` was moved to `IO.Primitive.Core`.
 
 Other major improvements
 ------------------------
@@ -130,6 +131,12 @@ New modules
   Data.Container.Indexed.Relation.Binary.Equality.Setoid
   ```
 
+* New IO primitives to handle buffering
+  ```agda
+  IO.Primitive.Handle
+  IO.Handle
+  ```
+
 Additions to existing modules
 -----------------------------
 
diff --git a/GenerateEverything.hs b/GenerateEverything.hs
index f6add73649..8f75b549bf 100644
--- a/GenerateEverything.hs
+++ b/GenerateEverything.hs
@@ -56,11 +56,13 @@ unsafeModules = map modToFile
   , "IO"
   , "IO.Base"
   , "IO.Categorical"
+  , "IO.Handle"
   , "IO.Infinite"
   , "IO.Instances"
   , "IO.Effectful"
   , "IO.Finite"
-  , "IO.Primitive"
+  , "IO.Primitive.Core"
+  , "IO.Primitive.Handle"
   , "IO.Primitive.Infinite"
   , "IO.Primitive.Finite"
   , "Relation.Binary.PropositionalEquality.TrustMe"
diff --git a/src/IO.agda b/src/IO.agda
index 96f7db2760..0462d9b8b9 100644
--- a/src/IO.agda
+++ b/src/IO.agda
@@ -14,7 +14,7 @@ open import Data.Unit.Polymorphic.Base
 open import Data.String.Base using (String)
 import Data.Unit.Base as Unit0
 open import Function.Base using (_∘_; flip)
-import IO.Primitive as Prim
+import IO.Primitive.Core as Prim
 open import Level
 
 private
@@ -27,6 +27,7 @@ private
 -- Re-exporting the basic type and functions
 
 open import IO.Base public
+open import IO.Handle public
 
 ------------------------------------------------------------------------
 -- Utilities
diff --git a/src/IO/Base.agda b/src/IO/Base.agda
index ef264d3aae..54aff90dfc 100644
--- a/src/IO/Base.agda
+++ b/src/IO/Base.agda
@@ -16,7 +16,7 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 import Agda.Builtin.Unit as Unit0
 open import Data.Unit.Polymorphic.Base
 open import Function.Base using (_∘′_; const; flip)
-import IO.Primitive as Prim
+import IO.Primitive.Core as Prim
 
 private
   variable
diff --git a/src/IO/Finite.agda b/src/IO/Finite.agda
index 44b5edc050..1827d471b9 100644
--- a/src/IO/Finite.agda
+++ b/src/IO/Finite.agda
@@ -12,7 +12,7 @@ open import Data.Unit.Polymorphic.Base
 open import Agda.Builtin.String
 import Data.Unit.Base as Unit0
 open import IO.Base
-import IO.Primitive as Prim
+import IO.Primitive.Core as Prim
 import IO.Primitive.Finite as Prim
 open import Level
 
diff --git a/src/IO/Handle.agda b/src/IO/Handle.agda
new file mode 100644
index 0000000000..0c15906201
--- /dev/null
+++ b/src/IO/Handle.agda
@@ -0,0 +1,41 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- IO handles: simple bindings to Haskell types and functions
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --guardedness #-}
+
+module IO.Handle where
+
+open import Level using (Level)
+open import Data.Unit.Polymorphic.Base using (⊤)
+open import IO.Base using (IO; lift; lift′)
+
+private variable a : Level
+
+------------------------------------------------------------------------
+-- Re-exporting types and constructors
+
+open import IO.Primitive.Handle as Prim public
+  using ( BufferMode
+        ; noBuffering
+        ; lineBuffering
+        ; blockBuffering
+        ; Handle
+        ; stdin
+        ; stdout
+        ; stderr
+        )
+
+------------------------------------------------------------------------
+-- Wrapping functions
+
+hSetBuffering : Handle → BufferMode → IO {a} ⊤
+hSetBuffering hdl bm = lift′ (Prim.hSetBuffering hdl bm)
+
+hGetBuffering : Handle → IO BufferMode
+hGetBuffering hdl = lift (Prim.hGetBuffering hdl)
+
+hFlush : Handle → IO {a} ⊤
+hFlush hdl = lift′ (Prim.hFlush hdl)
diff --git a/src/IO/Infinite.agda b/src/IO/Infinite.agda
index f2137cc4c6..90afd8989d 100644
--- a/src/IO/Infinite.agda
+++ b/src/IO/Infinite.agda
@@ -13,7 +13,7 @@ open import Agda.Builtin.String
 open import Data.Unit.Polymorphic.Base
 import Data.Unit.Base as Unit0
 open import IO.Base
-import IO.Primitive as Prim
+import IO.Primitive.Core as Prim
 import IO.Primitive.Infinite as Prim
 open import Level
 
diff --git a/src/IO/Primitive.agda b/src/IO/Primitive/Core.agda
similarity index 96%
rename from src/IO/Primitive.agda
rename to src/IO/Primitive/Core.agda
index 8014a2bd7c..6fd22a03fb 100644
--- a/src/IO/Primitive.agda
+++ b/src/IO/Primitive/Core.agda
@@ -8,7 +8,7 @@
 
 {-# OPTIONS --cubical-compatible #-}
 
-module IO.Primitive where
+module IO.Primitive.Core where
 
 open import Level using (Level)
 private
diff --git a/src/IO/Primitive/Handle.agda b/src/IO/Primitive/Handle.agda
new file mode 100644
index 0000000000..e9a27c9499
--- /dev/null
+++ b/src/IO/Primitive/Handle.agda
@@ -0,0 +1,61 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Primitive IO handles: simple bindings to Haskell types and functions
+------------------------------------------------------------------------
+
+-- NOTE: the contents of this module should be accessed via `IO`.
+
+{-# OPTIONS --cubical-compatible #-}
+
+module IO.Primitive.Handle where
+
+open import Data.Maybe.Base using (Maybe)
+open import Data.Nat.Base using (ℕ)
+
+data BufferMode : Set where
+  noBuffering lineBuffering : BufferMode
+  blockBuffering : Maybe ℕ → BufferMode
+{-# FOREIGN GHC import qualified System.IO as SIO #-}
+{-# FOREIGN GHC
+    data AgdaBufferMode
+      = NoBuffering
+      | LineBuffering
+      | BlockBuffering (Maybe Integer)
+    toBufferMode :: AgdaBufferMode -> SIO.BufferMode
+    toBufferMode x = case x of
+      NoBuffering       -> SIO.NoBuffering
+      LineBuffering     -> SIO.LineBuffering
+      BlockBuffering mi -> SIO.BlockBuffering (fromIntegral <$> mi)
+    fromBufferMode :: SIO.BufferMode -> AgdaBufferMode
+    fromBufferMode x = case x of
+      SIO.NoBuffering       -> NoBuffering
+      SIO.LineBuffering     -> LineBuffering
+      SIO.BlockBuffering mi -> BlockBuffering (fromIntegral <$> mi)
+#-}
+
+{-# COMPILE GHC BufferMode = data AgdaBufferMode
+                           ( NoBuffering
+                           | LineBuffering
+                           | BlockBuffering
+                           )
+#-}
+
+open import Data.Unit.Base using (⊤)
+open import IO.Primitive.Core using (IO)
+
+postulate
+  Handle : Set
+  stdin stdout stderr : Handle
+  hSetBuffering : Handle → BufferMode → IO ⊤
+  hGetBuffering : Handle → IO BufferMode
+  hFlush : Handle → IO ⊤
+
+{-# FOREIGN GHC import System.IO #-}
+{-# COMPILE GHC Handle = type Handle #-}
+{-# COMPILE GHC stdin = stdin #-}
+{-# COMPILE GHC stdout = stdout #-}
+{-# COMPILE GHC stderr = stderr #-}
+{-# COMPILE GHC hSetBuffering = \ h -> hSetBuffering h . toBufferMode #-}
+{-# COMPILE GHC hGetBuffering = fmap fromBufferMode . hGetBuffering #-}
+{-# COMPILE GHC hFlush = hFlush #-}

From 1bf539eb7d924bb2e325bd9d11948e289cdee051 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 16 Apr 2024 13:15:00 +0100
Subject: [PATCH 03/11] [ fix ] and test for the new IO primitives

---
 doc/README/IO.agda           | 24 ++++++++++++++++++++----
 src/IO/Primitive/Handle.agda | 30 +++++++++++++++---------------
 tests/system/io/Main.agda    | 17 +++++++++++++++++
 tests/system/io/expected     |  6 ++++++
 tests/system/io/input        |  6 ++++++
 tests/system/io/io.agda-lib  |  2 ++
 tests/system/io/run          |  5 +++++
 7 files changed, 71 insertions(+), 19 deletions(-)
 create mode 100644 tests/system/io/Main.agda
 create mode 100644 tests/system/io/expected
 create mode 100644 tests/system/io/input
 create mode 100644 tests/system/io/io.agda-lib
 create mode 100644 tests/system/io/run

diff --git a/doc/README/IO.agda b/doc/README/IO.agda
index 37553edd1d..bf913bbfdd 100644
--- a/doc/README/IO.agda
+++ b/doc/README/IO.agda
@@ -13,6 +13,7 @@ open import Data.Nat.Base
 open import Data.Nat.Show using (show)
 open import Data.String.Base using (String; _++_; lines)
 open import Data.Unit.Polymorphic
+open import Function.Base using (_$_)
 open import IO
 
 ------------------------------------------------------------------------
@@ -86,10 +87,21 @@ cat fp = do
   let ls = lines content
   List.mapM′ putStrLn ls
 
-open import Codata.Musical.Notation
-open import Codata.Musical.Colist
-open import Data.Bool
-open import Data.Unit.Polymorphic.Base
+------------------------------------------------------------------------
+-- TOP-LEVEL LOOP
+
+-- If you simply want to repeat the same action over and over again, you
+-- can use `forever` e.g. the following defines a REPL that echos whatever
+-- the user types
+
+echo : IO ⊤
+echo = do
+  hSetBuffering stdout noBuffering
+  forever $ do
+    putStr "echo< "
+    str ← getLine
+    putStrLn ("echo> " ++ str)
+
 
 ------------------------------------------------------------------------
 -- GUARDEDNESS
@@ -101,6 +113,10 @@ open import Data.Unit.Polymorphic.Base
 -- In this case you cannot use the convenient combinators that make `do`-notations
 -- and have to revert back to the underlying coinductive constructors.
 
+open import Codata.Musical.Notation
+open import Codata.Musical.Colist using (Colist; []; _∷_)
+open import Data.Bool
+open import Data.Unit.Polymorphic.Base
 
 -- Whether a colist is finite is semi decidable: just let the user wait until
 -- you reach the end!
diff --git a/src/IO/Primitive/Handle.agda b/src/IO/Primitive/Handle.agda
index e9a27c9499..f6b01a70be 100644
--- a/src/IO/Primitive/Handle.agda
+++ b/src/IO/Primitive/Handle.agda
@@ -16,28 +16,28 @@ open import Data.Nat.Base using (ℕ)
 data BufferMode : Set where
   noBuffering lineBuffering : BufferMode
   blockBuffering : Maybe ℕ → BufferMode
-{-# FOREIGN GHC import qualified System.IO as SIO #-}
+{-# FOREIGN GHC import System.IO #-}
 {-# FOREIGN GHC
     data AgdaBufferMode
-      = NoBuffering
-      | LineBuffering
-      | BlockBuffering (Maybe Integer)
-    toBufferMode :: AgdaBufferMode -> SIO.BufferMode
+      = AgdaNoBuffering
+      | AgdaLineBuffering
+      | AgdaBlockBuffering (Maybe Integer)
+    toBufferMode :: AgdaBufferMode -> BufferMode
     toBufferMode x = case x of
-      NoBuffering       -> SIO.NoBuffering
-      LineBuffering     -> SIO.LineBuffering
-      BlockBuffering mi -> SIO.BlockBuffering (fromIntegral <$> mi)
-    fromBufferMode :: SIO.BufferMode -> AgdaBufferMode
+      AgdaNoBuffering       -> NoBuffering
+      AgdaLineBuffering     -> LineBuffering
+      AgdaBlockBuffering mi -> BlockBuffering (fromIntegral <$> mi)
+    fromBufferMode :: BufferMode -> AgdaBufferMode
     fromBufferMode x = case x of
-      SIO.NoBuffering       -> NoBuffering
-      SIO.LineBuffering     -> LineBuffering
-      SIO.BlockBuffering mi -> BlockBuffering (fromIntegral <$> mi)
+      NoBuffering       -> AgdaNoBuffering
+      LineBuffering     -> AgdaLineBuffering
+      BlockBuffering mi -> AgdaBlockBuffering (fromIntegral <$> mi)
 #-}
 
 {-# COMPILE GHC BufferMode = data AgdaBufferMode
-                           ( NoBuffering
-                           | LineBuffering
-                           | BlockBuffering
+                           ( AgdaNoBuffering
+                           | AgdaLineBuffering
+                           | AgdaBlockBuffering
                            )
 #-}
 
diff --git a/tests/system/io/Main.agda b/tests/system/io/Main.agda
new file mode 100644
index 0000000000..c1cb619a80
--- /dev/null
+++ b/tests/system/io/Main.agda
@@ -0,0 +1,17 @@
+{-# OPTIONS --guardedness #-}
+
+module Main where
+
+open import Data.String.Base
+open import Function.Base using (_$_)
+open import IO
+open import System.Exit using (exitSuccess)
+
+main : Main
+main = run $ do
+  hSetBuffering stdout noBuffering
+  forever $ do
+    putStr "echo< "
+    "exit" ← getLine
+      where str → putStrLn ("echo> " ++ str)
+    exitSuccess
diff --git a/tests/system/io/expected b/tests/system/io/expected
new file mode 100644
index 0000000000..361d15957e
--- /dev/null
+++ b/tests/system/io/expected
@@ -0,0 +1,6 @@
+echo< echo> hello
+echo< echo> my
+echo< echo> name
+echo< echo> is
+echo< echo> Agda
+echo< 
\ No newline at end of file
diff --git a/tests/system/io/input b/tests/system/io/input
new file mode 100644
index 0000000000..bba046a9d5
--- /dev/null
+++ b/tests/system/io/input
@@ -0,0 +1,6 @@
+hello
+my
+name
+is
+Agda
+exit
\ No newline at end of file
diff --git a/tests/system/io/io.agda-lib b/tests/system/io/io.agda-lib
new file mode 100644
index 0000000000..74c23d5ccc
--- /dev/null
+++ b/tests/system/io/io.agda-lib
@@ -0,0 +1,2 @@
+name: io
+include: ../../../src/ .
diff --git a/tests/system/io/run b/tests/system/io/run
new file mode 100644
index 0000000000..ad42dc90b2
--- /dev/null
+++ b/tests/system/io/run
@@ -0,0 +1,5 @@
+$1 --compile-dir=../../_build -c Main.agda > log
+./../../_build/Main hello world < input > output
+
+rm ../../_build/Main
+rm ../../_build/MAlonzo/Code/Main*
\ No newline at end of file

From a8853358ea356ac4d72e95cf07c625f041e6f831 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 16 Apr 2024 13:16:38 +0100
Subject: [PATCH 04/11] [ fix ] compilation

---
 src/Foreign/Haskell/Coerce.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Foreign/Haskell/Coerce.agda b/src/Foreign/Haskell/Coerce.agda
index 3eb411c325..4383a1ac86 100644
--- a/src/Foreign/Haskell/Coerce.agda
+++ b/src/Foreign/Haskell/Coerce.agda
@@ -35,7 +35,7 @@ open import Level using (Level; _⊔_)
 open import Agda.Builtin.Nat
 open import Agda.Builtin.Int
 
-import IO.Primitive            as STD
+import IO.Primitive.Core       as STD
 import Data.List.Base          as STD
 import Data.List.NonEmpty.Base as STD
 import Data.Maybe.Base         as STD

From 1cf6f2ce0eb330f0805f225eae7afc6842e3a336 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 16 Apr 2024 13:22:08 +0100
Subject: [PATCH 05/11] [ fix ] more import fixing

---
 src/System/Clock/Primitive.agda          | 2 +-
 src/System/FilePath/Posix/Primitive.agda | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/System/Clock/Primitive.agda b/src/System/Clock/Primitive.agda
index 330b9e36c4..9e394af190 100644
--- a/src/System/Clock/Primitive.agda
+++ b/src/System/Clock/Primitive.agda
@@ -9,7 +9,7 @@
 module System.Clock.Primitive where
 
 open import Agda.Builtin.Nat using (Nat)
-open import IO.Primitive using (IO)
+open import IO.Primitive.Core using (IO)
 open import Foreign.Haskell using (Pair)
 
 data Clock : Set where
diff --git a/src/System/FilePath/Posix/Primitive.agda b/src/System/FilePath/Posix/Primitive.agda
index ed4cd56792..8226666ba6 100644
--- a/src/System/FilePath/Posix/Primitive.agda
+++ b/src/System/FilePath/Posix/Primitive.agda
@@ -14,7 +14,7 @@ open import Agda.Builtin.List using (List)
 open import Agda.Builtin.Maybe using (Maybe)
 open import Agda.Builtin.String using (String)
 open import Foreign.Haskell as FFI using (Pair; Either)
-open import IO.Primitive using (IO)
+open import IO.Primitive.Core using (IO)
 
 -- A filepath has a nature: it can be either relative or absolute.
 -- We postulate this nature rather than defining it as an inductive

From 513f5646ccaebe60e958bb887132bf0525b4f007 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 16 Apr 2024 13:24:13 +0100
Subject: [PATCH 06/11] [ done (?) ] with compilation fixes

---
 src/System/Environment/Primitive.agda | 2 +-
 src/System/Process/Primitive.agda     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/System/Environment/Primitive.agda b/src/System/Environment/Primitive.agda
index c1f8533e03..9408613641 100644
--- a/src/System/Environment/Primitive.agda
+++ b/src/System/Environment/Primitive.agda
@@ -14,7 +14,7 @@
 
 module System.Environment.Primitive where
 
-open import IO.Primitive using (IO)
+open import IO.Primitive.Core using (IO)
 open import Data.List.Base using (List)
 open import Data.Maybe.Base using (Maybe)
 open import Data.String.Base using (String)
diff --git a/src/System/Process/Primitive.agda b/src/System/Process/Primitive.agda
index aa2bdfcbf2..828a275433 100644
--- a/src/System/Process/Primitive.agda
+++ b/src/System/Process/Primitive.agda
@@ -13,7 +13,7 @@ open import Agda.Builtin.List
 open import Agda.Builtin.String
 open import Agda.Builtin.Unit
 open import Foreign.Haskell using (Pair)
-open import IO.Primitive using (IO)
+open import IO.Primitive.Core using (IO)
 open import System.Exit.Primitive using (ExitCode)
 
 postulate

From cd7200f2aea8c8e663de0afe73b280b0fa37d606 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 16 Apr 2024 13:31:09 +0100
Subject: [PATCH 07/11] [ test ] add test to runner

---
 tests/runtests.agda | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tests/runtests.agda b/tests/runtests.agda
index cf9af60245..f4ebea40e8 100644
--- a/tests/runtests.agda
+++ b/tests/runtests.agda
@@ -23,6 +23,7 @@ systemTests = mkTestPool "System modules"
   $ "ansi"
   ∷ "directory"
   ∷ "environment"
+  ∷ "io"
   ∷ []
 
 showTests : TestPool

From 1138237eb32f103570e841912dd1b5383ba57201 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 16 Apr 2024 13:42:00 +0100
Subject: [PATCH 08/11] [ doc ] explain the loop

---
 tests/system/io/Main.agda | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/tests/system/io/Main.agda b/tests/system/io/Main.agda
index c1cb619a80..4d2697ea27 100644
--- a/tests/system/io/Main.agda
+++ b/tests/system/io/Main.agda
@@ -3,15 +3,22 @@
 module Main where
 
 open import Data.String.Base
-open import Function.Base using (_$_)
+open import Function.Base using (_$_; case_of_)
 open import IO
 open import System.Exit using (exitSuccess)
 
 main : Main
 main = run $ do
+  -- Ensure no buffering so that the prompt "echo< "
+  -- gets outputed immediately
   hSetBuffering stdout noBuffering
   forever $ do
     putStr "echo< "
-    "exit" ← getLine
-      where str → putStrLn ("echo> " ++ str)
-    exitSuccess
+    -- Get a line from the user and immediately inspect it
+    -- If it's a magic "exit" keyword then we exit, otherwise
+    -- we print the echo'd message and let the `forever` action
+    -- continue
+    str ← getLine
+    case str of λ where
+      "exit" → exitSuccess
+      _ → putStrLn ("echo> " ++ str)

From e200afcff6a9690d3aab152c159ffdddb1ecdd97 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 16 Apr 2024 13:43:52 +0100
Subject: [PATCH 09/11] [ compat ] add deprecated stub

---
 GenerateEverything.hs |  1 +
 src/IO/Primitive.agda | 15 +++++++++++++++
 2 files changed, 16 insertions(+)
 create mode 100644 src/IO/Primitive.agda

diff --git a/GenerateEverything.hs b/GenerateEverything.hs
index 8f75b549bf..4facf17758 100644
--- a/GenerateEverything.hs
+++ b/GenerateEverything.hs
@@ -61,6 +61,7 @@ unsafeModules = map modToFile
   , "IO.Instances"
   , "IO.Effectful"
   , "IO.Finite"
+  , "IO.Primitive"
   , "IO.Primitive.Core"
   , "IO.Primitive.Handle"
   , "IO.Primitive.Infinite"
diff --git a/src/IO/Primitive.agda b/src/IO/Primitive.agda
new file mode 100644
index 0000000000..35460e2a36
--- /dev/null
+++ b/src/IO/Primitive.agda
@@ -0,0 +1,15 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use IO.Primitive.Core instead
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible #-}
+
+module IO.Primitive where
+
+open import IO.Primitive public
+
+{-# WARNING_ON_IMPORT
+"IO.Primitive was deprecated in v2.1. Use IO.Primitive.Core instead."
+#-}

From 9ae32c56abdf939e9b730580b12efb68cf78a6ca Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 16 Apr 2024 14:02:10 +0100
Subject: [PATCH 10/11] [ fix ] my silly mistake

---
 src/IO/Primitive.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/IO/Primitive.agda b/src/IO/Primitive.agda
index 35460e2a36..324a32b643 100644
--- a/src/IO/Primitive.agda
+++ b/src/IO/Primitive.agda
@@ -8,7 +8,7 @@
 
 module IO.Primitive where
 
-open import IO.Primitive public
+open import IO.Primitive.Core public
 
 {-# WARNING_ON_IMPORT
 "IO.Primitive was deprecated in v2.1. Use IO.Primitive.Core instead."

From 4f4bbe047e6d83ad89f71e9ea2043bea3a61ef6d Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Sun, 21 Apr 2024 11:36:45 +0100
Subject: [PATCH 11/11] [ doc ] list re-exports in CHANGELOG

---
 CHANGELOG.md | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index fc530458b7..07efe1d742 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -392,6 +392,21 @@ Additions to existing modules
   map : (Char → Char) → String → String
   ```
 
+* Re-exported new types and functions in `IO`:
+  ```agda
+  BufferMode : Set
+  noBuffering : BufferMode
+  lineBuffering : BufferMode
+  blockBuffering : Maybe ℕ → BufferMode
+  Handle : Set
+  stdin : Handle
+  stdout : Handle
+  stderr : Handle
+  hSetBuffering : Handle → BufferMode → IO ⊤
+  hGetBuffering : Handle → IO BufferMode
+  hFlush : Handle → IO ⊤
+  ```
+
 * Added new functions in `IO.Base`:
   ```agda
   whenInj₂ : E ⊎ A → (A → IO ⊤) → IO ⊤