Bazel builds

Stream: lean4

[Arjun Vedantham]

Is there any documentation on building/including Lean as a dependency within a Bazel build file? I previously found this repo, but I'm not sure if there's a better way of doing this now.

[Eric Wieser]

Open-sourcing some bazel rules to build Lean has been on my radar for a while, but I unfortunately haven't found time to do so.

[Arjun Vedantham]

I've been trying to set up a proof of concept using rules_foreign_cc: https://github.com/javathunderman/bazel-rules_foreign_cc-example

It's getting stuck while calling into CMake - specifically the log is returning:

CMake Error at /home/arjun/.cache/bazel/_bazel_arjun/0530fc5131259c17db36145ef68df50f/external/cmake-3.23.2-linux-x86_64/share/cmake-3.23/Modules/ExternalProject.cmake:2776 (message):
  No download info given for 'stage0' and its source directory:

   /home/arjun/.cache/bazel/_bazel_arjun/0530fc5131259c17db36145ef68df50f/sandbox/linux-sandbox/6/execroot/_main/lean4-4.25.1/stage0

  is not an existing non-empty directory.  Please specify one of:

   * SOURCE_DIR with an existing non-empty directory
   * DOWNLOAD_COMMAND
   * URL
   * GIT_REPOSITORY
   * SVN_REPOSITORY
   * HG_REPOSITORY
   * CVS_REPOSITORY and CVS_MODULE
Call Stack (most recent call first):
  /home/arjun/.cache/bazel/_bazel_arjun/0530fc5131259c17db36145ef68df50f/external/cmake-3.23.2-linux-x86_64/share/cmake-3.23/Modules/ExternalProject.cmake:3640 (_ep_add_download_command)
  CMakeLists.txt:90 (ExternalProject_add)

Maybe CMake is just getting invoked with the wrong options for the build? Not sure if it's failing because of that or something intrinsic to how Bazel invokes CMake with these rules.

[Arjun Vedantham]

I'm also wondering if it's Bazel blocking external network requests when that ExternalProject function gets invoked disregard, this should not be an issue anymore

[Arjun Vedantham]

Ah, never mind, it's just because I didn't include stage0 in the file group. Still not working but at least that error is resolved. :smiley: