diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index be65ae1c88..3f91d0d7e8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -256,17 +256,18 @@ jobs: "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst", "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*" }, - { - "name": "Linux 32bit", - "os": "ubuntu-latest", - // Use 32bit on stage0 and stage1 to keep oleans compatible - "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DPKG_CONFIG_EXECUTABLE=/usr/bin/i386-linux-gnu-pkg-config", - "cmultilib": true, - "release": true, - "check-level": 2, - "cross": true, - "shell": "bash -euxo pipefail {0}" - } + // Started running out of memory building expensive modules, a 2GB heap is just not that much even before fragmentation + //{ + // "name": "Linux 32bit", + // "os": "ubuntu-latest", + // // Use 32bit on stage0 and stage1 to keep oleans compatible + // "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DPKG_CONFIG_EXECUTABLE=/usr/bin/i386-linux-gnu-pkg-config", + // "cmultilib": true, + // "release": true, + // "check-level": 2, + // "cross": true, + // "shell": "bash -euxo pipefail {0}" + //} // { // "name": "Web Assembly", // "os": "ubuntu-latest",