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

2583 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
99a163f11d Simplify metavariable context. Now, we have only 'lift' and 'inst' instead of 'subst', 'lift' and 'lower' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-16 19:32:28 -07:00
Leonardo de Moura
cad562a448 Add support for metavariables in the normalizer. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-16 19:32:28 -07:00
Leonardo de Moura
1be2a30c8c Fix bug in normalizer. We must create a scope whenever we extend the value stack. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-16 19:32:28 -07:00
Soonho Kong
01339a93a3 Fix cpplint warning in util/safe_arith.cpp 2013-09-16 19:12:12 -07:00
Soonho Kong
85a92e8888 Fix typo in .travis.yml 2013-09-16 18:51:59 -07:00
Soonho Kong
13401d534c Add static assertion to util/safe_arith.cpp 2013-09-16 18:17:05 -07:00
Soonho Kong
6ee14bf17f Use unsigned short for the type of interval::bound_deps 2013-09-16 18:15:32 -07:00
Soonho Kong
a2182b59e3 Fix memcheck.supp problem 2013-09-16 18:14:55 -07:00
Soonho Kong
ef18759e77 Update src/CmakeLists.txt - only check style over files starting with [A-z] 2013-09-16 16:23:20 -07:00
Soonho Kong
9b792d938d Update .travis.yml 
fix typo [skip ci]
 2013-09-15 22:07:55 -07:00
Leonardo de Moura
f79f046294 Add partial support for metavariables in the normalizer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-15 21:23:50 -07:00
Soonho Kong
e6d9aa7527 Use GNU parallel to upload doxygen files to dropbox 
[skip ci]
 2013-09-15 20:31:15 -07:00
Soonho Kong
58c8c1a5ec Add EXCLUDE_PATTERNS to src/Doxyfile 
- */src/cmake/*
- GTAGS GPATH GRTAGS
- memcheck.supp
- *.cmake *.cmake.in
-  *.txt
 2013-09-15 20:31:15 -07:00
Soonho Kong
7b7cafd499 Fix typo in script/dropbox_upload.py 2013-09-15 20:31:15 -07:00
Leonardo de Moura
2800292947 Add timestamp to metavar_env 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-15 19:50:48 -07:00
Leonardo de Moura
5a4bc331d2 Make unification_problems a virtual class. Associate a 'standard' context with each metavariable in metavar_env 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-15 19:38:36 -07:00
Soonho Kong
b1310bd679 Update .travis.yml 
- force to use precompiled cmake
- do not delete old doxygen files (will fix later)
[skip ci]
 2013-09-15 13:51:02 -07:00
Soonho Kong
5edf78559d Fix typo in .travis.yml 2013-09-15 12:27:42 -07:00
Soonho Kong
2d8febb7f1 Fix .travis.yml 
- Use precompiled cmake
- clang + ninja + release build still has a bug. Use make instead.
 2013-09-15 12:23:10 -07:00
Leonardo de Moura
63e102055e Move metavariables to the kernel. This is the first step for implementing the new elaborator. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-15 12:09:01 -07:00
Soonho Kong
dfd4b3b57f Use latest version of cmake in travis-ci 2013-09-15 11:53:33 -07:00
Soonho Kong
e1b4a45f92 Update .travis.yml 
- clang++-3.3 has a bug on travis when it uses ninja for a release-build.
- let's use ninja for memcheck builds and GNU make for the rest of builds.
 2013-09-15 04:03:26 -07:00
Soonho Kong
c9affe489f Update travis.yml, disable parallel build on travis-ci 2013-09-15 03:40:28 -07:00
Soonho Kong
7834fe045f Update .travis.yml to build ninja from scratch 2013-09-15 03:20:34 -07:00
Soonho Kong
993f720ce1 Update .travis.yml to use ninja instead of GNU make 
There is a bug in cmake. With GNU Make, it ignores the memcheck suppressions
file (src/memcheck.supp), while it works well with ninja.
 2013-09-15 02:19:29 -07:00
Soonho Kong
09945add63 Fix typo in .travis.yml 2013-09-15 01:50:23 -07:00
Soonho Kong
e4b327bbaa Use C++11's <random> in pdeque/pvector tests (cygwin doesn't support rand_r) 2013-09-15 01:38:57 -07:00
Soonho Kong
dcc917a6b4 Use "sprintf" instead of "snprintf" because cygwin doesn't support "snprintf" 2013-09-15 01:38:21 -07:00
Soonho Kong
b553521578 Attempt to suppress valgrind warnings on Travis 
- don't understand why cmake on travis doesn't pick up the memcheck.supp
file. It works on my local machine.
 2013-09-15 01:17:05 -07:00
Soonho Kong
15861ef6ea Update binary uploading process 
- fix commit name for OSX & Windows
- fix NOW to use specific time zone, PST
- upload compressed binary for archiving
 2013-09-15 01:17:05 -07:00
Soonho Kong
d51af953ca Update doxygen process, only update changed files 2013-09-15 01:17:05 -07:00
Leonardo de Moura
f527b931d8 Update todo.md 2013-09-14 23:07:40 -07:00
Leonardo de Moura
a66d4ec42a Update todo.md 2013-09-14 23:06:10 -07:00
Soonho Kong
b0ad45a268 Update ccache.md 
Add reference [skip ci]
 2013-09-14 21:31:31 -07:00
Soonho Kong
d28edfce89 Update ccache.md 
fix typo [skip ci]
 2013-09-14 21:30:57 -07:00
Soonho Kong
8f88fcaf93 Add a section for clang to doc/make/ccache.md 2013-09-14 21:25:12 -07:00
Soonho Kong
626ba7247b Update docs, use 4-space indentation for code fragments 2013-09-14 21:18:05 -07:00
Soonho Kong
30f4b2de5f Update memcheck.supp 
[skip ci]
 2013-09-14 19:33:47 -07:00
Soonho Kong
ce05345129 Update CTestConfig.cmake to fix memcheck.supp 2013-09-14 20:22:05 -04:00
Soonho Kong
60903d3cea Fix cygwin build which was failed due to snprintf 2013-09-14 17:11:37 -07:00
Leonardo de Moura
b2deee629e Add documentation for automatic builds 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-14 11:58:51 -07:00
Leonardo de Moura
eb4c352dfe Add links to gcc and clang 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-14 11:39:31 -07:00
Soonho Kong
c96a6982a0 Add <ctime> header for time() in pdeque/pvector tests 2013-09-13 20:42:49 -07:00
Soonho Kong
5266e22f05 Remove debug code from cpplint.py 2013-09-13 20:37:31 -07:00
Soonho Kong
f752d4c791 Update style.md 2013-09-13 20:30:48 -07:00
Soonho Kong
eda25e77a4 Use time(0) as an initial seed for rand_r() in pvector/pdeque tests 2013-09-13 20:28:15 -07:00
Soonho Kong
f8c0c02cb0 Exclude 'style_check' from MemCheck list 2013-09-13 20:27:35 -07:00
Soonho Kong
0905529720 Add "style_check" test 2013-09-13 20:00:55 -07:00
Soonho Kong
0c450b5c23 Add StyleCheck.cmake 2013-09-13 19:21:02 -07:00
Soonho Kong
f620f54b32 Add target "style" to run cpplint.py 
- try "ninja style"
 2013-09-13 19:15:38 -07:00