Soonho Kong
5e551db9be
chore(CMakeLists.txt): use $PYTHON_EXECUTABLE instead of "python"
2014-10-02 17:25:13 -07:00
Leonardo de Moura
1a1e9a2340
feat(build): add 'CONSERVE_MEMORY' cmake option
...
When CONSERVE_MEMORY=ON and gcc is being used, we provide additional
command line options that will minimize the amount of memory used by gcc
when compiling Lean.
This is an attempt to fix the "out-of-memory" failures when building
Lean at Travis.
2014-09-29 12:44:29 -07:00
Leonardo de Moura
8143b51c7e
feat(build): add 'CROSS_COMPILE' cmake option
...
When CROSS_COMPILE=ON, the Lean standard library will not be compiled.
2014-09-26 09:26:40 -07:00
Leonardo de Moura
480bc639ea
feat(build): add IGNORE_SORRY cmake option
...
It allows us to perform nightly builds and avoid distracting warning
messages on CDASH.
2014-09-26 08:55:54 -07:00
Leonardo de Moura
358074ae3d
refactor(kernel/record): remove kernel extension for records, we will
...
implement it outside of the kernel on top of the inductive datatypes
2014-09-24 10:12:28 -07:00
Leonardo de Moura
b1ee888aae
refactor(*): start move to explicit initialization/finalization,
...
explicitly initialize/finalize options
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-22 10:41:07 -07:00
Leonardo de Moura
10a4148adb
fix(tests): make sure tests can be executed on Windows msys2 shell
2014-09-20 15:51:24 -07:00
Leonardo de Moura
8867f47dd6
feat(build): build standard library when building on Windows
2014-09-20 10:52:59 -07:00
Leonardo de Moura
2bde3f55d5
feat(shell): include build type when printing version
2014-09-18 22:40:05 -07:00
Leonardo de Moura
19148af7ae
feat(build): do not display WARNING message when tcmalloc is not found
2014-09-17 15:23:10 -07:00
Leonardo de Moura
26918022d8
feat(build): use Release when compilation mode is not specified
2014-09-17 15:23:10 -07:00
Soonho Kong
765d9b032f
feat(src/cmake/modules/CleanOlean.cmake): add CleanOlean.cmake
...
Instead of using 'find -delete', use CMAKE's FILE GLOB_RECURSE and FILE
REMOVE to implement clean-olean.
Related issue: #166
2014-09-14 01:40:21 -07:00
Leonardo de Moura
d3ec5ccac1
refactor(library/declaration_index): store declarations in a map
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 07:42:18 -07:00
Leonardo de Moura
3f50fd3ddd
feat(build): invoke linja from lean build
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 12:15:07 -07:00
Leonardo de Moura
11711a2409
fix(util/rb_tree): do not use thread local storage in template when compiling on OSX with clang++ without Boost
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 12:46:24 -07:00
Leonardo de Moura
dbaf81e16d
refactor(library): remove unnecessary 'standard' subdirectory
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 18:08:09 -07:00
Leonardo de Moura
9588336c15
refactor(kernel/type_checker): remove "global" constraint buffer from type_checker, and use constraint_seq instead
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:19 -07:00
Soonho Kong
74b665ea06
fix(CMakeLists.txt): use bin/lean to build library
...
close #49
2014-08-14 18:21:58 -07:00
Leonardo de Moura
29a7d6d05a
fix(library/hott): remove hott_lib from build, it will be integrated in the standard library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 18:05:48 -07:00
Leonardo de Moura
f319d084d4
feat(library/Makefile.common): use new --cache/-c option at Makefile.common
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-10 11:20:08 -07:00
Leonardo de Moura
53c7124c2b
fix(util/realpath): rename realpath to lrealpath
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 14:42:44 -07:00
Leonardo de Moura
bc4cef9ecb
feat(build): clean-olean target deletes .olean and .d files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 14:01:13 -07:00
Leonardo de Moura
d27c85e30c
fix(library/Makefile.common): avoid error message when .d files do not exist
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-01 10:11:01 -07:00
Leonardo de Moura
8834563a7f
feat(build): add 'clean-olean' custom-target
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-30 15:12:37 -07:00
Leonardo de Moura
b4700e4eed
chore(build): eliminate artificial dependencies
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 18:25:57 -07:00
Leonardo de Moura
f8eba36b0a
fix(build): set LEAN_PATH before make standard and hott libraries
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 10:06:39 -07:00
Leonardo de Moura
33c77afc29
feat(frontends/lean/structure): add 'structure' command skeleton
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 19:59:38 -07:00
Leonardo de Moura
e81d96ffc1
feat(build): add build option for jemalloc
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 13:44:47 -07:00
Leonardo de Moura
725f370e59
fix(build): number of core detection on OSX
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-21 20:07:11 -07:00
Leonardo de Moura
9c499e723f
perf(build): use make -j option when invoking external makefile for compiling Lean libraries
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-20 19:38:46 -07:00
Soonho Kong
5118ee7a83
chore(CMakeLists.txt): mark gmp and mpfr as required packages
2014-07-18 08:29:51 -04:00
Leonardo de Moura
f7317a7139
feat(build): compile HoTT library when building
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-15 21:56:36 +01:00
Leonardo de Moura
e445515f2b
refactor(kernel): move standard and hott kernel instantiations to library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 10:31:27 -07:00
Leonardo de Moura
e59889d84f
fix(build): do not build libraries when cross compiling
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 10:00:08 -07:00
Leonardo de Moura
5a7e198583
feat(build): add Makefile for libraries
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-28 18:41:53 -07:00
Leonardo de Moura
f1d8d8dcf9
chore(library/tactic): update goal objects
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-27 07:00:12 -07:00
Leonardo de Moura
611f29a954
chore(library/elaborator): remove dead code
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 16:35:00 -07:00
Leonardo de Moura
a04af30d85
fix(CMakeLists): remove -pthread flag when compiling using Boost on OSX
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 13:21:00 -07:00
Leonardo de Moura
d9794d8ea4
feat(CMakeLists): hide compilation warnings due to Boost when using g++ on OSX
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 11:59:31 -07:00
Leonardo de Moura
8d1ec69599
fix(CMakeLists): use Boost_LIBRARIES
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 11:31:56 -07:00
Leonardo de Moura
d10d70423a
feat(frontends/lean): add new scanner
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-05 18:57:26 -07:00
Leonardo de Moura
4a25e7442a
feat(kernel/expr): add optional expression caching (aka "partial" hash-consing)
...
We do not enforce full hash-consing because we would need to synchronize
the access to the hashtable/cache.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 15:35:47 -07:00
Leonardo de Moura
4cbcc73bb6
feat(build): add GPROF compilation mode for using gprof
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-27 10:21:03 -07:00
Leonardo de Moura
45d473d44e
feat(kernel): add mk_hott_environment function for creating HoTT compatible environments
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 11:31:34 -07:00
Leonardo de Moura
f3ed20a229
feat(kernel/inductive): add normalizer extension for inductive datatypes, add procedure for creating an standard (empty) Lean environment
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-19 12:52:25 -07:00
Leonardo de Moura
eb0abf557d
feat(kernel/inductive): add inductive datatype kernel extension module interface
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 09:53:51 -07:00
Leonardo de Moura
391b2fe739
refactor(builtin): remove old library, we will build a new one for Lean 0.2
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 15:56:28 -07:00
Leonardo de Moura
c6af56260e
refactor(frontends/lean): remove dead code
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 15:51:41 -07:00
Leonardo de Moura
cd30bb49c1
chore(library/arith): remove unnecessary library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 16:14:15 -07:00
Leonardo de Moura
f7e705badb
refactor(library/kernel_bindings): reactive some of the kernel Lua bindings
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 11:52:09 -07:00