Soonho Kong
ba13144094
chore(.travis.yml): add 'travis_wait' to doxygen build
...
"If you have a command that doesn't produce output for
more than 10 minutes, you can prefix it with travis_wait,
a function that's exported by our build environment."
http://docs.travis-ci.com/user/build-timeouts/
2014-06-02 22:37:27 -04:00
Leonardo de Moura
7b28419260
chore(*): disable multi thread support for OSX, remove the !defined(APPLE) directives
...
We should re-enable multi thread support for OSX as soon as the bug in clang is fixed.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 18:23:26 -07:00
Leonardo de Moura
980eb2fa5c
fix(doc/lua): typos in the documentation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 18:14:19 -07:00
Leonardo de Moura
f816487f4b
fix(kernel/level): add (trivial) case for is_geq predicate: l >= 0 for any l
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 18:13:50 -07:00
Leonardo de Moura
045fa911d1
fix(library/kernel_bindings): missing kind in lean_kind
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 18:12:02 -07:00
Leonardo de Moura
ab7469c175
fix(library/scope): warning message, and old comment
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 18:08:46 -07:00
Leonardo de Moura
5f3ac6287f
fix(doc/lua): markup
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 17:47:25 -07:00
Leonardo de Moura
c0b82412db
doc(doc/lua): add universe level documentation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 17:36:07 -07:00
Leonardo de Moura
1467bb256e
chore(library): remove unnecessary code
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 16:22:38 -07:00
Leonardo de Moura
33bbcd9526
chore(kernel/declaration): rename declaration::get_params to declaration::get_univ_params
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 16:20:34 -07:00
Leonardo de Moura
82e1f87e08
feat(kernel): add function param_names_to_levels
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 16:17:04 -07:00
Leonardo de Moura
96f639811c
chore(kernel/level): remove unnecessary code
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 15:42:37 -07:00
Leonardo de Moura
712c10f818
fix(library/scope): make sure the local universe names do not conflict with universe parameter names when close a section, add declaration parameter name sanitizers
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 15:39:57 -07:00
Leonardo de Moura
f82658f213
feat(library): add helper functions for 'updating' declarations
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 15:13:38 -07:00
Leonardo de Moura
e155708dda
feat(util): add (functional) name_map
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 14:46:13 -07:00
Leonardo de Moura
dcacf6fbca
refactor(util): rename name_map to name_hash_map
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 14:34:22 -07:00
Leonardo de Moura
b6d2328c1d
fix(library/scope): make sure local levels are added in the beginning of the universe parameter list
...
The idea is to make sure it is consistent with the behavior used for regular local parameters.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 14:06:31 -07:00
Leonardo de Moura
e9664cb042
fix(kernel/type_checker): check if the declaration contains duplicate universe level parameters
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 13:57:43 -07:00
Leonardo de Moura
9b6b162a7c
fix(library/scope): bug when abstracting inductive declaration in the end of a section
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 13:46:16 -07:00
Leonardo de Moura
2a101657c8
test(lua): add section+inductive_family test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 13:07:13 -07:00
Leonardo de Moura
6ee272477a
fix(library/private): bug when preserving private names at end_section
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 11:32:14 -07:00
Leonardo de Moura
936ca80b9b
fix(library/scope): bug in add_definition
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 11:04:34 -07:00
Leonardo de Moura
e56307f006
fix(library/scope): bug in end_scope procedure
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 10:43:28 -07:00
Leonardo de Moura
6e113206b6
feat(library/scope): add support for inductive datatypes in sections
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 10:28:07 -07:00
Leonardo de Moura
d36ef5dcbe
feat(library/private): preserve 'hidden/private name => user name' map when section is closed
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-01 18:09:11 -07:00
Leonardo de Moura
585f3adde1
feat(library/scope): add sections
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-01 17:55:11 -07:00
Leonardo de Moura
286d7f0e64
feat(library): add namespace management
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-31 15:41:01 -07:00
Leonardo de Moura
3145cee51f
refactor(library/aliases): move replace_prefix to util/name
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-31 15:11:22 -07:00
Leonardo de Moura
f7b3061a66
feat(library/module): improve 'import module' error messages
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-31 12:52:06 -07:00
Leonardo de Moura
37b5570e99
test(lua): add .olean corrupted file tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-31 12:51:33 -07:00
Leonardo de Moura
75abcea83f
fix(library/kernel_bindings): Lua API consistency, environment:add method also register declaration in the export table
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-31 12:20:57 -07:00
Leonardo de Moura
7bd10c2d2d
feat(library/module): export global universe level declarations
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-31 12:12:41 -07:00
Leonardo de Moura
1b5366cfb7
feat(library): add module for implementing aliases and 'using' command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-30 21:42:40 -07:00
Leonardo de Moura
6902d8cb05
feat(library): add simple placeholder module
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-30 20:28:28 -07:00
Leonardo de Moura
72f9e26dab
refactor(library/private): add hidden_to_user_name and user_to_hidden_name functions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-30 17:52:01 -07:00
Leonardo de Moura
cba52b76c7
test(lua): add integer datatype test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-30 16:30:33 -07:00
Leonardo de Moura
6587d0f8f3
test(lua): add is_sorted inductive predicate example
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-30 16:30:32 -07:00
Leonardo de Moura
128d668f03
feat(library): add support for creating 'private/hidden' names
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 18:37:09 -07:00
Leonardo de Moura
13f9db26b7
refactor(library): add module namespace
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 13:58:47 -07:00
Leonardo de Moura
fc7d5461b1
feat(library/kernel_bindings): add to_io_state_ext helper function
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 13:35:11 -07:00
Leonardo de Moura
f8e71f711f
feat(library/expr_lt): add expr_quick_cmp functional object
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 13:34:16 -07:00
Leonardo de Moura
88440cbb3e
feat(util/name): add optional<name> helper functions for implementing Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 13:33:42 -07:00
Leonardo de Moura
bfa9b90af0
feat(library/kernel_bindings): used 'named' parameters in import_modules API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 11:03:44 -07:00
Leonardo de Moura
ade5d99023
feat(library/modules): add option for discarding the proof of imported theorems (after checking them)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 10:56:28 -07:00
Leonardo de Moura
28b9d17a14
perf(library/module): do not use multiple threads when skipping type checking, add flag to disable/enable type checking theorems asynchronously
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-28 10:04:42 -07:00
Leonardo de Moura
e206fcc1af
perf(kernel/type_checker): reduce the overhead of creating delayed_justification objects, a huge number of them is created when type checking applications
...
We reduce the cost by avoiding the allocation of std::functional objects, and the unnecessary increment/decrement of reference counters.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-27 23:16:52 -07:00
Leonardo de Moura
1b4c9f63ce
perf(kernel/environment): improve is_descendant performance, optimize for the common case: the is_descendant tree is huge but has few deep branches
...
This is an important optimization for module.cpp. The benchmark tests/lua/slow/mod2.lua is a good example where the cost of is_descendant was neutralizing the benefit of the replace method.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-27 22:29:03 -07:00
Leonardo de Moura
0f894f4618
chore(*): tag 'slow' tests as 'expensive', and exclude 'expensive' tests when testing under valgrind
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-27 17:47:53 -07:00
Leonardo de Moura
162fa25250
test(lua): move slow tests to tests/lua/slow
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-27 10:24:18 -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