can't build Blodwen

[shmish111]

Hi, as an initial project I tried to convert Blodwen to bazel however I got

[nix-shell:~/personal/Blodwen]$ bazel build //:blodwen
DEBUG: /private/var/tmp/_bazel_davidsmith/97b9387c2678536cdd95804d66b9af62/external/bazel_tools/tools/osx/xcode_configure.bzl:87:9: Invoking xcodebuild failed, developer dir: /Users/davidsmith/Downloads/Xcode.app/Contents/Developer ,return code 256, stderr: Process terminated by signal 6, stdout:
INFO: Analysed target //:blodwen (0 packages loaded).
INFO: Found 1 target...
ERROR: /Users/davidsmith/personal/Blodwen/BUILD.bazel:7:1: error executing shell command: '/nix/store/96378wn4nd0lpbaz4npf8ifbxg266jh5-bash/bin/bash -c export THE_PATH=`pwd` && cd "." && cp "$THE_PATH/bazel-out/darwin-fastbuild/bin/blodwen.ipkg" "blodwen.ipkg" && HOME=`pwd` $THE_PATH/baz...' failed (Exit 1)

Uncaught error: user error (/private/var/tmp/_bazel_davidsmith/97b9387c2678536cdd95804d66b9af62/sandbox/darwin-sandbox/1/execroot/__main__/blodwen.ipkg:3:11:
  |
3 | modules =
  |           ^
unexpected end of input
)
ERROR: Idris execution has faild, with exit code 1
Target //:blodwen failed to build
Use --verbose_failures to see the command lines of failed build steps.
INFO: Elapsed time: 0.886s, Critical Path: 0.75s
INFO: 0 processes.
FAILED: Build did NOT complete successfully

You can see my fork here /~https://github.com/shmish111/Blodwen

[shmish111]

OK, so I've progressed a bit but I realise that the layout of the Blodwen project doesn't seem to work properly with rules_idris. From looking at the generated ipkg file I can see that it thinks modules should be prefixed with src, e.g. src.Compiler.Common for a module in src/Compiler.Common even if BUILD.bazel is inside src/.

I moved WORKSPACE into the src directory (which seems very wrong) and got much further.

./Core/Evaluate.idr:18:15-31:
   |
18 |        Nil  : LocalEnv outer []
   |               ~~~~~~~~~~~~~~~~~
When checking type of Core.Evaluate.Nil:
Can't disambiguate name: Core.Evaluate.LocalEnv, Core.TT.LocalEnv

./Core/Evaluate.idr:23:20-25:56:
   |
23 |        MkClosure : LocalEnv outer vars ->
   |                    ~~~~~~~~~~~~~~~~~~~~~~~ ...
When checking type of MkClosure:
Can't disambiguate name: Core.Evaluate.LocalEnv, Core.TT.LocalEnv

./Core/Evaluate.idr:28:11:
   |
28 | toClosure : Env Term outer -> Term outer -> Closure outer
   |           ^
When checking type of Core.Evaluate.toClosure:
Can't disambiguate name: Core.Evaluate.Closure, Core.TT.Closure

I'm guessing but I think it's because there are really 2 projects in here, blodwen and ttimp which presumably have some parts in common. So I next tried to temporarily get rid of Core/TT.idr and came across the next error, one I think has come up in other rules implementations, Argument list too long. As it's a biggish project I think this is trying to add all the files in the command. Something like https://stackoverflow.com/questions/50312539/bazel-build-gives-argument-list-too-long-error which I'm going to have a look at now.

WRT the problem of Core.TT, is this something that will be inherently difficult for bazel to deal with? In fact, if blodwen and ttimp share some files it seems like those should be in a separate package anyway and all the source files should be separate so perhaps this part is a blodwen issue?

[shmish111]

OK, so the issue here is that Blodwen has multiple projects in one source directory, it appears that ./Core/Evaluate.idr isn't actually used anywhere. I managed to get things working by changing the ideris_library rule srcs to be the exact files I need only, rather than a glob of everything.

Unfortunately I still have the problem of rules_idris thinking that the module name should be src.Something.Something rather than Something.Something. This is resolved if the WORKSPACE file is placed in the src directory rather than the project root.

[marcesquerra]

Yes, right now idris rules tries to follow the idea that bazel can have nested modules that are, at the same time, bazel rules.

That is, if I have the modules foo.Foo and foo.bar.Bar, the file structure would be something like this:

|____foo
| |____Foo.idr
| |____bar
| | |____Bar.idr
| | |____BUILD
| |____BUILD
|____WORKSPACE

For this reason, all the directories are, right now, meaningful. I might, if you think it useful, add an optional remove-prefix field in the different idris rules?

[shmish111]

I was thinking that the language should be the same as an ipkgs file, so sourcedir would be an attr that you can add to the rule.

Additionally, why do we need to use the ip tool? couldn't we just generate an ipkg file based on modules the user requires and then use idris --build name.ipkg?

[marcesquerra]

I was thinking that the language should be the same as an ipkgs file, so sourcedir would be an attr that you can add to the rule.

This would work in a top level module all right, but would not be so clear on a sub module. Imagine this:

.
|____src
| |____sub
| | |____Sub.idr  // This is module sub.Sub
| | |____BUILD
| |____Main.idr   // This is module Main
| |____BUILD

In this example there are two modules Main and sub.Sub. But idris_rules is going to think they are src.Main and src.sub.Sub respectively. If we make something like the sourcedir approach, to achieve our goal we would need something like this:

|____src
| |____sub
| | |____sub
| | | |____Sub.idr
| | |____BUILD // Specifies sourcedir = . (so that Sub.idr is found below the inner sub)
| |____Main.idr
|____BUILD // Specifies sourcedir = src

I find this far from ideal. My solution is to add this strip_prefix option (that seems to be a known pattern in bazel)

With the strip prefix we get this:

.
|____src
| |____sub
| | |____Sub.idr  // This is module sub.Sub
| | |____BUILD    // Sets `strip_prefix = "src"`
| |____Main.idr   // This is module Main
| |____BUILD      // Sets `strip_prefix = "src"`

With this approach, idris_rules and bazel are going to regard the modules as Main and sub.Sub. Which is what we wanted from the very begining.

Additionally, why do we need to use the ip tool? couldn't we just generate an ipkg file based on modules the user requires and then use idris --build name.ipkg?

In cases where the whole project is in a single "idris_library" or a single "idris_binary", you would be absolutely right and, in fact, that was my intention initially. But bazel has a convoluted way to move stuff from the output of one rule to the input of another rule.

The ip tool basically generates a zip file with everything one module have (minus dependencies) and makes it a single thing to move. In fact, this zip file contains all the ibc files of that module too, ensuring things get compiled only once.

[shmish111]

but a submodule shouldn't have a BUILD file in it should it? Currently it seems to consider src.Main and src.sub.Sub as well.

[marcesquerra]

In bazel they can. And in a way, is the idea: with the BUILD init, it becomes an independent compile (and test!) unit

[shmish111]

are they mandatory though? you wouldn't want a BUILD file in every subdirectory, /~https://github.com/edwinb/Blodwen/tree/master/src for example

[marcesquerra]

No, they are not mandatory. But if you take a look at bazel, you'll see that the more you split the code this way, the more you benefit from bazel.

The idea is that bazel is very good keeping the relationship betwwen each 'rule' to ensure to only build/test whatever has been affected by a change

[shmish111]

ok so given all this, can we add strip_prefix.

In the case of Blodwen there are 2 packages within the src directory and in addition there are even some files that don't compile (like ./Core/Evaluate.idr) but since they are not used anywhere idris has no issue. If in the worst case you just explicitly add all the files you need to srcs then this would work, right?

[shmish111]

IIUC an idris_library will produce an ipz file and that will be what is cached by bazel? So in your example, the sub directory would produce an ipz file (that would be cached) and the src directory would produce another ipz file that would also be cached. Is rules_idris (or ip I think) clever enough to remove the sub stuff from the ipz of the src package?

[shmish111]

Ok, I had a go with strip_prefix and discovered that not only does this prefix need to be stripped off the module names but the idrisPackager command also needs to be run from within this directory (in this case src). I'm not sure how that would work with modules in sub-directories then.

[shmish111]

This also needs to be the same for idris_binary and in addition there should be the option to say which file is the Main module in idris_binary.