[ refactor ] Clean up the dependency graph

[gallais]

Following agda/agda#5231 (comment) I investigated using Agda's --dependency-graph
option and managed to reorganise the dependency graph quite a bit.

We now only need to compile 34 library modules (of which 12 are Builtin modules!)
to run hello world.

Note: I still need to document the breaking changes in the CHANGELOG

[jmchapman]

Nice work!

It would be nice to get rid of the musical codata stuff from IO too and cut down the builtin modules. Perhaps in a later PR. Correct me if I am wrong but I think supporting finite strings only would cover quite a lot of use cases.

This is roughly all the code that's actually needed to run 'hello world' after all:

% cat Hello.agda           
module Hello where

open import Agda.Builtin.IO
open import Agda.Builtin.Unit
open import Agda.Builtin.String

postulate putStrLn : String → IO ⊤
{-# FOREIGN GHC import qualified Data.Text.IO as T #-}
{-# COMPILE GHC putStrLn = T.putStrLn #-}

main : IO ⊤
main = putStrLn "hello world"

% agda --compile Hello.agda
Compiling Agda.Primitive in /nix/store/6rd59zf2v561w8rfshjnkpgpwrv2ic4g-Agda-2.6.1.2-data/share/ghc-8.10.2/x86_64-osx-ghc-8.10.2/Agda-2.6.1.2/lib/prim/Agda/Primitive.agdai to MAlonzo/Code/Agda/Primitive.hs
Compiling Agda.Builtin.Unit in /nix/store/6rd59zf2v561w8rfshjnkpgpwrv2ic4g-Agda-2.6.1.2-data/share/ghc-8.10.2/x86_64-osx-ghc-8.10.2/Agda-2.6.1.2/lib/prim/Agda/Builtin/Unit.agdai to MAlonzo/Code/Agda/Builtin/Unit.hs
Compiling Agda.Builtin.IO in /nix/store/6rd59zf2v561w8rfshjnkpgpwrv2ic4g-Agda-2.6.1.2-data/share/ghc-8.10.2/x86_64-osx-ghc-8.10.2/Agda-2.6.1.2/lib/prim/Agda/Builtin/IO.agdai to MAlonzo/Code/Agda/Builtin/IO.hs
Compiling Agda.Builtin.Bool in /nix/store/6rd59zf2v561w8rfshjnkpgpwrv2ic4g-Agda-2.6.1.2-data/share/ghc-8.10.2/x86_64-osx-ghc-8.10.2/Agda-2.6.1.2/lib/prim/Agda/Builtin/Bool.agdai to MAlonzo/Code/Agda/Builtin/Bool.hs
Compiling Agda.Builtin.Nat in /nix/store/6rd59zf2v561w8rfshjnkpgpwrv2ic4g-Agda-2.6.1.2-data/share/ghc-8.10.2/x86_64-osx-ghc-8.10.2/Agda-2.6.1.2/lib/prim/Agda/Builtin/Nat.agdai to MAlonzo/Code/Agda/Builtin/Nat.hs
Compiling Agda.Builtin.Char in /nix/store/6rd59zf2v561w8rfshjnkpgpwrv2ic4g-Agda-2.6.1.2-data/share/ghc-8.10.2/x86_64-osx-ghc-8.10.2/Agda-2.6.1.2/lib/prim/Agda/Builtin/Char.agdai to MAlonzo/Code/Agda/Builtin/Char.hs
Compiling Agda.Builtin.List in /nix/store/6rd59zf2v561w8rfshjnkpgpwrv2ic4g-Agda-2.6.1.2-data/share/ghc-8.10.2/x86_64-osx-ghc-8.10.2/Agda-2.6.1.2/lib/prim/Agda/Builtin/List.agdai to MAlonzo/Code/Agda/Builtin/List.hs
Compiling Agda.Builtin.String in /nix/store/6rd59zf2v561w8rfshjnkpgpwrv2ic4g-Agda-2.6.1.2-data/share/ghc-8.10.2/x86_64-osx-ghc-8.10.2/Agda-2.6.1.2/lib/prim/Agda/Builtin/String.agdai to MAlonzo/Code/Agda/Builtin/String.hs
Compiling Hello in Hello.agdai to MAlonzo/Code/Hello.hs
Calling: /nix/store/drw76lkmh4l8mm8q1navr7r8bx4ygbvw-ghc-8.10.2-with-packages/bin/ghc -O -o Hello -Werror -i. -main-is MAlonzo.Code.Hello MAlonzo/Code/Hello.hs --make -fwarn-incomplete-patterns -fno-warn-overlapping-patterns
[1 of 5] Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
[2 of 5] Compiling MAlonzo.Code.Agda.Builtin.Unit ( MAlonzo/Code/Agda/Builtin/Unit.hs, MAlonzo/Code/Agda/Builtin/Unit.o )
[3 of 5] Compiling MAlonzo.Code.Agda.Builtin.String ( MAlonzo/Code/Agda/Builtin/String.hs, MAlonzo/Code/Agda/Builtin/String.o )
[4 of 5] Compiling MAlonzo.Code.Agda.Builtin.IO ( MAlonzo/Code/Agda/Builtin/IO.hs, MAlonzo/Code/Agda/Builtin/IO.o )
[5 of 5] Compiling MAlonzo.Code.Hello ( MAlonzo/Code/Hello.hs, MAlonzo/Code/Hello.o )
Linking Hello ...
% ./Hello                  
hello world

Even with this it pulls in more Builtin modules than are ideal.

[JacquesCarette]

This is really nice. Hopefully we can get better tools to continue analyzing the dependency graph and keep cleaning it up like this. Once this term-from-hell is over, I'm hoping to dig back in to such things.

[gallais]

Hopefully we can get better tools to continue analyzing the dependency graph
and keep cleaning it up like this.

Yep. I had to start from Data.Char.Base because the full IO dependency graph
was too big for dot to handle. It would be nice to have a tool spitting out some
of the graph's properties (a collection of the longest paths for instance) rather
than computing a graphical representation of it!

[MatthewDaggitt]

Looks great! A plethora of minor comments though...

[gallais]

Latest state of affairs: compiling IO.Finite pulls only 11 modules
(IO is still at 34 modules).

Of course you'll have to write your "hello world" using Agda.Builtin.String to keep
such a small dependency graph. As soon as you pull Data.String.Base, you'll get
the Base for Char, List, Maybe, These, etc.

[jmchapman]

IO.Finite ❤️