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.
10552 commits 1 branch 0 tags 5.3 GiB
Find a file
Leonardo de Moura 20d0ea7925 fix(library/module_mgr): invalid memory read 
@gebner I was getting the following error with valgrind:

==9902== Invalid read of size 1
==9902==    at 0xAD209B: lean::module_mgr::mark_out_of_date(std::string const&, lean::buffer<std::string, 16u>&) (module_mgr.cpp:24)
==9902==    by 0xAD3EF5: lean::module_mgr::invalidate(std::string const&) (module_mgr.cpp:286)
==9902==    by 0x986A84: lean::server::handle_sync(nlohmann::basic_json<std::map, std::vector, std::string, bool, long, unsigned long, double, std::allocator> const&) (server.cpp:141)
==9902==    by 0x986603: lean::server::handle_request(nlohmann::basic_json<std::map, std::vector, std::string, bool, long, unsigned long, double, std::allocator> const&) (server.cpp:105)
==9902==    by 0x986313: lean::server::run() (server.cpp:90)
==9902==    by 0x975E98: main (lean.cpp:383)
==9902==  Address 0x0 is not stack'd, malloc'd or (recently) free'd
==9902==
==9902==
==9902== Process terminating with default action of signal 11 (SIGSEGV)
==9902==  Access not within mapped region at address 0x0
==9902==    at 0xAD209B: lean::module_mgr::mark_out_of_date(std::string const&, lean::buffer<std::string, 16u>&) (module_mgr.cpp:24)
==9902==    by 0xAD3EF5: lean::module_mgr::invalidate(std::string const&) (module_mgr.cpp:286)
==9902==    by 0x986A84: lean::server::handle_sync(nlohmann::basic_json<std::map, std::vector, std::string, bool, long, unsigned long, double, std::allocator> const&) (server.cpp:141)
==9902==    by 0x986603: lean::server::handle_request(nlohmann::basic_json<std::map, std::vector, std::string, bool, long, unsigned long, double, std::allocator> const&) (server.cpp:105)
==9902==    by 0x986313: lean::server::run() (server.cpp:90)
==9902==    by 0x975E98: main (lean.cpp:383)
2016-11-30 09:50:08 -08:00
bin chore(bin,src,src/emacs): delete linja 2016-11-29 14:14:42 -08:00
doc chore(CMakeLists): make python dependency optional 2016-11-30 11:27:02 -05:00
extras feat(kernel/declaration,*): all theorems are delayed, and are revealed on delta-reduction 2016-11-29 11:12:43 -08:00
images chore(CMakeLists.txt): move Lean logo to make sure we can test leanemacs without installing Lean 2015-01-31 17:38:49 -08:00
library feat(library/vm/vm_task): expose task_result objects to VM 2016-11-29 11:12:43 -08:00
old_library chore(old_library): save old library 2016-09-21 11:43:28 -07:00
script feat(shell/server): first version of the compile server API 2016-10-13 18:49:10 -07:00
src fix(library/module_mgr): invalid memory read 2016-11-30 09:50:08 -08:00
tests/lean chore(tests): update tests to new position information for by tac 2016-11-30 11:27:02 -05:00
tmp feat(library): add debugger 2016-11-16 14:53:13 -08:00
.gitignore feat(util/file_lock): add support for Windows 2015-12-14 10:07:26 -08:00
.travis.osx.yml fix(.travis.osx.yml): explicitly turn on multi-thread support 2015-05-06 02:37:31 -04:00
.travis.windows.yml fix(.travis.windows.yml): use cmake-2.8.11.2 2015-05-05 17:17:37 -04:00
.travis.yml fix(.travis.yml): disable broken parts 2016-09-24 17:15:44 -07:00
LICENSE Add LICENSE file 2013-07-15 18:55:48 -07:00
README.md doc(*): remove Lua from the list of required packages 2016-11-04 14:05:05 -07:00

README.md

logo

LicenseWindowsUbuntuOS XBuilds/Tests

Issue Stats Issue Stats

About

Requirements

Installing required packages at

Windows

Linux

OS X

Build Instructions

Miscellaneous