Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions .github/workflows/build-template.yml
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,8 @@ jobs:
CCACHE_MAXSIZE: 400M
# squelch error message about missing nixpkgs channel
NIX_BUILD_SHELL: bash
# TODO
ASAN_OPTIONS: detect_leaks=0
LSAN_OPTIONS: max_leaks=10
# somehow MinGW clang64 (or cmake?) defaults to `g++` even though it doesn't exist
CXX: c++
Expand Down
22 changes: 13 additions & 9 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,8 @@ jobs:

# 0: PRs without special label
# 1: PRs with `merge-ci` label, merge queue checks, master commits
# 2: PRs with `release-ci` label, releases (incl. nightlies)
# 2: nightlies
# 2: PRs with `release-ci` label, full releases
- name: Set check level
id: set-level
# We do not use github.event.pull_request.labels.*.name here because
Expand All @@ -118,14 +119,16 @@ jobs:
check_level=0
fast=false

if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
if [[ -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
check_level=3
elif [[ -n "${{ steps.set-nightly.outputs.nightly }}" ]]; then
check_level=2
elif [[ "${{ github.event_name }}" != "pull_request" ]]; then
check_level=1
else
labels="$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }} --jq '.labels')"
if echo "$labels" | grep -q "release-ci"; then
check_level=2
check_level=3
elif echo "$labels" | grep -q "merge-ci"; then
check_level=1
fi
Expand Down Expand Up @@ -210,17 +213,18 @@ jobs:
"test": true,
"CMAKE_PRESET": "reldebug",
},
// TODO: suddenly started failing in CI
/*{
{
"name": "Linux fsanitize",
"os": "ubuntu-latest",
"enabled": level >= 2,
// do not have nightly release wait for this
"secondary": level <= 2,
"test": true,
// turn off custom allocator & symbolic functions to make LSAN do its magic
"CMAKE_PRESET": "sanitize",
// exclude seriously slow/problematic tests (laketests crash)
"CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
},*/
// exclude seriously slow/problematic tests (laketests crash, async_base_functions timeouts)
"CTEST_OPTIONS": "-E '(interactive|pkg|lake|bench)/|treemap|StackOverflow|async_base_functions'"
},
{
"name": "macOS",
"os": "macos-15-intel",
Expand Down Expand Up @@ -252,7 +256,7 @@ jobs:
},
{
"name": "Windows",
"os": large && (fast || level == 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
"os": large && (fast || level >= 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
"release": true,
"enabled": level >= 2,
"test": true,
Expand Down
2 changes: 1 addition & 1 deletion CMakePresets.json
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@
"SMALL_ALLOCATOR": "OFF",
"USE_MIMALLOC": "OFF",
"BSYMBOLIC": "OFF",
"LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000"
"LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000 ASAN_OPTIONS=detect_leaks=0"
},
"generator": "Unix Makefiles",
"binaryDir": "${sourceDir}/build/sanitize"
Expand Down
2 changes: 1 addition & 1 deletion src/runtime/compact.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -397,7 +397,7 @@ compacted_region::~compacted_region() {

inline object * compacted_region::fix_object_ptr(object * o) {
if (lean_is_scalar(o)) return o;
return reinterpret_cast<object*>(static_cast<char*>(m_begin) + (reinterpret_cast<size_t>(o) - reinterpret_cast<size_t>(m_base_addr)));
return reinterpret_cast<object*>(static_cast<char*>(m_begin) - reinterpret_cast<char*>(m_base_addr) + reinterpret_cast<ptrdiff_t>(o));
}

inline void compacted_region::move(size_t d) {
Expand Down
4 changes: 2 additions & 2 deletions src/runtime/io.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1499,8 +1499,8 @@ extern "C" LEAN_EXPORT uint8_t lean_st_ref_ptr_eq(b_obj_arg ref1, b_obj_arg ref2
return lean_to_ref(ref1) == lean_to_ref(ref2);
}

/* {α : Type} (act : BaseIO α) : α */
static obj_res lean_io_as_task_fn(obj_arg act) {
/* {α : Type} (act : BaseIO α) (_ : IO.RealWorld) : α */
static obj_res lean_io_as_task_fn(obj_arg act, obj_arg) {
object_ref r(apply_1(act, io_mk_world()));
return object_ref(r.raw(), true).steal();
}
Expand Down
Loading