platform transitions are breaking my Coq/OCaml builds

Skip to first unread message

Gregg Reynolds

Apr 7, 2021, 7:06:39 PMApr 7
to bazel-discuss
I've got rules_ocaml working pretty well; now I'm trying to add rules_coq.

It works fine (I can build and run coqtop) until I try to put the `coqc` compiler in a toolchain.  The problem then is that a bunch of stuff gets built twice, and in particular a lib that is a dependency of both the `coqc` compiler and the things the compiler builds.  I end up with a very OCamlish error when I try to use (toolchainized) `coqc` to compile a coq module, e.g.

`Error: Dynlink error: interface mismatch on Gramlib`

since the output of the OCaml compiler contains metadata indicating how it was built, so it can see two different builds of Gramlib were used and barfs.

I believe the problem is that some of my deps are built on the host platform and also on (presumably) the execution platform.  Example log msgs:

SUBCOMMAND: # //kernel:_GenOpcodeFiles [action 'native compiling ocaml_module: coq//kernel:_GenOpcodeFiles', configuration: dc73254f32901a6e5c6dd8ffc7359cbf52b48985034ebda0a6dc2cd38ac6974f, execution platform: @local_config_platform//:host]


SUBCOMMAND: # //kernel:_GenOpcodeFiles [action 'native compiling ocaml_module: coq//kernel:_GenOpcodeFiles [for host]', configuration: 66ba5f67c7587007cdeadf15db71cd651aafe5d6039fb4390272ae283c6b9db1, execution platform: @local_config_platform//:host]

Note the `[for host]` bit in the second example.

How can I get everything to build one way, without dups?  I've added `cfg="exec"` to all my executable attribs, and `exec_tools` to my genrules, but I'm still seeing lots of stuff built with `[for host]`.  What causes that?

Some of my actions use `ctx.actions.run_shell` to copy/rename source files. I don't see any way to set `cfg="exec"` for those; is that what is causing the transition to host platform?



John Cater

Apr 9, 2021, 3:50:44 PMApr 9
to Gregg Reynolds, bazel-discuss
Are you using the `incompatible_enable_toolchain_transition attribute` on your rules? See the proposal for details, but the short version is that legacy toolchains will use the host transition, but the rule that depends on a toolchain can set `incompatible_enable_toolchain_transition attribute`, and then toolchains that it depends on will use the toolchain transition and be in a special configuration. This is most likely what you're running into.

I am hoping to finish the migration on this in the next quarter, flip the defaults, and remove the attribute and flags entirely, at which point this won't be an issue for new toolchains.

You received this message because you are subscribed to the Google Groups "bazel-discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
To view this discussion on the web visit

Gregg Reynolds

Apr 17, 2021, 9:33:42 PMApr 17
to John Cater, bazel-discuss
Thanks, hoping to test this next week...
Reply all
Reply to author
0 new messages