Skip to content

Commit 7087c07

Browse files
committed
refactor: split Init.System.IO for build parallelism
1 parent 30ea417 commit 7087c07

File tree

21 files changed

+47
-1250
lines changed

21 files changed

+47
-1250
lines changed

src/Init/Internal/Order/Basic.lean

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,11 +7,12 @@ module
77

88
prelude
99

10-
public import Init.System.IO -- for `MonoBind` instance
11-
import all Init.Control.Except -- for `MonoBind` instance
12-
import all Init.Control.StateRef -- for `MonoBind` instance
13-
import all Init.Control.Option -- for `MonoBind` instance
14-
import all Init.System.ST -- for `MonoBind` instance
10+
public import Init.System.IO
11+
public import Init.Control.StateRef
12+
public import Init.Control.Option
13+
import Init.Control.Except
14+
import all Init.Control.StateRef
15+
import all Init.System.ST
1516

1617
public section
1718

src/Init/Internal/Order/Lemmas.lean

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,11 @@ module
88

99
prelude
1010

11+
public import Init.Internal.Order.Basic
12+
public import Init.Control.Lawful.Basic
13+
public import Init.Data.List.Control
1114
import all Init.Data.List.Control
12-
import all Init.Data.Option.Basic
1315
import all Init.Data.Array.Basic
14-
public import Init.Internal.Order.Basic
1516

1617
public section
1718

src/Init/System.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,4 @@ public import Init.System.IO
1010
public import Init.System.Platform
1111
public import Init.System.Uri
1212
public import Init.System.Promise
13+
public import Init.System.Files

0 commit comments

Comments
 (0)