- land `HelloWorld.agda` and `TrivialBackend.hs` in files - replace `runCommand` by `stdenvNoCC.mkDerivation` - refactor asserts