michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(*): fix cygwin compilation errors

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-28 13:49:18 -08:00
parent 662fb71d59
commit ff052d41ee
4 changed files with 10 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/tactic/cex_builder.cpp
View file

@ -22,9 +22,9 @@ static int mk_cex_builder(lua_State * L) {
luaref ref(L, 1); luaref ref(L, 1);
return push_cex_builder(L, return push_cex_builder(L,
mk_cex_builder([=](name const & n, optional<counterexample> const & cex, assignment const & a) -> counterexample { mk_cex_builder([=](name const & n, optional<counterexample> const & cex, assignment const & a) -> counterexample {
script_state _S(S); script_state S_copy(S);
optional<environment> r; optional<environment> r;
_S.exec_protected([&]() { S_copy.exec_protected([&]() {
ref.push(); // push user-fun on the stack ref.push(); // push user-fun on the stack
push_name(L, n); push_name(L, n);
if (cex) if (cex)

4
src/library/tactic/proof_builder.cpp
View file

@ -83,8 +83,8 @@ static int mk_proof_builder(lua_State * L) {
return push_proof_builder(L, return push_proof_builder(L,
mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr { mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
expr r; expr r;
script_state _S(S); script_state S_copy(S);
_S.exec_protected([&]() { S_copy.exec_protected([&]() {
ref.push(); // push user-fun on the stack ref.push(); // push user-fun on the stack
push_proof_map(L, m); push_proof_map(L, m);
push_assignment(L, a); push_assignment(L, a);

10
src/library/tactic/tactic.cpp
View file

@ -386,13 +386,13 @@ static int mk_lua_tactic01(lua_State * L) {
luaref ref(L, 1); luaref ref(L, 1);
return push_tactic(L, return push_tactic(L,
mk_tactic01([=](environment const & env, io_state const & ios, proof_state const & s) -> optional<proof_state> { mk_tactic01([=](environment const & env, io_state const & ios, proof_state const & s) -> optional<proof_state> {
script_state _S(S); script_state S_copy(S);
optional<proof_state> r; optional<proof_state> r;
luaref coref; // Remark: we have to release the reference in a protected block. luaref coref; // Remark: we have to release the reference in a protected block.
try { try {
bool done = false; bool done = false;
lua_State * co; lua_State * co;
_S.exec_protected([&]() { S_copy.exec_protected([&]() {
co = lua_newthread(L); // create a coroutine for executing user-fun co = lua_newthread(L); // create a coroutine for executing user-fun
coref = luaref(L, -1); // make sure co-routine in not deleted coref = luaref(L, -1); // make sure co-routine in not deleted
lua_pop(L, 1); lua_pop(L, 1);
@ -406,11 +406,11 @@ static int mk_lua_tactic01(lua_State * L) {
while (!done) { while (!done) {
check_interrupted(); check_interrupted();
std::this_thread::yield(); // give another thread a chance to execute std::this_thread::yield(); // give another thread a chance to execute
_S.exec_protected([&]() { S_copy.exec_protected([&]() {
done = resume(co, 0); done = resume(co, 0);
}); });
} }
_S.exec_protected([&]() { S_copy.exec_protected([&]() {
if (is_proof_state(co, -1)) { if (is_proof_state(co, -1)) {
r = to_proof_state(co, -1); r = to_proof_state(co, -1);
} }
@ -418,7 +418,7 @@ static int mk_lua_tactic01(lua_State * L) {
}); });
return r; return r;
} catch (...) { } catch (...) {
_S.exec_protected([&]() { coref.release(); }); S_copy.exec_protected([&]() { coref.release(); });
throw; throw;
} }
})); }));

1
src/util/script_exception.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/ */
#include <sstream> #include <sstream>
#include <string> #include <string>
#include <cstdlib>
#include "util/debug.h" #include "util/debug.h"
#include "util/script_exception.h" #include "util/script_exception.h"