Open shmish111 opened 5 years ago
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?
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.
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?
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
?
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.
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.
In bazel they can. And in a way, is the idea: with the BUILD init, it becomes an independent compile (and test!) unit
are they mandatory though? you wouldn't want a BUILD file in every subdirectory, https://github.com/edwinb/Blodwen/tree/master/src for example
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
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?
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?
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.
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
.
Hi, as an initial project I tried to convert Blodwen to bazel however I got
You can see my fork here https://github.com/shmish111/Blodwen