438
85%

Ran 10 Feb 2015 02:15AM UTC

Jobs 2

Files 313

Run time 8min

Badge

Embed ▾

pending completion

Build # 438

Build Type

push

travis-ci

Committed by

leodemoura

Commit Message

feat(lua): add safe_function template that catches Lean and C++ exceptions and convert them into Lua errors

I'm using the approach described at:
http://stackoverflow.com/questions/4615890/how-to-handle-c-exceptions-when-calling-functions-from-lua

BTW, in some Lua versions, the C++ exceptions are correctly propagated.
I think we should not rely on features of particular implementations.
For example, LuaJIT does not propagate C++ exceptions.
Whenever an exception is thrown from C++ code invoked from LuaJit, LuaJit interrupts the execution and converts it to an error "C++ exception".
On the other hand, Lua 5.2 PUC-Rio interpreter (for Ubuntu) seem to propagate the C++ exceptions.
The template safe_function solves the issue. It will also produce a Lua error whenever the function being wrapped throws an exception. The error message is based on the "what()" method.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

Run Details

5239 of 9489 relevant lines covered (55.21%)

44.84 hits per line

Jobs

ID	Job ID	Ran	Files	Coverage
7	438.7 (CMAKE_CXX_COMPILER=g++-4.8 CMAKE_BUILD_TYPE=RELEASE TCMALLOC=ON UPLOAD=linux_tcmalloc PUSH_TO_CDASH=TRUE)	13 Mar 2014 08:00PM UTC	313	55.21	Travis Job 438.7
9	438.9 (CMAKE_CXX_COMPILER=g++-4.8 CMAKE_BUILD_TYPE=RELEASE TCMALLOC=OFF UPLOAD=linux PUSH_TO_CDASH=TRUE)	10 Feb 2015 02:23AM UTC	0		Travis Job 438.9

Source Files on build 438

Coverage	∆	File	Lines	Relevant	Covered	Missed	Hits/Line

leanprover / lean / 438
85%

README BADGES
x

Markdown

Textile

RDoc

HTML

Rst

Jobs

Source Files on build 438

leanprover / lean / 438 85%

README BADGES x

Markdown

Textile

RDoc

HTML

Rst

Jobs

Source Files on build 438

leanprover / lean / 438
85%

README BADGES
x