Commit graph

5097 commits

Author SHA1 Message Date
Soonho Kong
a993424165 Use "--gen-suppressions=all" in valgrind 2013-09-10 17:09:39 -07:00
Soonho Kong
9b0f12931c Update .travis files
- move triggers (BB/Win/OSX) to before_script section
 - update DROPBOX_KEY for windows
 - copy archive binaries to dropbox
 - do not use custom lcov. just use ctest -ExperimentalCoverage
2013-09-10 17:05:14 -07:00
Soonho Kong
ecc43e51ed Add "-VV" option to MemCheck to avoid travis time-outs 2013-09-10 16:10:58 -07:00
Soonho Kong
6569406fb9 Update memcheck.supp
add reference for the suppression stuff
[skip ci]
2013-09-10 15:47:47 -07:00
Soonho Kong
3505ed8adb Use suppressions file to ignore certain valgrind warnings 2013-09-10 15:37:09 -07:00
Soonho Kong
9113f824bd Use '--track-origins=yes' option in valgrind 2013-09-10 14:31:30 -07:00
Leonardo de Moura
6fe86ffefd Fix initialized memory error reported by Valgrind. Disable 2 tests that produce memory leaks due to a bug in g++.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-10 13:51:02 -07:00
Soonho Kong
fae6c29237 Fix memory leaks in mpfp.h 2013-09-10 13:26:14 -07:00
Soonho Kong
8ce18a1508 Use "--leak-check=full" option in valgrind 2013-09-10 13:12:22 -07:00
Soonho Kong
48b5625f41 Update .travis files to continue memcheck if it generates exceptions 2013-09-10 13:09:10 -07:00
Soonho Kong
f4edbba325 Turn off '--show-reachable=yes' valgrind option 2013-09-10 12:34:33 -07:00
Leonardo de Moura
9fe52900a7 Add script for using HPC cluster
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-10 11:05:03 -07:00
Soonho Kong
b04bdae763 Use "--trace-children=yes" option for MemCheck(valgrind) to handle
leantests shell script
2013-09-10 10:47:04 -07:00
Leonardo de Moura
4c67721d32 Fix test error on Cygwin
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-09 18:35:11 -07:00
Leonardo de Moura
d912c9cd09 Add more 'bad' examples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-09 09:19:49 -07:00
Leonardo de Moura
0a08494f4d Add another bad example for current elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-08 23:21:43 -07:00
Leonardo de Moura
adfbba6447 Fix problem reported by Soonho
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-08 23:10:33 -07:00
Leonardo de Moura
2ca30571b4 Display the input term in the output of the Check command. It is useful to see the fully elaborated term.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-08 22:55:21 -07:00
Leonardo de Moura
a8ba50531b Fix typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-08 20:38:11 -07:00
Leonardo de Moura
59a589037e Keep expanded form when pretty printings variable declarations with implicit marks (i.e., curly braces)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-08 11:23:46 -07:00
Leonardo de Moura
df116f88e0 Improve pretty printer for Pi's
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-08 11:04:07 -07:00
Leonardo de Moura
1cee392483 Add light_checker: module for extracting the type of (fully elaborated) expressions. It is much faster than type_checker, which infers the type but also check whether the input is type correct or not.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-07 22:33:18 -07:00
Leonardo de Moura
6bb9fc859e Add examples that demonstrate limitations of the current elaborator. The new design, we are working on, will be able to solve them.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-07 19:40:40 -07:00
Leonardo de Moura
33c4b44b2b Encapsulate context implementation. The current implementantion based on lists may be a performance problem in the future, and we should be able to change it without affecting the whole code base.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-07 11:15:11 -07:00
Leonardo de Moura
bab11b57ad Move Symm and Trans back to basic_thms.cpp
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 23:49:35 -07:00
Leonardo de Moura
c674bb3790 Add castlib as an independent library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 23:40:47 -07:00
Leonardo de Moura
7a9d53d0d7 Refactor arith libraries
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 23:19:47 -07:00
Leonardo de Moura
b92bbeb83b Add casting propagation and normalization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 20:45:26 -07:00
Leonardo de Moura
7eab229114 Improve check_pi in lean elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 18:58:33 -07:00
Leonardo de Moura
c0c2f52087 Add Cast, DomInj and RanInj. Improve operator << for lean_frontend objects.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 18:32:15 -07:00
Leonardo de Moura
b62816cc25 Fix problem with pretty printer. Add another test for elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 18:01:11 -07:00
Leonardo de Moura
edafd519e1 Add missing case to elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 17:43:08 -07:00
Leonardo de Moura
26bf7bcaac Fix bug in the elaborator. Move character ' to class A
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 17:12:35 -07:00
Leonardo de Moura
8840b37258 Fix type checker and elaborator for let expressions. Fix get_coercions (we need to pass the context). Fix pretty printer for def_type_mismatch_exception.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 11:02:00 -07:00
Leonardo de Moura
2459c4ae7c Add (optional) type to let declarations
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 10:06:26 -07:00
Leonardo de Moura
6da194334e Move 'slow' test files to different subdir. Modify CTestCustom.cmake.in to run leantests.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 08:48:12 -07:00
Leonardo de Moura
6f3b0c30fb Add 'Variables' command.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 08:48:12 -07:00
Leonardo de Moura
3dc55c452c Parse decimal values
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 08:48:12 -07:00
Soonho Kong
f3f74b9ff5 Fix .travis files
- OSX sed expects parameter for "-i" option
- for Windows and OSX build, we need to get the commit hash of HEAD~
  instead of HEAD because we made an extra commit to trigger the build
2013-09-05 20:53:21 -07:00
Soonho Kong
d9bca66585 Update .travis files to have consistent site/build names 2013-09-05 20:20:37 -07:00
Leonardo de Moura
0680865689 Fix typo 2013-09-05 19:18:55 -07:00
Leonardo de Moura
b3a095b068 Fix pretty printer for evaluator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-05 18:57:29 -07:00
Leonardo de Moura
71d76a891c Add proof by evaluation examples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-05 18:56:33 -07:00
Leonardo de Moura
c22bd8b6ed Clean elaborator_exception pretty printing
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-05 10:15:52 -07:00
Leonardo de Moura
eb96e6441f Moved kernel exception formatting to kernel_exception_formatter.cpp.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-05 10:15:43 -07:00
Soonho Kong
fbd778fe2e Update .travis.windows.yml
change OS to Windows from Linux.
[skip ci]
2013-09-04 17:52:38 -07:00
Soonho Kong
974b99b424 Update CTestCustom.cmake.in
Exclude "threads" test from valgrind targets
[skip ci]
2013-09-04 16:41:04 -07:00
Leonardo de Moura
87d3961158 Improve elaborator error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 16:36:58 -07:00
Leonardo de Moura
613d83cdf4 Improve application type mismatch errors. We also show the implicit arguments (not just their types)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 16:36:58 -07:00
Leonardo de Moura
408005b730 Fix typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 16:36:57 -07:00