Leonardo de Moura
2c926478dd
feat(bin): add leanemacs startup script
2015-01-30 13:05:30 -08:00
Leonardo de Moura
d0ce4cf62f
fix(CMakeLists.txt): path to ninja
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2015-01-30 10:37:49 -08:00
Leonardo de Moura
a44fec6eb4
fix(CMakeLists.txt): path to ninja
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2015-01-30 10:32:35 -08:00
Leonardo de Moura
1ee52a3ddc
feat(CMakeLists.txt): include ninja in Windows binary distribution package
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2015-01-30 09:59:55 -08:00
Leonardo de Moura
12674114a4
feat(shell): set default behavior to "trusted"
...
closes #402
2015-01-21 16:25:09 -08:00
Leonardo de Moura
5ab7ff62b5
feat(CMakeLists): add --Trust option when building standard/hott libraries
2015-01-20 11:11:35 -08:00
Soonho Kong
901c9bf67a
refactor: rename ltags => leantags
...
fix #394
2015-01-18 13:44:41 +09:00
Leonardo de Moura
5c9a277dea
feat(CMakeLists): include runtime files in Windows binary distribution package
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2015-01-14 12:37:25 -08:00
Leonardo de Moura
730e038dd3
feat(CMakeLists): add basic example to binary distribution package
2015-01-14 10:39:07 -08:00
Leonardo de Moura
0509baa64a
feat(CMakeLists): add README file for binary distribution packages
2015-01-14 10:35:51 -08:00
Leonardo de Moura
c9132648a2
feat(CMakeLists): include HoTT library in binary package
2015-01-14 10:00:35 -08:00
Leonardo de Moura
d52fc83274
fix(build): clean-olean target should also clean HoTT library
2014-12-05 14:42:37 -08:00
Leonardo de Moura
0034ad9b34
feat(build): add HoTT library to build
2014-12-05 14:38:45 -08:00
Soonho Kong
53e18d0e39
chore(src/CMakeLists.txt): copy linja and ltag to bin when install
2014-11-04 18:16:04 -05:00
Leonardo de Moura
a7a06ab0f8
feat(library/definitional/rec_on): automatically generate rec_on function for inductive datatypes
2014-10-25 13:08:59 -07:00
Leonardo de Moura
ab4c292872
fix(build): do not disable unicode chars on Windows
2014-10-23 20:58:23 -07:00
Soonho Kong
1915674b4d
feat(CMakeLists.txt): support emscripten
2014-10-14 18:59:15 -07:00
Leonardo de Moura
5ff200c516
chore(library/simplifier): delete old simplifier
...
This was the simplifier used in Lean 0.1.
2014-10-14 15:56:09 -07:00
Soonho Kong
826166c257
feat(CMakeLists.txt): use bin/package_version if needed
...
1) When git sha1 is available:
Lean (version 0.2.0, commit 4a119a0424
, Release)
2) When git sha1 is not available, but there is bin/package_version file
Lean (version 0.2.0, package 0.2.0~ubuntu1~12.04, Release)
3) Git sha1 is not available, bin/package_version does not exist.
Lean (version 0.2.0, Release)
Close #229
2014-10-07 16:58:44 -07:00
Soonho Kong
d5abaf6446
feat(CMakeLists.txt): install lean library to LIBRARY_DIR (default: lib/lean)
2014-10-07 12:30:39 -07:00
Soonho Kong
013cd5640e
fix(CMakeLists.txt): rename EMACS_LIB to EMACS_LISP_DIR (default: share/eamcs/site-lisp/lean)
2014-10-07 12:30:39 -07:00
Soonho Kong
103cf57a46
chore(CMakeLists.txt): standard_lib target generates TAGS for library
2014-10-07 12:30:39 -07:00
Soonho Kong
2cf6cf19c0
feat(src): add LEAN_VERSION_PATCH
2014-10-07 12:30:38 -07:00
Soonho Kong
286aae933c
chore(CMakeLists.txt): add EMACS_LIB option to specify installation path for emacs stuff
2014-10-06 11:20:13 -07:00
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