michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
1661 commits 3 branches 0 tags 28 MiB
Commit graph

101 commits

Author SHA1 Message Date
Leonardo de Moura
49698bd053 chore(library/all): remove unnecessary files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 13:37:25 -08:00
Leonardo de Moura
6633dff46f fix(build): githash generation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-29 14:41:28 -08:00
Leonardo de Moura
66178ae65a refactor(extra): move extra to builtin 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-28 22:06:11 -08:00
Leonardo de Moura
41c1010043 feat(frontends/lean/parser): make Import command use binary Lean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-28 19:20:04 -08:00
Leonardo de Moura
aee1c6d3f3 feat(kernel): export/import (.olean) binary files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-28 17:31:35 -08:00
Leonardo de Moura
99f9478d93 feat(build): cpack support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-25 16:18:51 -08:00
Leonardo de Moura
00e89190c2 refactor(library/cast): use .lean file instead of .cpp file to define casting library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 22:04:19 -08:00
Leonardo de Moura
84c984a435 feat(build): copy extra files to bin directory 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 21:00:32 -08:00
Leonardo de Moura
9bac91f5ef fix(frontends/lean): libreadline support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 18:57:15 -08:00
Soonho Kong
26afc6cf12 fix(cmake): fix problem of using LuaJit on OSX(64-bit) 
http://luajit.org/install.html

If you're building a 64 bit application on OSX which links directly or
indirectly against LuaJIT, you need to link your main executable with
these flags:

    -pagezero_size 10000 -image_base 100000000
 2013-12-13 19:52:40 -05:00
Leonardo de Moura
0cd8e3e76b feat(split-stack): add support for split-stacks (no more stackoverflows) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 22:30:54 -08:00
Leonardo de Moura
e3403492a5 feat(build): -D STATIC=ON option for building a static Lean executable 
On Linux, -D STATIC=ON does not work if MULTI_THREAD support is enabled.
If we search for "pthread static crash" we find other projects with the same problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 18:02:10 -08:00
Leonardo de Moura
e7ae749221 feat(boost): implement multi-threading support using Boost 
To use Boost instead of the standard library, we must use the cmake option
    -D BOOST=ON

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 17:24:32 -08:00
Leonardo de Moura
8f2fe273ea refactor(*): isolate std::thread dependency 
This commit allows us to build Lean without the pthread dependency.
It is also useful if we want to implement multi-threading on top of Boost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 15:20:26 -08:00
Leonardo de Moura
1e5518002b feat(shell/lean): add git hash to executable 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-04 11:23:15 -08:00
Leonardo de Moura
74dfdd02de feat(util): add primitives for checking the amount of available stack space 
Recursive functions that may go very deep should invoke the function check_stack. It throws an exception if the amount of stack space is limited.

The function check_system() is syntax sugar for
    check_interrupted();
    check_stack();

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 17:19:27 -08:00
Leonardo de Moura
feca9dbdf8 refactor(bindings/lua): move to frontends/lua 
Lua API is an integral part of Lean. It does *not* have the same status
of external APIs (e.g., Python) we will add in the future.

We will reserve the directory bindings for external APIs for using Lean
as a library.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 19:30:07 -08:00
Leonardo de Moura
956f203a55 refactor(bindings/lua): move Lua bindings to the file associated with them 
The directory bindings/lua was getting too big and had too many dependencies.
Moreover, it was getting too painful to edit/maintain two different places.
Now, the bindings for module X are in the directory that defines X.
For example, the bindings for util/name.cpp are located at util/name.cpp.

The only exception is the kernel. We do not want to inflate the kernel
with Lua bindings. The bindings for the kernel classes are located
at bindings/kernel_bindings.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 19:15:56 -08:00
Leonardo de Moura
3a6aa2dc75 feat(library/tactic): add tactic framework APIs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-20 17:19:05 -08:00
Leonardo de Moura
a98fdd9be6 refactor(shell): combine lean and leanlua executables in a single executable 
The main motivation is to allow users to configure/extend Lean using .lua files before loading the actual .lean files.
Example:
        ./lean extension1.lua extension2.lua file.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 16:48:21 -08:00
Leonardo de Moura
4d1d3d7cc7 fix(build): cygwin also needs the LEAN_WINDOWS flag 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 12:40:02 -08:00
Leonardo de Moura
e0c23e5984 fix(kernel/environment): compilation problem on Windows 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 09:52:47 -08:00
Leonardo de Moura
19533c811b feat(library/script_evaluator): add abstract class that exposes only the API needed by frontend objects 
The main motivation is to break the remove the dependency frontends/lean <-- bindings/lua.
This dependency is undesirable because we want to expose the frontends/lean parser and pretty printer objects at bindings/lua.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 12:13:09 -08:00
Leonardo de Moura
6e0fc0ca9b chore(build): include dl.so when compiling on Linux 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 18:44:28 -08:00
Leonardo de Moura
0a6f622aec chore(build): remove CheckLuaObjlen, it is easier to check the Lua version 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 12:58:22 -08:00
Leonardo de Moura
c8b0c10c88 refactor(lua): make Lua a required (non-optional) package 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-08 10:56:29 -08:00
Leonardo de Moura
a10aa0880f fix(build): add CheckLuaObjlen.cc test, not every Lua version has the function lua_objlen 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-08 08:26:04 -08:00
Leonardo de Moura
db8b16641c chore(build): check if the Lua installed in the system supports lua_newstate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-07 21:54:57 -08:00
Leonardo de Moura
a9b2be0b9c feat(frontends/lean): add support for embedded Lua scripts in Lean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-07 13:56:04 -08:00
Soonho Kong
c5fd828a71 chore(cmake): switch the ordering between gmp and mpfr 2013-11-05 19:31:10 -05:00
Leonardo de Moura
9884c056ce feat(lua): allow Lean to be compiled with Lua 5.1 and LuaJit 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-03 12:40:44 -08:00
Soonho Kong
a9d55bf036 fix(lua): use updated FindLua and check version 5.2 2013-11-03 13:24:46 -05:00
Soonho Kong
0d0d0cd533 chore(cmake): add gmp/mpfr include paths to cmakelists.txt 2013-11-03 13:00:42 -05:00
Leonardo de Moura
dbf2d56c77 feat(lua/name): expose hierarchical names in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-02 20:49:42 -07:00
Leonardo de Moura
1b9cf816c4 fix(lua): mark package as optional 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-02 11:43:23 -07:00
Leonardo de Moura
ac08e244a6 feat(lua): add Lua support to build 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-02 11:16:30 -07:00
Leonardo de Moura
c3c66b6c90 feat(make): add THREAD_SAFE build option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 11:50:35 -07:00
Leonardo de Moura
b1b49e86e7 test(elaborator): add simple test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
1548ffabb1 feat(elaborator): add new elaborator interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
93d4466d06 refactor(interval): move interval unit tests to tests/util/interval 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-21 18:17:34 -07:00
Soonho Kong
0065d69e0a chore(build): put --coverage CXX_FLAGS for TESTCOV build 2013-09-27 10:24:31 -07:00
Soonho Kong
a05b6b476e fix(testcov): install lcov and include testcov only when it's on 2013-09-26 22:24:24 -07:00
Soonho Kong
5e5087b0a3 chore(testcov): add compile target "cov" to run code-coverage locally 
- need to run cmake with "-DTESTCOV=ON" and "-DCMAKE_BUILD_TYPE=Debug"
 - type "make/ninja cov"
 - open "coverage/index.html" to check the code coverage
 2013-09-26 20:28:52 -07:00
Soonho Kong
a50f5f92b8 Rename 'rewrite' to 'Rewriter', change type of rewriter::operator() 2013-09-25 15:38:16 -07:00
Soonho Kong
f89ededddc Add rewrite and first-order pattern matching skeletal 2013-09-24 01:19:03 -07:00
Soonho Kong
48318511f2 Undo the previous change which caused compile-errors 2013-09-21 00:04:23 -07:00
Soonho Kong
66ba1a20d7 Suppress cmake warning for OSX build 2013-09-20 23:49:09 -07:00
Soonho Kong
9226c46358 Add support OSX's malloc_size 2013-09-20 17:48:55 -07:00
Leonardo de Moura
3971265bcb Add support for _msize 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-20 14:14:57 -07:00
Leonardo de Moura
dae654e4c6 Track memory usage. Add new CMake option TRACK_MEMORY_USAGE (It is ON by default). 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-20 12:32:12 -07:00