max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
771 commits 1 branch 0 tags 5.3 GiB
Find a file
Soonho Kong a2a5a77a44 fix(memory): increase memory counters by the actual size of reallocated memory 
On OSX, we had a test failure on memory module. The problem was in
the realloc function (line 38):

    void * realloc(void * ptr, size_t sz) {
        size_t old_sz = malloc_size(ptr);
        g_global_memory.dec(old_sz);
        g_global_memory.inc(sz);
        g_thread_memory.dec(old_sz);
        g_thread_memory.inc(sz);
        void * r = realloc_core(ptr, sz);
        if (r || sz == 0)
            return r;
        else
            ...

The size of r could be bigger than sz. For instance,

    |ptr| = 40 but |r| = 48

In the current code, here we only increase counters by 40.
But later when we free it, we decrease them by 48, and this
caused the problem, underflow of an unsigned counter in
g_global_memory.
2013-09-26 00:33:56 -07:00
doc doc(commit_convention): add git commit_convention 2013-09-25 19:45:15 -07:00
examples/lean Fix typo 2013-09-05 19:18:55 -07:00
script Fix typo in script/dropbox_upload.py 2013-09-15 20:31:15 -07:00
src fix(memory): increase memory counters by the actual size of reallocated memory 2013-09-26 00:33:56 -07:00
tests/lean Simplify metavariable context. Now, we have only 'lift' and 'inst' instead of 'subst', 'lift' and 'lower' 2013-09-16 19:32:28 -07:00
.gitignore Add more tests 2013-08-31 18:46:18 -07:00
.travis.osx.yml Update .travis.osx.yml 2013-09-20 18:10:12 -07:00
.travis.windows.yml Update .travis.windows.yml 2013-09-20 13:41:26 -07:00
.travis.yml Update .travis.yml 2013-09-20 13:45:10 -07:00
LICENSE Add LICENSE file 2013-07-15 18:55:48 -07:00
README.md doc(commit_convention): add git commit_convention 2013-09-25 19:45:15 -07:00

README.md

Build Status Ubuntu 12.04 LTS 64bit, g++-4.8 | clang++-3.3

Build Status Mac OS X 10.8.2, g++-4.9

Build Status Windows, x86_64-w64-mingw32-g++-4.8.1

[Result of Build/UnitTest/Coverage/Dynamic Analysis]

About

Requirements

Installing required packages at

Build Instructions

Miscellaneous