From d3990fd0e22954c9bc6194cffc48e1f789a8ba0d Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Sat, 27 Apr 2019 23:17:35 -0400 Subject: [PATCH 01/36] Add src/library/vm/vm_dynload.h This module will allow the vm to dynamically link shared objects at run time so that Lean can call external code written in C/C++. Fixes: leanprover-community/lean #24 --- src/library/vm/vm.cpp | 1 + src/library/vm/vm_dynload.cpp | 12 ++++++++++++ src/library/vm/vm_dynload.h | 5 +++++ 3 files changed, 18 insertions(+) create mode 100644 src/library/vm/vm_dynload.cpp create mode 100644 src/library/vm/vm_dynload.h diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index cad7be9d1e..4f0762efb0 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -30,6 +30,7 @@ Author: Leonardo de Moura #include "library/vm/vm_name.h" #include "library/vm/vm_option.h" #include "library/vm/vm_expr.h" +#include "library/vm/vm_dynload.h" #include "library/normalize.h" #ifndef LEAN_DEFAULT_PROFILER_FREQ diff --git a/src/library/vm/vm_dynload.cpp b/src/library/vm/vm_dynload.cpp new file mode 100644 index 0000000000..4cceaa7d13 --- /dev/null +++ b/src/library/vm/vm_dynload.cpp @@ -0,0 +1,12 @@ +/* +Author: James King +*/ + +#include + +void get_shared_funcptr(const char * pathname) { + void* handle = dlopen("libpq.so", RTLD_LAZY); + if (!handle) { + cerr << "Cannot load library: " << dlerror() << '\n'; + } +} diff --git a/src/library/vm/vm_dynload.h b/src/library/vm/vm_dynload.h new file mode 100644 index 0000000000..590c6bbaec --- /dev/null +++ b/src/library/vm/vm_dynload.h @@ -0,0 +1,5 @@ +#include + +namespace lean { +void get_shared_funcptr(const char * pathname); +} From bd7478f7bb0c94b55ba95c6407cb97c4a2e711dd Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Tue, 30 Apr 2019 22:52:01 -0400 Subject: [PATCH 02/36] Add vm_foreign_obj struct --- src/library/vm/vm_dynload.cpp | 32 ++++++++++++++++++++++++++++---- 1 file changed, 28 insertions(+), 4 deletions(-) diff --git a/src/library/vm/vm_dynload.cpp b/src/library/vm/vm_dynload.cpp index 4cceaa7d13..b233e77912 100644 --- a/src/library/vm/vm_dynload.cpp +++ b/src/library/vm/vm_dynload.cpp @@ -3,10 +3,34 @@ Author: James King */ #include +#include +#include + +#define FOREIGN_OBJ void * void get_shared_funcptr(const char * pathname) { - void* handle = dlopen("libpq.so", RTLD_LAZY); - if (!handle) { - cerr << "Cannot load library: " << dlerror() << '\n'; - } + void* handle = dlopen("libpq.so", RTLD_LAZY); + if (!handle) { + cerr << "Cannot load library: " << dlerror() << '\n'; + } +} + +struct vm_foreign_obj : public vm_external { + FOREIGN_OBJ m_handle; + std::string m_filename; + + vm_foreign_obj(FOREIGN_OBJ handle, std::string filename) + : m_handle(handle), + m_filename(filename) {}; + virtual ~vm_foreign_obj() {} + virtual void dealloc() override { + this->~vm_foreign_obj(); + get_vm_allocator().deallocate(sizeof(vm_foreign_obj), this); + } + virtual vm_external * clone(vm_clone_fn const &) override { + return new vm_foreign_obj(m_fd, m_filename); + } + virtual vm_external * ts_clone(vm_clone_fn const &) override { + lean_unreachable(); + } } From b2d116f270c960b7786384ec1e74bde15cd9a66f Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Wed, 1 May 2019 21:10:06 -0400 Subject: [PATCH 03/36] Add load_foreign_obj Following some conventions established in (#20) I added some constructor functions to allocate the `vm_foreign_obj` struct in the VM. --- src/library/vm/vm_dynload.cpp | 19 +++++++++++++++++-- src/library/vm/vm_dynload.h | 5 ----- 2 files changed, 17 insertions(+), 7 deletions(-) delete mode 100644 src/library/vm/vm_dynload.h diff --git a/src/library/vm/vm_dynload.cpp b/src/library/vm/vm_dynload.cpp index b233e77912..91bd38e29e 100644 --- a/src/library/vm/vm_dynload.cpp +++ b/src/library/vm/vm_dynload.cpp @@ -6,6 +6,9 @@ Author: James King #include #include +#include "util/sstream.h" +#include "library/vm/vm_io.h" + #define FOREIGN_OBJ void * void get_shared_funcptr(const char * pathname) { @@ -17,9 +20,9 @@ void get_shared_funcptr(const char * pathname) { struct vm_foreign_obj : public vm_external { FOREIGN_OBJ m_handle; - std::string m_filename; + char * m_filename; - vm_foreign_obj(FOREIGN_OBJ handle, std::string filename) + vm_foreign_obj(FOREIGN_OBJ handle, const char & filename) : m_handle(handle), m_filename(filename) {}; virtual ~vm_foreign_obj() {} @@ -34,3 +37,15 @@ struct vm_foreign_obj : public vm_external { lean_unreachable(); } } + +static vm_obj mk_foreign_obj(FOREIGN_OBJ handle, const char & fname) { + return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_foreign_obj))) vm_foreign_obj(handle, fname)); +} + +static vm_obj load_foreign_obj(vm_obj const & fname) { + FOREIGN_OBJ handle = dlopen(fname, RTLD_LAZY); + if (!handle) { + return mk_io_failure(sstream() << "failed to load foreign lib: " << dlerror()); + } + return mk_io_result(mk_foreign_obj(handle, fname); +} diff --git a/src/library/vm/vm_dynload.h b/src/library/vm/vm_dynload.h deleted file mode 100644 index 590c6bbaec..0000000000 --- a/src/library/vm/vm_dynload.h +++ /dev/null @@ -1,5 +0,0 @@ -#include - -namespace lean { -void get_shared_funcptr(const char * pathname); -} From ba09d6fca55c6efa9350f083be840ea7eb578b0d Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Wed, 1 May 2019 21:58:42 -0400 Subject: [PATCH 04/36] Add doc/library/vm.md As I'm learning about the VM architecture in Lean I'm adding notes to help future contributors. --- doc/library/vm.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 doc/library/vm.md diff --git a/doc/library/vm.md b/doc/library/vm.md new file mode 100644 index 0000000000..5d158c36a8 --- /dev/null +++ b/doc/library/vm.md @@ -0,0 +1,18 @@ +# Lean's Virtual Machine + +## Overview + +In simple terms Lean's VM is a single-threaded command-based +interpreter. As it processes a file it adds the commands it +encounters to a global environment. + +The environment is, in simple terms, a map of names to pairs of +types and values. The type and value are both expressions. + +Unless we are evaluating proofs we evaluate expressions in the +environment using the VM. Every expression in a command is compiled +to a form of byte code that can be executed by the VM. + +## TODO Architecture + +## TODO Memory From 3ee640007648b665010710e3279c9984b421b405 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Thu, 2 May 2019 20:44:50 -0400 Subject: [PATCH 05/36] add foreign objects as environment extensions --- library/init/meta/environment.lean | 6 ++++ src/library/vm/CMakeLists.txt | 3 +- src/library/vm/vm.cpp | 28 +++++++++++++-- src/library/vm/vm.h | 4 +++ src/library/vm/vm_dynload.cpp | 56 ++++++++++++------------------ src/library/vm/vm_dynload.h | 34 ++++++++++++++++++ src/library/vm/vm_environment.cpp | 22 ++++++++++++ src/library/vm/vm_io.h | 2 ++ tests/lean/vm_dynload/Makefile | 12 +++++++ tests/lean/vm_dynload/client.c | 19 ++++++++++ tests/lean/vm_dynload/ffi.lean | 22 ++++++++++++ tests/lean/vm_dynload/some_file.c | 6 ++++ 12 files changed, 178 insertions(+), 36 deletions(-) create mode 100644 src/library/vm/vm_dynload.h create mode 100644 tests/lean/vm_dynload/Makefile create mode 100644 tests/lean/vm_dynload/client.c create mode 100644 tests/lean/vm_dynload/ffi.lean create mode 100644 tests/lean/vm_dynload/some_file.c diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean index 10fff08cdb..ccfe23f29f 100644 --- a/library/init/meta/environment.lean +++ b/library/init/meta/environment.lean @@ -153,6 +153,12 @@ meta constant structure_fields : environment → name → option (list name) meta constant get_class_attribute_symbols : environment → name → name_set /-- The fingerprint of the environment is a hash formed from all of the declarations in the environment. -/ meta constant fingerprint : environment → nat + +meta constant load_foreign_object (env : environment) (n : name) (file_name : string) : environment + +meta constant bind_foreign_symbol(env : environment) (fo : name) (fn : name) + (arity : nat) (symbol : string) : environment + open expr meta constant unfold_untrusted_macros : environment → expr → expr diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt index e63e1c09da..572f59ae06 100644 --- a/src/library/vm/CMakeLists.txt +++ b/src/library/vm/CMakeLists.txt @@ -1,4 +1,5 @@ add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp vm_options.cpp vm_format.cpp vm_rb_map.cpp vm_level.cpp vm_expr.cpp vm_exceptional.cpp vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp vm_task.cpp - vm_int.cpp init_module.cpp vm_parser.cpp vm_array.cpp vm_pos_info.cpp) + vm_int.cpp init_module.cpp vm_parser.cpp vm_array.cpp + vm_pos_info.cpp vm_dynload.cpp) diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 4f0762efb0..2cd92afcda 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -1119,8 +1119,9 @@ void declare_vm_cases_builtin(name const & n, char const * i, vm_cases_function /** \brief VM function/constant declarations are stored in an environment extension. */ struct vm_decls : public environment_extension { - unsigned_map m_decls; - unsigned_map m_cases; + unsigned_map m_decls; + unsigned_map m_cases; + std::unordered_map, name_hash> m_foreign; name m_monitor; @@ -1149,6 +1150,17 @@ struct vm_decls : public environment_extension { m_decls.insert(idx, vm_decl(n, idx, arity, fn)); } + void add_foreign_obj(name const & n, string const & file_name) { + m_foreign[n] = load_foreign_obj(file_name); + } + + void bind_foreign_symbol(name const & fo, name const & fn, string const & sym, unsigned arity) { + std::cout << "bind_foreign_symbol\n"; + auto c_fun = m_foreign[fo]->get_cfun(sym); + c_fun(mk_vm_none()); + add_native(fn,arity,c_fun); + } + unsigned reserve(name const & n, unsigned arity) { unsigned idx = get_vm_index(n); if (m_decls.contains(idx)) @@ -1227,6 +1239,18 @@ environment add_native(environment const & env, name const & n, unsigned arity, return add_native(env, n, arity, reinterpret_cast(fn)); } +environment load_foreign_object(environment const & env, name const & n, string const & file_name) { + auto ext = get_extension(env); + ext.add_foreign_obj(n, file_name); + return update(env, ext); +} + +environment bind_foreign_symbol(environment const & env, name const & fo, name const & fn, unsigned arity, string const & symbol) { + auto ext = get_extension(env); + ext.bind_foreign_symbol(fo, fn, symbol, arity); + return update(env, ext); +} + bool is_vm_function(environment const & env, name const & fn) { auto const & ext = get_extension(env); return ext.m_decls.contains(get_vm_index(fn)) || g_vm_builtins->contains(fn); diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index 56bdaf7735..c9a78304b6 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -900,6 +900,10 @@ environment add_native(environment const & env, name const & n, vm_cfunction_7 f environment add_native(environment const & env, name const & n, vm_cfunction_8 fn); environment add_native(environment const & env, name const & n, unsigned arity, vm_cfunction_N fn); +environment load_foreign_object(environment const & env, name const & n, std::string const & file_name); +environment bind_foreign_symbol(environment const & env, name const & fo, name const & fn, + unsigned arity, std::string const & symbol); + unsigned get_vm_index(name const & n); unsigned get_vm_index_bound(); name get_vm_name(unsigned idx); diff --git a/src/library/vm/vm_dynload.cpp b/src/library/vm/vm_dynload.cpp index 91bd38e29e..f15e986855 100644 --- a/src/library/vm/vm_dynload.cpp +++ b/src/library/vm/vm_dynload.cpp @@ -4,48 +4,38 @@ Author: James King #include #include +#include #include #include "util/sstream.h" #include "library/vm/vm_io.h" +#include "library/vm/vm_string.h" +#include "library/vm/vm_dynload.h" -#define FOREIGN_OBJ void * +// void get_shared_funcptr(string const & pathname) { +// void* handle = dlopen(pathname.c_str(), RTLD_LAZY); +// if (!handle) { +// std::cerr << "Cannot load library: " << dlerror() << '\n'; +// } +// } -void get_shared_funcptr(const char * pathname) { - void* handle = dlopen("libpq.so", RTLD_LAZY); - if (!handle) { - cerr << "Cannot load library: " << dlerror() << '\n'; - } -} +namespace lean { +using namespace std; -struct vm_foreign_obj : public vm_external { - FOREIGN_OBJ m_handle; - char * m_filename; - - vm_foreign_obj(FOREIGN_OBJ handle, const char & filename) - : m_handle(handle), - m_filename(filename) {}; - virtual ~vm_foreign_obj() {} - virtual void dealloc() override { - this->~vm_foreign_obj(); - get_vm_allocator().deallocate(sizeof(vm_foreign_obj), this); - } - virtual vm_external * clone(vm_clone_fn const &) override { - return new vm_foreign_obj(m_fd, m_filename); - } - virtual vm_external * ts_clone(vm_clone_fn const &) override { - lean_unreachable(); + vm_cfunction vm_foreign_obj::get_cfun(string const & fun_name) { + return reinterpret_cast(dlsym(m_handle, fun_name.c_str())); } -} -static vm_obj mk_foreign_obj(FOREIGN_OBJ handle, const char & fname) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_foreign_obj))) vm_foreign_obj(handle, fname)); -} + vm_foreign_obj::~vm_foreign_obj() { + dlclose(m_handle); + } -static vm_obj load_foreign_obj(vm_obj const & fname) { - FOREIGN_OBJ handle = dlopen(fname, RTLD_LAZY); - if (!handle) { - return mk_io_failure(sstream() << "failed to load foreign lib: " << dlerror()); + shared_ptr load_foreign_obj(string const & fname) { + FOREIGN_OBJ handle = dlopen(fname.c_str(), RTLD_LAZY); + if (!handle) { + throw exception(sstream() << "failed to load foreign lib: " << dlerror()); + } + return make_shared(vm_foreign_obj(handle, fname)); } - return mk_io_result(mk_foreign_obj(handle, fname); + } diff --git a/src/library/vm/vm_dynload.h b/src/library/vm/vm_dynload.h new file mode 100644 index 0000000000..a3559af625 --- /dev/null +++ b/src/library/vm/vm_dynload.h @@ -0,0 +1,34 @@ +#include +#include + +#define FOREIGN_OBJ void * + +namespace lean { + + using std::string; + + class vm_foreign_obj { + private: + FOREIGN_OBJ m_handle; + std::string m_filename; + public: + vm_foreign_obj(FOREIGN_OBJ handle, string const & filename) + : m_handle(handle), + m_filename(filename) {}; + ~vm_foreign_obj(); + vm_cfunction get_cfun(string const & fun_name); + /* virtual void dealloc() override { */ + /* this->~vm_foreign_obj(); */ + /* get_vm_allocator().deallocate(sizeof(vm_foreign_obj), this); */ + /* } */ + /* virtual vm_external * clone(vm_clone_fn const &) override { */ + /* return new vm_foreign_obj(m_handle, m_filename); */ + /* } */ + /* virtual vm_external * ts_clone(vm_clone_fn const &) override { */ + /* return new (get_vm_allocator().allocate(sizeof(vm_foreign_obj))) vm_foreign_obj(m_handle, m_filename); */ + /* } */ + }; + + std::shared_ptr load_foreign_obj(string const & fname); + +} diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp index 3b650db0fb..c5ba356002 100644 --- a/src/library/vm/vm_environment.cpp +++ b/src/library/vm/vm_environment.cpp @@ -314,6 +314,26 @@ vm_obj environment_fingerprint(vm_obj const & env) { return mk_vm_nat(mpz(get_fingerprint(to_env(env)))); } +// environment load_foreign_object(environment const & env, name const & n, std::string const & file_name); +vm_obj environment_load_foreign_object(vm_obj const & _env, vm_obj const & _n, vm_obj const & _file_name) { + environment env = to_env(_env); + name n = to_name(_n); + std::string file_name = to_string(_file_name); + return to_obj(load_foreign_object(env,n,file_name)); +} + +// environment bind_foreign_symbol(environment const & env, name const & fo, name const & fn, +// unsigned arity, std::string const & symbol); +vm_obj environment_bind_foreign_symbol(vm_obj const & _env, vm_obj const & _fo, vm_obj const & _fn, + vm_obj const & _arity, vm_obj const & _symbol) { + environment env = to_env(_env); + name fo = to_name(_fo); + name fn = to_name(_fn); + unsigned arity = to_unsigned(_arity); + std::string symbol = to_string(_symbol); + return to_obj(bind_foreign_symbol(env,fo,fn,arity,symbol)); +} + void initialize_vm_environment() { DECLARE_VM_BUILTIN(name({"environment", "mk_std"}), environment_mk_std); DECLARE_VM_BUILTIN(name({"environment", "trust_lvl"}), environment_trust_lvl); @@ -347,6 +367,8 @@ void initialize_vm_environment() { DECLARE_VM_BUILTIN(name({"environment", "structure_fields"}), environment_structure_fields); DECLARE_VM_BUILTIN(name({"environment", "get_class_attribute_symbols"}), environment_get_class_attribute_symbols); DECLARE_VM_BUILTIN(name({"environment", "fingerprint"}), environment_fingerprint); + DECLARE_VM_BUILTIN(name({"environment", "load_foreign_object"}), environment_load_foreign_object); + DECLARE_VM_BUILTIN(name({"environment", "bind_foreign_symbol"}), environment_bind_foreign_symbol); } void finalize_vm_environment() { diff --git a/src/library/vm/vm_io.h b/src/library/vm/vm_io.h index a605e53945..002c9f508c 100644 --- a/src/library/vm/vm_io.h +++ b/src/library/vm/vm_io.h @@ -13,6 +13,8 @@ Author: Leonardo de Moura namespace lean { vm_obj mk_io_result(vm_obj const & r); vm_obj mk_io_failure(std::string const & s); +class sstream; +vm_obj mk_io_failure(sstream const & s); /* The io monad produces a result object, or an error. If `o` is a result, then we return the result value. */ optional is_io_result(vm_obj const & o); diff --git a/tests/lean/vm_dynload/Makefile b/tests/lean/vm_dynload/Makefile new file mode 100644 index 0000000000..2a7f60de2e --- /dev/null +++ b/tests/lean/vm_dynload/Makefile @@ -0,0 +1,12 @@ + +all: some_file.so client + ./client + +%.o: %.c + gcc -c -fPIC $< -o $@ + +some_file.so: some_file.o + gcc some_file.o -shared -o some_file.so + +client: client.c + gcc client.c -o client diff --git a/tests/lean/vm_dynload/client.c b/tests/lean/vm_dynload/client.c new file mode 100644 index 0000000000..811728b5fa --- /dev/null +++ b/tests/lean/vm_dynload/client.c @@ -0,0 +1,19 @@ + +#include +#include + + +int main () { + int (*my_main) (); + void* handle = dlopen("some_file.so", RTLD_LAZY); + if (!handle) { + printf("Cannot load library: %s", dlerror()); + return -1; + } + my_main = dlsym(handle, "main"); + if (!my_main) { + printf("Cannot load 'main': %s", dlerror()); + return -1; + } + my_main(); +} diff --git a/tests/lean/vm_dynload/ffi.lean b/tests/lean/vm_dynload/ffi.lean new file mode 100644 index 0000000000..6f34207350 --- /dev/null +++ b/tests/lean/vm_dynload/ffi.lean @@ -0,0 +1,22 @@ + +namespace tactic + +open environment + +meta def load_foreign_object (n : name) (str : string) : tactic unit := +updateex_env $ λ env, pure $ env.load_foreign_object n str + +meta def bind_foreign_symbol (fo fn : name) (arity : ℕ) (sym : string) : tactic unit := +updateex_env $ λ env, pure $ env.bind_foreign_symbol fo fn arity sym + +end tactic +open tactic + +def main : unit → unit → unit := λ _, id + +run_cmd +do load_foreign_object `foo "/Users/simon/lean/lean-master/tests/lean/vm_dynload/some_file.so", + bind_foreign_symbol `foo `main 2 "main", + return () + +#eval main () () diff --git a/tests/lean/vm_dynload/some_file.c b/tests/lean/vm_dynload/some_file.c new file mode 100644 index 0000000000..b6fb0c95d5 --- /dev/null +++ b/tests/lean/vm_dynload/some_file.c @@ -0,0 +1,6 @@ + +#include + +int main () { + printf("hello world\n"); +} From f4de3fb86c2676d265fdb72db804685337fef42b Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Thu, 2 May 2019 22:56:33 -0400 Subject: [PATCH 06/36] src/CMakeLists.txt We add libffi to our build dependencies --- src/CMakeLists.txt | 31 ++++++++++++++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6d4c1ef6bc..e0acf6a12f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1,3 +1,5 @@ +include(CheckSymbolExists) + cmake_minimum_required(VERSION 2.8.7) if ((${CMAKE_MAJOR_VERSION}.${CMAKE_MINOR_VERSION} GREATER 3.1) OR (${CMAKE_MAJOR_VERSION}.${CMAKE_MINOR_VERSION} EQUAL 3.1)) cmake_policy(SET CMP0054 NEW) @@ -302,6 +304,33 @@ else() find_package(GMP 5.0.5 REQUIRED) include_directories(${GMP_INCLUDE_DIR}) set(EXTRA_LIBS ${EXTRA_LIBS} ${GMP_LIBRARIES}) + # libffi + find_path(FFI_INCLUDE_PATH ffi.h PATHS ${FFI_INCLUDE_DIR}) + if( EXISTS "${FFI_INCLUDE_PATH}/ffi.h" ) + set(FFI_HEADER ffi.h CACHE INTERNAL "") + set(HAVE_FFI_H 1 CACHE INTERNAL "") + else() + find_path(FFI_INCLUDE_PATH ffi/ffi.h PATHS ${FFI_INCLUDE_DIR}) + if( EXISTS "${FFI_INCLUDE_PATH}/ffi/ffi.h" ) + set(FFI_HEADER ffi/ffi.h CACHE INTERNAL "") + set(HAVE_FFI_FFI_H 1 CACHE INTERNAL "") + endif() + endif() + + if( NOT FFI_HEADER ) + message(FATAL_ERROR "libffi includes are not found.") + endif() + + find_library(FFI_LIBRARY_PATH ffi PATHS ${FFI_LIBRARY_DIR}) + if( NOT FFI_LIBRARY_PATH ) + message(FATAL_ERROR "libffi is not found.") + endif() + + list(APPEND CMAKE_REQUIRED_LIBRARIES ${FFI_LIBRARY_PATH}) + list(APPEND CMAKE_REQUIRED_INCLUDES ${FFI_INCLUDE_PATH}) + check_symbol_exists(ffi_call ${FFI_HEADER} HAVE_FFI_CALL) + list(REMOVE_ITEM CMAKE_REQUIRED_INCLUDES ${FFI_INCLUDE_PATH}) + list(REMOVE_ITEM CMAKE_REQUIRED_LIBRARIES ${FFI_LIBRARY_PATH}) endif() # DL @@ -571,7 +600,7 @@ endif() if(STATIC) SET(CPACK_DEBIAN_PACKAGE_DEPENDS "") else() - SET(CPACK_DEBIAN_PACKAGE_DEPENDS "libstdc++-4.8-dev,libgmp-dev") + SET(CPACK_DEBIAN_PACKAGE_DEPENDS "libstdc++-4.8-dev,libgmp-dev,libffi-dev") endif() SET(CPACK_DEBIAN_PACKAGE_DESCRIPTION "Lean Theorem Prover") SET(CPACK_DEBIAN_PACKAGE_SECTION "devel") From 54f164bfc4ea51835efff8c3c76d641573e008cd Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Thu, 2 May 2019 23:10:33 -0400 Subject: [PATCH 07/36] Add libffi to EXTRA_LIBS and includes --- src/CMakeLists.txt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e0acf6a12f..7d95190156 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -331,6 +331,8 @@ else() check_symbol_exists(ffi_call ${FFI_HEADER} HAVE_FFI_CALL) list(REMOVE_ITEM CMAKE_REQUIRED_INCLUDES ${FFI_INCLUDE_PATH}) list(REMOVE_ITEM CMAKE_REQUIRED_LIBRARIES ${FFI_LIBRARY_PATH}) + set(EXTRA_LIBS ${EXTRA_LIBS} ${FFI_LIBRARY_PATH}) + include_directories(${FFI_INCLUDE_PATH}) endif() # DL From 9061f8e279933b5013d9159bb42a0b6dad2ab563 Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Fri, 3 May 2019 00:29:57 -0400 Subject: [PATCH 08/36] Modify doc/library/vm.md Add initial documentation on the VM FFI --- doc/library/vm.md | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/doc/library/vm.md b/doc/library/vm.md index 5d158c36a8..1182d2b1c4 100644 --- a/doc/library/vm.md +++ b/doc/library/vm.md @@ -16,3 +16,24 @@ to a form of byte code that can be executed by the VM. ## TODO Architecture ## TODO Memory + +## Foreign Function Interface + +Lean depends on `libffi` for it's foreign function interface on top of +`dlopen`. + +The VM environment has two functions we use to load pointers to +foreign objects opened with `dlopen`: + +1. `environment_load_foreign_object` which uses `vm_dynload` to call + `dlopen` and construct a `vm_foreign_object` instance. The instance + is added to a special map in the environment declarations. + +2. `environment_bind_foreign_symbol` which uses `libffi` to create a + `ff_cif` object from the Lean function definition. The `lib_cif` + gets stored in the declaration with the function. + +When the environment evaluates an expression that calls a function +from a foreign object it gets the `ffi_cif` for that function, +initializes the argument values on the stack, and calls the `libffi` +interface with the handle to the foreign library and the `ffi_cif`. From 1a8fa985d8a7f97cb4769735e05c55dda248ea5d Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Thu, 9 May 2019 22:34:53 -0400 Subject: [PATCH 09/36] Register ffi attribute WIP We register a declaration attribute to bind foreign functions to Lean constants like so: @[ffi `libfoo] constant foo_fun : c_int -> c_int -> c_int Allowing the vm to get a handle to the foreign function from `dlsym` and map it with a `ffi_cif` struct from `ffi.h`. This will allow Lean users to then create functions using this type to marshal Lean values into the bound `ffi_cif` and make the call with `libffi` under the hood. --- src/library/vm/vm_environment.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp index c5ba356002..173e2fe905 100644 --- a/src/library/vm/vm_environment.cpp +++ b/src/library/vm/vm_environment.cpp @@ -5,10 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include #include "library/unfold_macros.h" #include "kernel/type_checker.h" #include "kernel/inductive/inductive.h" #include "kernel/standard_kernel.h" +#include "library/attribute_manager.h" #include "library/module.h" #include "library/scoped_ext.h" #include "library/class.h" @@ -335,6 +337,11 @@ vm_obj environment_bind_foreign_symbol(vm_obj const & _env, vm_obj const & _fo, } void initialize_vm_environment() { + register_system_attribute(basic_attribute( + "ffi", "Registers a binding to a foreign function.", + [](environment const &, io_state const &, name const &, unsigned, bool) { + return; + })); DECLARE_VM_BUILTIN(name({"environment", "mk_std"}), environment_mk_std); DECLARE_VM_BUILTIN(name({"environment", "trust_lvl"}), environment_trust_lvl); DECLARE_VM_BUILTIN(name({"environment", "add"}), environment_add); From 872c148d4c6af3f89f2d895a9583ab5c121ce7bc Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Fri, 3 May 2019 18:16:23 -0400 Subject: [PATCH 10/36] fix(tactic/case): `case` fails when used with `let` #32 --- library/init/meta/interactive.lean | 1 + tests/lean/case_let.lean | 8 ++++++++ 2 files changed, 9 insertions(+) create mode 100644 tests/lean/case_let.lean diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 8885e32768..87f0444f57 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -659,6 +659,7 @@ private meta def find_case (goals : list expr) (ty : name) (idx : nat) (num_indi (find_case (some arg) arg) end | (lam _ _ _ e) := find_case case e + | (elet _ _ _ e) := find_case case e | (macro n args) := list.foldl (<|>) none $ args.map (find_case case) | _ := none end else none diff --git a/tests/lean/case_let.lean b/tests/lean/case_let.lean new file mode 100644 index 0000000000..0bf142b671 --- /dev/null +++ b/tests/lean/case_let.lean @@ -0,0 +1,8 @@ + +example (n m : ℕ) : n + m = m + n := +begin +let s := n + m, +induction n, +case nat.zero : {sorry}, -- error: could not find open goal of given case +case nat.succ : {sorry} +end From 1a1a5756a7f03dcdb956e5b5d2760ad5499e2721 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Fri, 3 May 2019 18:28:22 -0400 Subject: [PATCH 11/36] chore(build): avoid redundant builds [skip ci] --- .travis.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.travis.yml b/.travis.yml index 0c5ac08b0d..fc270eaf32 100644 --- a/.travis.yml +++ b/.travis.yml @@ -2,6 +2,9 @@ language: cpp sudo: true cache: apt dist: trusty +branches: + only: + - master group: deprecated-2017Q3 addons: apt: From dad53e7e80d778e9ab32f121a119ee5ffa2a5ff4 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Sat, 4 May 2019 14:39:16 -0400 Subject: [PATCH 12/36] fix(tests): add `expected` file for `case_let.lean` --- .gitignore | 1 + .travis.yml | 13 +++++++++++-- tests/lean/case_let.lean.expected.out | 1 + 3 files changed, 13 insertions(+), 2 deletions(-) create mode 100644 tests/lean/case_let.lean.expected.out diff --git a/.gitignore b/.gitignore index c951623a94..8d03439650 100644 --- a/.gitignore +++ b/.gitignore @@ -22,3 +22,4 @@ settings.json /library/init/version.lean CMakeSettings.json CppProperties.json +/_cache/ \ No newline at end of file diff --git a/.travis.yml b/.travis.yml index fc270eaf32..58e077804d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,10 +1,20 @@ language: cpp sudo: true -cache: apt +cache: + apt: true + directories: + - build/library/ + - build/kernel/ + - build/init/ + - build/frontends/ + - build/api/ + - build/util/ + - build/checker/ dist: trusty branches: only: - master + - debug-travis group: deprecated-2017Q3 addons: apt: @@ -116,7 +126,6 @@ before_install: fi script: - - set -e - mkdir -p build - cd build - if [[ $TESTCOV != ON ]]; then TESTCOV=OFF; fi diff --git a/tests/lean/case_let.lean.expected.out b/tests/lean/case_let.lean.expected.out new file mode 100644 index 0000000000..31e414b58f --- /dev/null +++ b/tests/lean/case_let.lean.expected.out @@ -0,0 +1 @@ +case_let.lean:2:0: warning: declaration '[anonymous]' uses sorry From fa6a121eb8b7eae72331468efef7942ee328d271 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Sat, 4 May 2019 20:53:01 -0400 Subject: [PATCH 13/36] fix(build): disable building other branches than master --- .travis.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index 58e077804d..332f52dd6d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -14,7 +14,6 @@ dist: trusty branches: only: - master - - debug-travis group: deprecated-2017Q3 addons: apt: From 5c76c03a1640fe20b93b35e73f3ca6669cc7d71b Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Sat, 4 May 2019 22:02:49 -0400 Subject: [PATCH 14/36] chore(build): restrict Travis tasks when building nightlies [skip ci] --- .travis.yml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/.travis.yml b/.travis.yml index 332f52dd6d..5210536f4b 100644 --- a/.travis.yml +++ b/.travis.yml @@ -42,6 +42,7 @@ matrix: FIRST=1 - os: linux + if: type != cron env: CMAKE_CXX_COMPILER=clang++-3.4 CMAKE_BUILD_TYPE=Release @@ -56,6 +57,7 @@ matrix: - *default_packages - g++-6 - gcc-6 + if: type != cron env: CMAKE_CXX_COMPILER=g++-6 CMAKE_BUILD_TYPE=Release @@ -63,6 +65,7 @@ matrix: - os: linux addons: *gcc6_addons + if: type != cron env: CMAKE_CXX_COMPILER=g++-6 CMAKE_BUILD_TYPE=Release @@ -70,6 +73,7 @@ matrix: - os: linux addons: *gcc6_addons + if: type != cron env: CMAKE_CXX_COMPILER=g++-6 CMAKE_BUILD_TYPE=Release @@ -82,6 +86,7 @@ matrix: packages: - *default_packages - z3 + if: type != cron env: CMAKE_CXX_COMPILER=g++-4.9 CMAKE_BUILD_TYPE=Release @@ -89,6 +94,7 @@ matrix: TEST_LEANPKG_REGISTRY=ON - os: linux + if: type != cron env: CMAKE_CXX_COMPILER=clang++-3.4 CMAKE_BUILD_TYPE=Debug @@ -96,6 +102,7 @@ matrix: - os: linux dist: precise + if: type != cron env: CMAKE_CXX_COMPILER=g++-4.9 CMAKE_BUILD_TYPE=Debug @@ -108,6 +115,7 @@ matrix: TEST_LEANPKG_REGISTRY=ON - os: osx + if: type != cron env: CMAKE_CXX_COMPILER=g++ CMAKE_BUILD_TYPE=Debug From 40912b44152c416db628dd0f32bc77d939503531 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Mon, 6 May 2019 23:39:45 -0400 Subject: [PATCH 15/36] feat(tactic/add_def_eqns): add a Lean function to access the equation compiler (#26) --- .gitignore | 3 +- .travis.yml | 9 +- library/init/meta/environment.lean | 5 + library/init/meta/expr.lean | 46 ++-- library/init/meta/tactic.lean | 50 +++- src/frontends/lean/decl_cmds.cpp | 2 +- src/frontends/lean/decl_util.cpp | 75 +++++- src/frontends/lean/decl_util.h | 25 +- src/frontends/lean/definition_cmds.cpp | 109 ++++++--- src/frontends/lean/definition_cmds.h | 2 + src/frontends/lean/elaborator.cpp | 38 +++ src/frontends/lean/parser.cpp | 48 ++-- src/frontends/lean/parser.h | 270 +++++++++++++-------- src/frontends/lean/util.cpp | 12 +- src/frontends/lean/util.h | 13 +- src/library/io_state.cpp | 2 + src/library/io_state.h | 1 + tests/lean/add_defn_eqns.lean | 126 ++++++++++ tests/lean/add_defn_eqns.lean.expected.out | 140 +++++++++++ 19 files changed, 763 insertions(+), 213 deletions(-) create mode 100644 tests/lean/add_defn_eqns.lean create mode 100644 tests/lean/add_defn_eqns.lean.expected.out diff --git a/.gitignore b/.gitignore index 8d03439650..1159106b7a 100644 --- a/.gitignore +++ b/.gitignore @@ -22,4 +22,5 @@ settings.json /library/init/version.lean CMakeSettings.json CppProperties.json -/_cache/ \ No newline at end of file +/build +/_cache/ diff --git a/.travis.yml b/.travis.yml index 5210536f4b..8d39b6ed35 100644 --- a/.travis.yml +++ b/.travis.yml @@ -2,14 +2,7 @@ language: cpp sudo: true cache: apt: true - directories: - - build/library/ - - build/kernel/ - - build/init/ - - build/frontends/ - - build/api/ - - build/util/ - - build/checker/ + ccache: true dist: trusty branches: only: diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean index ccfe23f29f..4801e39a7c 100644 --- a/library/init/meta/environment.lean +++ b/library/init/meta/environment.lean @@ -74,6 +74,11 @@ match env.get d with | exceptional.success _ := tt | exceptional.exception ._ _ := ff end + +meta constant add_defn_eqns (env : environment) (opt : options) + (lp_params : list name) (params : list expr) (sig : expr) + (eqns : list (list (expr ff) × expr)) (is_meta : bool) : exceptional environment + /-- Register the given name as a namespace, making it available to the `open` command -/ meta constant add_namespace : environment → name → environment /-- Return tt iff the given name is a namespace -/ diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index 013c4a3369..5c29e869db 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -21,26 +21,26 @@ else is_false (λ contra, pos.no_confusion contra (λ e₁ e₂, absurd e₁ h meta instance : has_to_format pos := ⟨λ ⟨l, c⟩, "⟨" ++ l ++ ", " ++ c ++ "⟩"⟩ -/-- Auxiliary annotation for binders (Lambda and Pi). +/-- Auxiliary annotation for binders (Lambda and Pi). This information is only used for elaboration. - The difference between `{}` and `⦃⦄` is how implicit arguments are treated that are *not* followed by explicit arguments. + The difference between `{}` and `⦃⦄` is how implicit arguments are treated that are *not* followed by explicit arguments. `{}` arguments are applied eagerly, while `⦃⦄` arguments are left partially applied: ```lean def foo {x : ℕ} : ℕ := x def bar ⦃x : ℕ⦄ : ℕ := x #check foo -- foo : ℕ #check bar -- bar : Π ⦃x : ℕ⦄, ℕ -``` +``` -/ inductive binder_info /- `(x : α)` -/ -| default +| default /- `{x : α}` -/ -| implicit +| implicit /- `⦃x:α⦄` -/ -| strict_implicit +| strict_implicit /- `[x : α]`. Should be inferred with typeclass resolution. -/ -| inst_implicit +| inst_implicit /- Auxiliary internal attribute used to mark local constants representing recursive functions in recursive equations and `match` statements. -/ | aux_decl @@ -55,11 +55,11 @@ instance : has_repr binder_info := end⟩ /-- Macros are basically "promises" to build an expr by some C++ code, you can't build them in Lean. You can unfold a macro and force it to evaluate. - They are used for + They are used for - `sorry`. - Term placeholders (`_`) in `pexpr`s. - - Expression annotations. See `expr.is_annotation`. - - Meta-recursive calls. Eg: + - Expression annotations. See `expr.is_annotation`. + - Meta-recursive calls. Eg: ``` meta def Y : (α → α) → α | f := f (Y f) ``` @@ -77,8 +77,8 @@ end⟩ -/ meta constant macro_def : Type -/-- An expression. eg ```(4+5)``. - +/-- An expression. eg ```(4+5)``. + The `elab` flag is indicates whether the `expr` has been elaborated and doesn't contain any placeholder macros. For example the equality `x = x` is represented in `expr ff` as ``app (app (const `eq _) x) x`` while in `expr tt` it is represented as ``app (app (app (const `eq _) t) x) x`` (one more argument). The VM replaces instances of this datatype with the C++ implementation. -/ @@ -87,10 +87,10 @@ meta inductive expr (elaborated : bool := tt) | var {} : nat → expr /- A type universe: `Sort u` -/ | sort {} : level → expr -/- A global constant. These include definitions, constants and inductive type stuff present +/- A global constant. These include definitions, constants and inductive type stuff present in the environment as well as hard-coded definitions. -/ | const {} : name → list level → expr -/- [WARNING] Do not trust the types for `mvar` and `local_const`, +/- [WARNING] Do not trust the types for `mvar` and `local_const`, they are sometimes dummy values. Use `tactic.infer_type` instead. -/ /- An `mvar` is a 'hole' yet to be filled in by the elaborator or tactic state. -/ | mvar (unique : name) (pretty : name) (type : expr) : expr @@ -105,7 +105,7 @@ they are sometimes dummy values. Use `tactic.infer_type` instead. -/ /- An explicit let binding. -/ | elet (var_name : name) (type : expr) (assignment : expr) (body : expr) : expr /- A macro, see the docstring for `macro_def`. - The list of expressions are local constants and metavariables that the macro depends on. + The list of expressions are local constants and metavariables that the macro depends on. -/ | macro : macro_def → list expr → expr @@ -118,7 +118,7 @@ meta constant expr.macro_def_name (d : macro_def) : name meta def expr.mk_var (n : nat) : expr := expr.var n /-- Expressions can be annotated using an annotation macro during compilation. -For example, a `have x:X, from p, q` expression will be compiled to `(λ x:X,q)(p)`, but nested in an annotation macro with the name `"have"`. +For example, a `have x:X, from p, q` expression will be compiled to `(λ x:X,q)(p)`, but nested in an annotation macro with the name `"have"`. These annotations have no real semantic meaning, but are useful for helping Lean's pretty printer. -/ meta constant expr.is_annotation : expr elab → option (name × expr elab) @@ -147,8 +147,8 @@ meta instance : has_to_format (expr elab) := ⟨λ e, e.to_string⟩ meta instance : has_coe_to_fun (expr elab) := { F := λ e, expr elab → expr elab, coe := λ e, expr.app e } -/-- Each expression created by Lean carries a hash. -This is calculated upon creation of the expression. +/-- Each expression created by Lean carries a hash. +This is calculated upon creation of the expression. Two structurally equal expressions will have the same hash. -/ meta constant expr.hash : expr → nat @@ -162,7 +162,7 @@ meta constant expr.fold {α : Type} : expr → α → (expr → nat → α → /-- `expr.replace e f` Traverse over an expr `e` with a function `f` which can decide to replace subexpressions or not. For each subexpression `s` in the expression tree, `f s n` is called where `n` is how many binders are present above the given subexpression `s`. - If `f s n` returns `none`, the children of `s` will be traversed. + If `f s n` returns `none`, the children of `s` will be traversed. Otherwise if `some s'` is returned, `s'` will replace `s` and this subexpression will not be traversed further. -/ meta constant expr.replace : expr → (expr → nat → option expr) → expr @@ -196,7 +196,7 @@ meta constant expr.has_local : expr → bool /-- `has_meta_var e` returns true iff `e` contains a metavariable. -/ meta constant expr.has_meta_var : expr → bool /-- `lower_vars e s d` lowers the free variables >= s in `e` by `d`. Note that this can cause variable clashes. - examples: + examples: - ``lower_vars `(#2 #1 #0) 1 1 = `(#1 #0 #0)`` - ``lower_vars `(λ x, #2 #1 #0) 1 1 = `(λ x, #1 #1 #0 )`` -/ @@ -207,7 +207,7 @@ meta constant expr.lift_vars : expr → nat → nat → expr protected meta constant expr.pos : expr elab → option pos /-- `copy_pos_info src tgt` copies position information from `src` to `tgt`. -/ meta constant expr.copy_pos_info : expr → expr → expr -/-- Returns `some n` when the given expression is a constant with the name `..._cnstr.n` +/-- Returns `some n` when the given expression is a constant with the name `..._cnstr.n` ``` is_internal_cnstr : expr → option unsigned |(const (mk_numeral n (mk_string "_cnstr" _)) _) := some n @@ -216,7 +216,7 @@ is_internal_cnstr : expr → option unsigned [NOTE] This is not used anywhere in core Lean. -/ meta constant expr.is_internal_cnstr : expr → option unsigned -/-- There is a macro called a "nat_value_macro" holding a natural number which are used during compilation. +/-- There is a macro called a "nat_value_macro" holding a natural number which are used during compilation. This function extracts that to a natural number. [NOTE] This is not used anywhere in Lean. -/ meta constant expr.get_nat_value : expr → option nat /-- Get a list of all of the universe parameters that the given expression depends on. -/ @@ -517,7 +517,7 @@ meta def to_raw_fmt : expr elab → format | (elet n g e f) := p ["elet", to_fmt n, to_raw_fmt g, to_raw_fmt e, to_raw_fmt f] | (macro d args) := sbracket (format.join (list.intersperse " " ("macro" :: to_fmt (macro_def_name d) :: args.map to_raw_fmt))) -/-- Fold an accumulator `a` over each subexpression in the expression `e`. +/-- Fold an accumulator `a` over each subexpression in the expression `e`. The `nat` passed to `fn` is the number of binders above the subexpression. -/ meta def mfold {α : Type} {m : Type → Type} [monad m] (e : expr) (a : α) (fn : expr → nat → α → m α) : m α := fold e (return a) (λ e n a, a >>= fn e n) diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 323cb18d43..0aaddba3fb 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -40,7 +40,7 @@ meta instance : has_to_string tactic_state := You use this to: - View and modify the local goals and hypotheses in the prover's state. - Invoke type checking and elaboration of terms. - - View and modify the environment. + - View and modify the environment. - Build new tactics out of existing ones such as `simp` and `rewrite`. -/ @[reducible] meta def tactic := interaction_monad tactic_state @@ -290,7 +290,7 @@ do s ← read, trace $ to_fmt s /-- A parameter representing how aggressively definitions should be unfolded when trying to decide if two terms match, unify or are definitionally equal. -By default, theorem declarations are never unfolded. +By default, theorem declarations are never unfolded. - `all` will unfold everything, including macros and theorems. Except projection macros. - `semireducible` will unfold everything except theorems and definitions tagged as irreducible. - `instances` will unfold all class instance definitions and definitions tagged with reducible. @@ -322,7 +322,7 @@ meta constant intron : nat → tactic unit meta constant clear : expr → tactic unit /-- `revert_lst : list expr → tactic nat` is the reverse of `intron`. It takes a local constant `c` and puts it back as bound by a `pi` or `elet` of the main target. If there are other local constants that depend on `c`, these are also reverted. Because of this, the `nat` that is returned is the actual number of reverted local constants. -Example: with `x : ℕ, h : P(x) ⊢ T(x)`, `revert_lst [x]` returns `2` and produces the state ` ⊢ Π x, P(x) → T(x)`. +Example: with `x : ℕ, h : P(x) ⊢ T(x)`, `revert_lst [x]` returns `2` and produces the state ` ⊢ Π x, P(x) → T(x)`. -/ meta constant revert_lst : list expr → tactic nat /-- Return `e` in weak head normal form with respect to the given transparency setting. @@ -355,7 +355,7 @@ meta constant resolve_name : name → tactic pexpr /-- Return the hypothesis in the main goal. Fail if tactic_state does not have any goal left. -/ meta constant local_context : tactic (list expr) /-- Get a fresh name that is guaranteed to not be in use in the local context. - If `n` is provided and `n` is not in use, then `n` is returned. + If `n` is provided and `n` is not in use, then `n` is returned. Otherwise a number `i` is appended to give `"n_i"`. -/ meta constant get_unused_name (n : name := `_x) (i : option nat := none) : tactic name @@ -444,7 +444,7 @@ meta constant rotate_left : nat → tactic unit meta constant get_goals : tactic (list expr) /-- Replace the current list of goals with the given one. Each expr in the list should be a metavariable. Any assigned metavariables will be ignored.-/ meta constant set_goals : list expr → tactic unit -/-- How to order the new goals made from an `apply` tactic. +/-- How to order the new goals made from an `apply` tactic. Supposing we were applying `e : ∀ (a:α) (p : P(a)), Q` - `non_dep_first` would produce goals `⊢ P(?m)`, `⊢ α`. It puts the P goal at the front because none of the arguments after `p` in `e` depend on `p`. It doesn't matter what the result `Q` depends on. - `non_dep_only` would produce goal `⊢ P(?m)`. @@ -667,9 +667,9 @@ target >>= whnf >>= change meta def unsafe_change (e : expr) : tactic unit := change e ff -/-- Pi or elet introduction. +/-- Pi or elet introduction. Given the tactic state `⊢ Π x : α, Y`, ``intro `hello`` will produce the state `hello : α ⊢ Y[x/hello]`. -Returns the new local constant. Similarly for `elet` expressions. +Returns the new local constant. Similarly for `elet` expressions. If the target is not a Pi or elet it will try to put it in WHNF. -/ meta def intro (n : name) : tactic expr := @@ -723,7 +723,7 @@ meta def to_expr_strict (q : pexpr) : tactic expr := to_expr q /-- -Example: with `x : ℕ, h : P(x) ⊢ T(x)`, `revert x` returns `2` and produces the state ` ⊢ Π x, P(x) → T(x)`. +Example: with `x : ℕ, h : P(x) ⊢ T(x)`, `revert x` returns `2` and produces the state ` ⊢ Π x, P(x) → T(x)`. -/ meta def revert (l : expr) : tactic nat := revert_lst [l] @@ -1326,6 +1326,40 @@ updateex_env $ λe, e.add_inductive n ls p ty is is_meta meta def add_meta_definition (n : name) (lvls : list name) (type value : expr) : tactic unit := add_decl (declaration.defn n lvls type value reducibility_hints.abbrev ff) +/-- `add_defn_equations` adds a definition specified by a list of equations. + + The arguments: + * `lp`: list of universe parameters + * `params`: list of parameters (binders before the colon); + * `fn`: a local constant giving the name and type of the declaration + (with `params` in the local context); + * `eqns`: a list of equations, each of which is a list of patterns + (constructors applied to new local constants) and the branch + expression; + * `is_meta`: is the definition meta? + + + `add_defn_equations` can be used as: + + do my_add ← mk_local_def `my_add `(ℕ → ℕ), + a ← mk_local_def `a ℕ, + b ← mk_local_def `b ℕ, + add_defn_equations [a] my_add + [ ([``(nat.zero)], a), + ([``(nat.succ %%b)], my_add b) ]) + ff -- non-meta + + to create the following definition: + + def my_add (a : ℕ) : ℕ → ℕ + | nat.zero := a + | (nat.succ b) := my_add b +-/ +meta def add_defn_equations (lp : list name) (params : list expr) (fn : expr) + (eqns : list (list pexpr × expr)) (is_meta : bool) : tactic unit := +do opt ← get_options, + updateex_env $ λ e, e.add_defn_eqns opt lp params fn eqns is_meta + meta def rename (curr : name) (new : name) : tactic unit := do h ← get_local curr, n ← revert h, diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index c5e38bbec3..d34a8e41e1 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -35,7 +35,7 @@ Author: Leonardo de Moura namespace lean { // TODO(Leo): delete -void update_univ_parameters(parser & p, buffer & lp_names, name_set const & found); +void update_univ_parameters(parser_info & p, buffer & lp_names, name_set const & found); static environment declare_universe(parser & p, environment env, name const & n, bool local) { if (local) { diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp index 0ab129ad8a..b65b6d384b 100644 --- a/src/frontends/lean/decl_util.cpp +++ b/src/frontends/lean/decl_util.cpp @@ -45,7 +45,8 @@ bool parse_univ_params(parser & p, buffer & lp_names) { } } -expr parse_single_header(parser & p, declaration_name_scope & scope, buffer & lp_names, buffer & params, +expr parse_single_header(parser & p, declaration_name_scope & scope, + buffer & lp_names, buffer & params, bool is_example, bool is_instance) { auto c_pos = p.pos(); name c_name; @@ -93,6 +94,45 @@ expr parse_single_header(parser & p, declaration_name_scope & scope, buffer & lp_names, buffer & params, + bool is_example, bool is_instance) { + auto c_pos = p.pos(); + name c_name; + if (is_example) { + c_name = "_example"; + scope.set_name(c_name); + } else { + lp_names = p.get_univ_params(); + c_name = p.get_name(); + scope.set_name(c_name); + } + + params = p.get_binders(); + for (expr const & param : params) + p.add_local(param); + expr type = p.get_type(); + if (is_instance && c_name.is_anonymous()) { + if (used_match_idx()) + throw parser_error("invalid instance, pattern matching cannot be used in the type of anonymous instance declarations", c_pos); + expr it = type; + while (is_pi(it)) it = binding_body(it); + expr const & C = get_app_fn(it); + name ns = get_namespace(p.env()); + if (is_constant(C) && !ns.is_anonymous()) { + c_name = const_name(C); + scope.set_name(c_name); + } else if (is_constant(C) && is_app(it) && is_constant(get_app_fn(app_arg(it)))) { + c_name = const_name(get_app_fn(app_arg(it))) + const_name(C); + scope.set_name(c_name); + } else { + p.maybe_throw_error({"failed to synthesize instance name, name should be provided explicitly", c_pos}); + c_name = mk_unused_name(p.env(), "_inst"); + } + } + lean_assert(!c_name.is_anonymous()); + return mk_local(c_name, type); +} + void parse_mutual_header(parser & p, buffer & lp_names, buffer & cs, buffer & params) { parse_univ_params(p, lp_names); while (true) { @@ -164,7 +204,7 @@ name_set collect_univ_params_ignoring_tactics(expr const & e, name_set const & l variable [decidable_eq A] */ -void collect_annonymous_inst_implicit(parser const & p, collected_locals & locals) { +void collect_annonymous_inst_implicit(parser_info const & p, collected_locals & locals) { buffer> entries; to_buffer(p.get_local_entries(), entries); unsigned i = entries.size(); @@ -188,7 +228,7 @@ void collect_annonymous_inst_implicit(parser const & p, collected_locals & local } /** \brief Sort local names by order of occurrence, and copy the associated parameters to ps */ -void sort_locals(buffer const & locals, parser const & p, buffer & ps) { +void sort_locals(buffer const & locals, parser_info const & p, buffer & ps) { buffer extra; name_set explicit_param_names; for (expr const & p : ps) { @@ -217,7 +257,7 @@ void sort_locals(buffer const & locals, parser const & p, buffer & p } /** TODO(Leo): mark as static */ -void update_univ_parameters(parser & p, buffer & lp_names, name_set const & found) { +void update_univ_parameters(parser_info & p, buffer & lp_names, name_set const & found) { unsigned old_sz = lp_names.size(); found.for_each([&](name const & n) { if (std::find(lp_names.begin(), lp_names.begin() + old_sz, n) == lp_names.begin() + old_sz) @@ -253,7 +293,7 @@ expr replace_local_preserving_pos_info(expr const & e, expr const & from, expr c return replace_locals_preserving_pos_info(e, 1, &from, &to); } -void collect_implicit_locals(parser & p, buffer & lp_names, buffer & params, buffer const & all_exprs) { +void collect_implicit_locals(parser_info & p, buffer & lp_names, buffer & params, buffer const & all_exprs) { collected_locals locals; buffer include_vars; name_set lp_found; @@ -296,12 +336,12 @@ void collect_implicit_locals(parser & p, buffer & lp_names, buffer & } } -void collect_implicit_locals(parser & p, buffer & lp_names, buffer & params, std::initializer_list const & all_exprs) { +void collect_implicit_locals(parser_info & p, buffer & lp_names, buffer & params, std::initializer_list const & all_exprs) { buffer tmp; tmp.append(all_exprs.size(), all_exprs.begin()); collect_implicit_locals(p, lp_names, params, tmp); } -void collect_implicit_locals(parser & p, buffer & lp_names, buffer & params, expr const & e) { +void collect_implicit_locals(parser_info & p, buffer & lp_names, buffer & params, expr const & e) { buffer all_exprs; all_exprs.push_back(e); collect_implicit_locals(p, lp_names, params, all_exprs); } @@ -316,7 +356,9 @@ void elaborate_params(elaborator & elab, buffer const & params, buffer const & lp_names, buffer const & var_params) { +environment add_local_ref(parser_info & p, environment const & env, name const & c_name, + name const & c_real_name, buffer const & lp_names, + buffer const & var_params) { buffer params; buffer lps; for (name const & u : lp_names) { @@ -412,6 +454,9 @@ declaration_info_scope::declaration_info_scope(name const & ns, decl_cmd_kind ki info.m_next_match_idx = 1; } +declaration_info_scope::declaration_info_scope(environment const & env, decl_cmd_kind kind, decl_modifiers const & modifiers): + declaration_info_scope(get_namespace(env), kind, modifiers) {} + declaration_info_scope::declaration_info_scope(parser const & p, decl_cmd_kind kind, decl_modifiers const & modifiers): declaration_info_scope(get_namespace(p.env()), kind, modifiers) {} @@ -555,4 +600,18 @@ restore_decl_meta_scope::~restore_decl_meta_scope() { definition_info & info = get_definition_info(); info.m_is_meta = m_old_is_meta; } + +root_scope::root_scope() { + definition_info & info = get_definition_info(); + m_old_prefix = info.m_prefix; + m_old_actual_prefix = info.m_actual_prefix; + info.m_prefix = {}; + info.m_actual_prefix = {}; +} + +root_scope::~root_scope() { + definition_info & info = get_definition_info(); + info.m_prefix = m_old_prefix; + info.m_actual_prefix = m_old_actual_prefix; +} } diff --git a/src/frontends/lean/decl_util.h b/src/frontends/lean/decl_util.h index 32927bee4f..e1713ac6dd 100644 --- a/src/frontends/lean/decl_util.h +++ b/src/frontends/lean/decl_util.h @@ -11,6 +11,8 @@ Author: Leonardo de Moura #include "frontends/lean/decl_attributes.h" namespace lean { class parser; +class parser_info; +class dummy_def_parser; class elaborator; enum class decl_cmd_kind { Theorem, Definition, Example, Instance, Var, Abbreviation }; @@ -35,6 +37,7 @@ struct decl_modifiers { class declaration_info_scope { declaration_info_scope(name const & ns, decl_cmd_kind kind, decl_modifiers const & modifiers); public: + declaration_info_scope(environment const & p, decl_cmd_kind kind, decl_modifiers const & modifiers); declaration_info_scope(parser const & p, decl_cmd_kind kind, decl_modifiers const & modifiers); ~declaration_info_scope(); bool gen_aux_lemmas() const; @@ -107,6 +110,17 @@ class restore_decl_meta_scope { ~restore_decl_meta_scope(); }; +/** \brief Auxiliary scope to clear the prefixes when calling parsers + inside tactics. */ +class root_scope { + name m_old_actual_prefix; + name m_old_prefix; +public: + root_scope(); + ~root_scope(); +}; + + /** \brief Return true if the current scope used match-expressions */ bool used_match_idx(); @@ -128,6 +142,9 @@ bool parse_univ_params(parser & p, buffer & lp_names); \remark Caller is responsible for using: parser::local_scope scope2(p, env); */ expr parse_single_header(parser & p, declaration_name_scope & s, buffer & lp_names, buffer & params, bool is_example = false, bool is_instance = false); + +expr parse_single_header(dummy_def_parser & p, declaration_name_scope & s, buffer & lp_names, buffer & params, + bool is_example = false, bool is_instance = false); /** \brief Parse the header of a mutually recursive declaration. It has the form {u_1 ... u_k} id_1, ... id_n (params) @@ -153,9 +170,9 @@ pair parse_inner_header(parser & p, name const & c_expect /** \brief Add section/namespace parameters (and universes) used by params and all_exprs. We also add parameters included using the command 'include'. lp_names and params are input/output. */ -void collect_implicit_locals(parser & p, buffer & lp_names, buffer & params, buffer const & all_exprs); -void collect_implicit_locals(parser & p, buffer & lp_names, buffer & params, std::initializer_list const & all_exprs); -void collect_implicit_locals(parser & p, buffer & lp_names, buffer & params, expr const & e); +void collect_implicit_locals(parser_info & p, buffer & lp_names, buffer & params, buffer const & all_exprs); +void collect_implicit_locals(parser_info & p, buffer & lp_names, buffer & params, std::initializer_list const & all_exprs); +void collect_implicit_locals(parser_info & p, buffer & lp_names, buffer & params, expr const & e); /** \brief Elaborate the types of the parameters \c params, and update the elaborator local context using them. Store the elaborated parameters at new_params. @@ -166,7 +183,7 @@ void elaborate_params(elaborator & elab, buffer const & params, buffer (c_real_name.{level_params} params) level_params and params are subsets of lp_names and var_params that were declared using the parameter command. */ -environment add_local_ref(parser & p, environment const & env, name const & c_name, name const & c_real_name, +environment add_local_ref(parser_info & p, environment const & env, name const & c_name, name const & c_real_name, buffer const & lp_names, buffer const & var_params); /** \brief Add alias for new declaration. */ diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index aa1abb7be9..06f409b2dd 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -85,7 +85,7 @@ optional parse_using_well_founded(parser & p) { } } -expr mk_equations(parser & p, buffer const & fns, +expr mk_equations(parser_info & p, buffer const & fns, buffer const & fn_full_names, buffer const & fn_prv_names, buffer const & eqs, optional const & wf_tacs, pos_info const & pos) { buffer new_eqs; @@ -100,7 +100,7 @@ expr mk_equations(parser & p, buffer const & fns, } } -expr mk_equations(parser & p, expr const & fn, name const & full_name, name const & full_prv_name, buffer const & eqs, +expr mk_equations(parser_info & p, expr const & fn, name const & full_name, name const & full_prv_name, buffer const & eqs, optional const & wf_tacs, pos_info const & pos) { buffer fns; fns.push_back(fn); buffer full_names; full_names.push_back(full_name); @@ -178,7 +178,7 @@ static void finalize_definition(elaborator & elab, buffer const & params, lp_names.append(implicit_lp_names); } -static certified_declaration check(parser & p, environment const & env, name const & c_name, declaration const & d, pos_info const & pos) { +static certified_declaration check(parser_info const & p, environment const & env, name const & c_name, declaration const & d, pos_info const & pos) { try { time_task _("type checking", p.mk_message(pos, INFORMATION), p.get_options(), c_name); return ::lean::check(env, d); @@ -215,7 +215,7 @@ static bool check_noncomputable(bool ignore_noncomputable, environment const & e return true; } -static environment compile_decl(parser & p, environment const & env, +static environment compile_decl(parser_info const & p, environment const & env, name const & c_name, name const & c_real_name, pos_info const & pos) { try { time_task _("compilation", p.mk_message(message_severity::INFORMATION), p.get_options(), c_real_name); @@ -231,7 +231,7 @@ static environment compile_decl(parser & p, environment const & env, } static pair -declare_definition(parser & p, environment const & env, decl_cmd_kind kind, buffer const & lp_names, +declare_definition(parser_info const & p, environment const & env, decl_cmd_kind kind, buffer const & lp_names, name const & c_name, name const & prv_name, expr type, optional val, task const & proof, cmd_meta const & meta, bool is_abbrev, pos_info const & pos) { name c_real_name; @@ -520,8 +520,10 @@ static environment mutual_definition_cmd_core(parser & p, decl_cmd_kind kind, cm - actual_name for the kernel declaration. Note that mlocal_pp_name(fn) and actual_name are different for scoped/private declarations. */ -static std::tuple parse_definition(parser & p, buffer & lp_names, buffer & params, - bool is_example, bool is_instance, bool is_meta, bool is_abbrev) { +std::tuple +parser::parse_definition(buffer & lp_names, buffer & params, + bool is_example, bool is_instance, bool is_meta, bool is_abbrev) { + parser & p = *this; parser::local_scope scope1(p); auto header_pos = p.pos(); time_task _("parsing", p.mk_message(header_pos, INFORMATION), p.get_options()); @@ -569,6 +571,43 @@ static std::tuple parse_definition(parser & p, buffer & return std::make_tuple(fn, val, scope2.get_actual_name()); } +std::tuple +dummy_def_parser::parse_definition(buffer & lp_names, buffer & params, + bool is_example, bool is_instance, bool, bool) { + dummy_def_parser & p = *this; + parser::local_scope scope1(p); + auto header_pos = p.pos(); + time_task _("parsing", p.mk_message(header_pos, INFORMATION), p.get_options()); + declaration_name_scope scope2; + expr fn = parse_single_header(p, scope2, lp_names, params, is_example, is_instance); + expr val; + { + declaration_name_scope scope2("_main"); + fn = mk_local(mlocal_name(fn), mlocal_pp_name(fn), mlocal_type(fn), mk_rec_info(true)); + p.add_local(fn); + buffer eqns; + if (p.get_val().empty()) { + eqns.push_back(mk_no_equation()); + } else { + for (pair, expr> const &eq : p.get_val()) { + buffer pat; expr rhs; + collected_locals cl; + std::tie(pat, rhs) = eq; + for (auto p : pat) { + collect_locals(p, cl); } + eqns.push_back(lean::Fun(cl.get_collected(), + mk_equation(mk_app(mk_explicit(fn), pat), + lean::instantiate(rhs, fn)), + p)); + } + } + optional wf_tacs = p.get_well_founded_tac(); + val = mk_equations(p, fn, scope2.get_name(), scope2.get_actual_name(), eqns, wf_tacs, header_pos); + } + collect_implicit_locals(p, lp_names, params, {mlocal_type(fn), val}); + return std::make_tuple(fn, val, scope2.get_actual_name()); +} + static void replace_params(buffer const & params, buffer const & new_params, expr & fn, expr & val) { expr fn_type = replace_locals_preserving_pos_info(mlocal_type(fn), params, new_params); expr new_fn = update_mlocal(fn, fn_type); @@ -593,7 +632,7 @@ static expr_pair elaborate_definition_core(elaborator & elab, decl_cmd_kind kind } } -static expr_pair elaborate_definition(parser & p, elaborator & elab, decl_cmd_kind kind, expr const & fn, expr const & val, pos_info const & pos) { +static expr_pair elaborate_definition(parser_info & p, elaborator & elab, decl_cmd_kind kind, expr const & fn, expr const & val, pos_info const & pos) { time_task _("elaboration", p.mk_message(pos, INFORMATION), p.get_options(), mlocal_pp_name(fn)); return elaborate_definition_core(elab, kind, fn, val); } @@ -722,13 +761,13 @@ static bool is_rfl_preexpr(expr const & e) { return is_constant(e, get_rfl_name()); } -environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta meta) { +environment single_definition_cmd_core(parser_info & p, decl_cmd_kind kind, cmd_meta meta) { buffer lp_names; buffer params; expr fn, val; auto header_pos = p.pos(); module::scope_pos_info scope_pos(header_pos); - declaration_info_scope scope(p, kind, meta.m_modifiers); + declaration_info_scope scope(p.env(), kind, meta.m_modifiers); environment env = p.env(); private_name_scope prv_scope(meta.m_modifiers.m_is_private, env); bool is_example = (kind == decl_cmd_kind::Example); @@ -743,7 +782,7 @@ environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta meta.m_attrs.set_attribute(env, "reducible"); } name prv_name; - std::tie(fn, val, prv_name) = parse_definition(p, lp_names, params, is_example, is_instance, meta.m_modifiers.m_is_meta, is_abbrev); + std::tie(fn, val, prv_name) = p.parse_definition(lp_names, params, is_example, is_instance, meta.m_modifiers.m_is_meta, is_abbrev); auto begin_pos = p.cmd_pos(); auto end_pos = p.pos(); @@ -754,7 +793,7 @@ environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta if (p.get_break_at_pos()) return p.env(); - bool recover_from_errors = true; + bool recover_from_errors = p.m_error_recovery; elaborator elab(env, p.get_options(), get_namespace(env) + mlocal_pp_name(fn), metavar_context(), local_context(), recover_from_errors); buffer new_params; elaborate_params(elab, params, new_params); @@ -837,25 +876,37 @@ environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta /* Apply attributes last so that they may access any information on the new decl */ return meta.m_attrs.apply(new_env, p.ios(), c_real_name); }; - - try { - return process(val); - } catch (throwable & ex) { - // Even though we catch exceptions during elaboration, there can still be other exceptions, - // e.g. when adding a declaration to the environment. - - // If we have already logged an error during elaboration, don't - // bother showing the less helpful kernel exception - if (!lt.get().has_entry_now(is_error_message)) - p.mk_message(header_pos, ERROR).set_exception(ex).report(); - // As a last resort, try replacing the definition body with `sorry`. - // If that doesn't work either, just silently give up since we have - // already logged at least one error. + if (p.m_error_recovery) { try { - return process(p.mk_sorry(header_pos, true)); - } catch (...) { - return env; + return process(val); + } catch (throwable & ex) { + // Even though we catch exceptions during elaboration, there can still be other exceptions, + // e.g. when adding a declaration to the environment. + + // If we have already logged an error during elaboration, don't + // bother showing the less helpful kernel exception + if (!lt.get().has_entry_now(is_error_message)) + p.mk_message(header_pos, ERROR).set_exception(ex).report(); + // As a last resort, try replacing the definition body with `sorry`. + // If that doesn't work either, just silently give up since we have + // already logged at least one error. + try { + return process(p.mk_sorry(header_pos, true)); + } catch (...) { + return env; + } } + } else { + auto r = process(val); + lt.get().for_each([&] (log_tree::node const & n) { + for (auto & e : n.get_entries()) { + if (auto msg = dynamic_cast(e.get())) { + if (msg->is_error()) { + throw throwable(msg->get_text()); + } } } + return true; } ); + + return r; } } diff --git a/src/frontends/lean/definition_cmds.h b/src/frontends/lean/definition_cmds.h index c9d4dfd917..b9bd320aab 100644 --- a/src/frontends/lean/definition_cmds.h +++ b/src/frontends/lean/definition_cmds.h @@ -11,5 +11,7 @@ Author: Leonardo de Moura namespace lean { environment definition_cmd_core(parser & p, decl_cmd_kind k, cmd_meta const & meta); +environment single_definition_cmd_core(parser_info & p, decl_cmd_kind kind, cmd_meta meta); + environment ensure_decl_namespaces(environment const & env, name const & full_n); } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 354d850db3..e00b15593b 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -47,6 +47,11 @@ Author: Leonardo de Moura #include "library/delayed_abstraction.h" #include "library/vm/vm_name.h" #include "library/vm/vm_expr.h" +#include "library/vm/vm_environment.h" +#include "library/vm/vm_exceptional.h" +#include "library/vm/vm_options.h" +#include "library/vm/vm_option.h" +#include "library/vm/vm_list.h" #include "library/compiler/vm_compiler.h" #include "library/tactic/kabstract.h" #include "library/tactic/unfold_tactic.h" @@ -58,7 +63,9 @@ Author: Leonardo de Moura #include "library/inductive_compiler/ginductive.h" #include "frontends/lean/builtin_exprs.h" #include "frontends/lean/brackets.h" +#include "frontends/lean/definition_cmds.h" #include "frontends/lean/util.h" +#include "frontends/lean/parser.h" #include "frontends/lean/prenum.h" #include "frontends/lean/structure_cmd.h" #include "frontends/lean/structure_instance.h" @@ -4294,6 +4301,35 @@ static vm_obj tactic_save_type_info(vm_obj const &, vm_obj const & _e, vm_obj co return tactic::mk_success(s); } +static vm_obj environment_add_defn_eqns(vm_obj const &_env, vm_obj const &_opts, + vm_obj const &_lp_names, vm_obj const &_params, + vm_obj const &_sig, vm_obj const &_eqns, + vm_obj const &_meta ) { + try { + environment env = lean::to_env(_env); + cmd_meta meta; + meta.m_modifiers.m_is_meta = lean::to_bool(_meta); + auto kind = decl_cmd_kind::Definition; + root_scope scope; + dummy_def_parser p(env, lean::to_options(_opts)); + expr sig = to_expr(_sig); + p.m_name = mlocal_pp_name(sig); + p.m_type = mk_as_is(mlocal_type(sig)); + lean::to_buffer_name(_lp_names, p.m_lp_params); + to_buffer_expr(_params, p.m_params); + for (vm_obj const * it = &_eqns; !is_simple(*it); it = &cfield(*it, 1)) { + auto o = cfield(*it, 0); + buffer pat; + to_buffer_expr(cfield(o, 0), pat); + p.m_val.push_back(std::pair, expr>(std::move(pat), mk_as_is(abstract(to_expr(cfield(o, 1)), sig)))); + } + return mk_vm_exceptional_success(to_obj(single_definition_cmd_core(p, kind, meta))); + } catch (throwable & ex) { + return mk_vm_exceptional_exception(ex); + } +} + + void initialize_elaborator() { g_elab_strategy = new name("elab_strategy"); register_trace_class("elaborator"); @@ -4331,6 +4367,8 @@ void initialize_elaborator() { register_incompatible("elab_simple", "elab_as_eliminator"); register_incompatible("elab_with_expected_type", "elab_as_eliminator"); + DECLARE_VM_BUILTIN(name({"environment", "add_defn_eqns"}), environment_add_defn_eqns); + DECLARE_VM_BUILTIN(name({"tactic", "save_type_info"}), tactic_save_type_info); DECLARE_VM_BUILTIN(name({"tactic", "resolve_name"}), tactic_resolve_local_name); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 8ef19931f8..1c7035faf6 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -87,22 +87,22 @@ bool get_parser_show_errors(options const & opts) { // ========================================== -parser::local_scope::local_scope(parser & p, bool save_options): +parser_info::local_scope::local_scope(parser_info & p, bool save_options): m_p(p), m_env(p.env()) { m_p.push_local_scope(save_options); } -parser::local_scope::local_scope(parser & p, environment const & env): +parser_info::local_scope::local_scope(parser_info & p, environment const & env): m_p(p), m_env(p.env()) { m_p.m_env = env; m_p.push_local_scope(); } -parser::local_scope::local_scope(parser & p, optional const & env): +parser_info::local_scope::local_scope(parser_info & p, optional const & env): m_p(p), m_env(p.env()) { if (env) m_p.m_env = *env; m_p.push_local_scope(); } -parser::local_scope::~local_scope() { +parser_info::local_scope::~local_scope() { m_p.pop_local_scope(); m_p.m_env = m_env; } @@ -156,7 +156,7 @@ parser::parser(environment const & env, io_state const & ios, module_loader const & import_fn, std::istream & strm, std::string const & file_name, bool use_exceptions) : - m_env(env), m_ngen(*g_frontend_fresh), m_ios(ios), + parser_info(env, ios), m_ngen(*g_frontend_fresh), m_use_exceptions(use_exceptions), m_import_fn(import_fn), m_file_name(file_name), @@ -228,11 +228,11 @@ void parser::scan() { m_curr = m_scanner.scan(m_env); } -expr parser::mk_sorry(pos_info const & p, bool synthetic) { +expr parser_info::mk_sorry(pos_info const & p, bool synthetic) { return save_pos(::lean::mk_sorry(mk_Prop(), synthetic), p); } -void parser::updt_options() { +void parser_info::updt_options() { m_profile = get_profiler(m_ios.get_options()); m_show_errors = get_parser_show_errors(m_ios.get_options()); } @@ -446,13 +446,13 @@ expr parser::mk_app(std::initializer_list const & args, pos_info const & p return r; } -parser_scope parser::mk_parser_scope(optional const & opts) { +parser_scope parser_info::mk_parser_scope(optional const & opts) { return parser_scope(opts, m_level_variables, m_variables, m_include_vars, m_next_inst_idx, m_has_params, m_local_level_decls, m_local_decls); } -void parser::restore_parser_scope(parser_scope const & s) { +void parser_info::restore_parser_scope(parser_scope const & s) { if (s.m_options) { m_ios.set_options(*s.m_options); updt_options(); @@ -466,25 +466,25 @@ void parser::restore_parser_scope(parser_scope const & s) { m_next_inst_idx = s.m_next_inst_idx; } -void parser::push_local_scope(bool save_options) { +void parser_info::push_local_scope(bool save_options) { optional opts; if (save_options) opts = m_ios.get_options(); m_parser_scope_stack = cons(mk_parser_scope(opts), m_parser_scope_stack); } -void parser::pop_local_scope() { +void parser_info::pop_local_scope() { lean_assert(m_parser_scope_stack); auto s = head(m_parser_scope_stack); restore_parser_scope(s); m_parser_scope_stack = tail(m_parser_scope_stack); } -void parser::clear_expr_locals() { +void parser_info::clear_expr_locals() { m_local_decls = local_expr_decls(); } -void parser::add_local_level(name const & n, level const & l, bool is_variable) { +void parser_info::add_local_level(name const & n, level const & l, bool is_variable) { if (m_local_level_decls.contains(n)) maybe_throw_error({sstream() << "invalid universe declaration, '" << n << "' shadows a local universe", pos()}); m_local_level_decls.insert(n, l); @@ -494,7 +494,7 @@ void parser::add_local_level(name const & n, level const & l, bool is_variable) } } -void parser::add_local_expr(name const & n, expr const & p, bool is_variable) { +void parser_info::add_local_expr(name const & n, expr const & p, bool is_variable) { if (!m_in_quote) { // HACK: Certainly not in a pattern. We need this information early in `builtin_exprs::parse_quoted_expr`. // Without it, the quotation would be elaborated only in `patexpr_to_expr`, with the local not being @@ -512,7 +512,7 @@ void parser::add_local_expr(name const & n, expr const & p, bool is_variable) { } } -environment parser::add_local_ref(environment const & env, name const & n, expr const & ref) { +environment parser_info::add_local_ref(environment const & env, name const & n, expr const & ref) { add_local_expr(n, ref, false); if (is_as_atomic(ref)) { buffer args; @@ -544,20 +544,20 @@ static void check_no_metavars(name const & n, expr const & e) { } } -void parser::add_variable(name const & n, expr const & v) { +void parser_info::add_variable(name const & n, expr const & v) { lean_assert(is_local(v)); check_no_metavars(n, v); add_local_expr(n, v, true); } -void parser::add_parameter(name const & n, expr const & p) { +void parser_info::add_parameter(name const & n, expr const & p) { lean_assert(is_local(p)); check_no_metavars(n, p); add_local_expr(n, p, false); m_has_params = true; } -bool parser::is_local_decl(expr const & l) { +bool parser_info::is_local_decl(expr const & l) { lean_assert(is_local(l)); // TODO(Leo): add a name_set with internal ids if this is a bottleneck for (pair const & p : m_local_decls.get_entries()) { @@ -567,7 +567,7 @@ bool parser::is_local_decl(expr const & l) { return false; } -bool parser::update_local_binder_info(name const & n, binder_info const & bi) { +bool parser_info::update_local_binder_info(name const & n, binder_info const & bi) { auto it = get_local(n); if (!it || !is_local(*it)) return false; @@ -610,17 +610,17 @@ bool parser::update_local_binder_info(name const & n, binder_info const & bi) { return true; } -unsigned parser::get_local_index(name const & n) const { +unsigned parser_info::get_local_index(name const & n) const { return m_local_decls.find_idx(n); } -void parser::get_include_variables(buffer & vars) const { +void parser_info::get_include_variables(buffer & vars) const { m_include_vars.for_each([&](name const & n) { vars.push_back(*get_local(n)); }); } -list parser::locals_to_context() const { +list parser_info::locals_to_context() const { return map_filter(m_local_decls.get_entries(), [](pair const & p, expr & out) { out = p.second; @@ -2631,6 +2631,10 @@ void parser::init_scanner() { } } +void dummy_def_parser::maybe_throw_error(parser_error && err) { + throw std::move(err); +} + void parser::maybe_throw_error(parser_error && err) { if (m_error_recovery) { auto err_pos = err.get_pos() ? *err.get_pos() : pos(); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 22bfce11eb..e3937ffa55 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -35,31 +35,129 @@ class metavar_context; class local_context_adapter; class scope_message_context; -class parser : public abstract_parser { +class parser_info { +protected: environment m_env; - name_generator m_ngen; + local_expr_decls m_local_decls; + name_set m_level_variables; + name_set m_variables; // subset of m_local_decls that is marked as variables + local_level_decls m_local_level_decls; + bool m_has_params; // true context context contains parameters + name_set m_include_vars; // subset of m_local_decls that is marked as include + bool m_in_quote; + bool m_in_pattern; io_state m_ios; - bool m_use_exceptions; + parser_scope_stack m_parser_scope_stack; + unsigned m_next_inst_idx; bool m_show_errors; + // profiling + bool m_profile; + + // If the following flag is true we do not raise error messages + // noncomputable definitions not tagged as noncomputable. + bool m_ignore_noncomputable; + + // error recovery + bool m_error_recovery = true; + +public: + parser_info(environment const & env, io_state const & ios) : + m_env(env), m_ios(ios) {} + bool is_local_decl_user_name(expr const & l) const { return is_local(l) && m_local_decls.contains(mlocal_pp_name(l)); } + bool is_local_decl(expr const & l); + bool is_local_level_variable(name const & n) const { return m_level_variables.contains(n); } + bool is_local_variable(expr const & e) const { return m_variables.contains(mlocal_name(e)); } + bool is_local_variable_user_name(name const & n) const { + if (expr const * d = m_local_decls.find(n)) + return is_local(*d) && m_variables.contains(mlocal_name(*d)); + else + return false; + } + void clear_expr_locals(); + bool has_locals() const { return !m_local_decls.empty() || !m_local_level_decls.empty(); } + void add_local_level(name const & n, level const & l, bool is_variable = false); + void add_local_expr(name const & n, expr const & p, bool is_variable = false); + environment add_local_ref(environment const & env, name const & n, expr const & ref); + void add_variable(name const & n, expr const & p); + void add_parameter(name const & n, expr const & p); + void add_local(expr const & p) { return add_local_expr(mlocal_pp_name(p), p); } + bool has_params() const { return m_has_params; } + /** \brief Update binder information for the section parameter n, return true if success, and false if n is not a section parameter. */ + bool update_local_binder_info(name const & n, binder_info const & bi); + void include_variable(name const & n) { m_include_vars.insert(n); } + void omit_variable(name const & n) { m_include_vars.erase(n); } + bool is_include_variable(name const & n) const { return m_include_vars.contains(n); } + void get_include_variables(buffer & vars) const; + /** \brief Position of the local level declaration named \c n in the sequence of local level decls. */ + unsigned get_local_level_index(name const & n) const { return m_local_level_decls.find_idx(n); } + bool is_local_level(name const & n) const { return m_local_level_decls.contains(n); } + /** \brief Position of the local declaration named \c n in the sequence of local decls. */ + unsigned get_local_index(name const & n) const; + unsigned get_local_index(expr const & e) const { return get_local_index(mlocal_pp_name(e)); } + /** \brief Return the local parameter named \c n */ + expr const * get_local(name const & n) const { return m_local_decls.find(n); } + /** \brief Return local declarations as a list of local constants. */ + list locals_to_context() const; + /** \brief Return all local declarations and aliases */ + list> const & get_local_entries() const { return m_local_decls.get_entries(); } + virtual pos_info pos() const = 0; + virtual void maybe_throw_error(parser_error && err) = 0; + + environment const & env() const { return m_env; } + void set_env(environment const & env) { m_env = env; } + io_state const & ios() const { return m_ios; } + + struct local_scope { + parser_info & m_p; environment m_env; + local_scope(parser_info & p, bool save_options = false); + local_scope(parser_info & p, environment const & env); + local_scope(parser_info & p, optional const & env); + ~local_scope(); + }; + + bool has_local_scopes() const { return !is_nil(m_parser_scope_stack); } + void push_local_scope(bool save_options = true); + void pop_local_scope(); +protected: + parser_scope mk_parser_scope(optional const & opts = optional()); + void restore_parser_scope(parser_scope const & s); + + virtual std::tuple parse_definition(buffer & lp_names, buffer & params, + bool is_example, bool is_instance, bool, bool) = 0; + + friend environment single_definition_cmd_core(parser_info & p, decl_cmd_kind kind, cmd_meta meta); +public: + void updt_options(); + options get_options() const { return m_ios.get_options(); } + template void set_option(name const & n, T const & v) { m_ios.set_option(n, v); } + virtual expr save_pos(expr const & e, pos_info p) = 0; + virtual expr rec_save_pos(expr const & e, pos_info p) = 0; + virtual expr rec_save_pos(expr const & e, optional p) = 0; + virtual optional get_pos_info(expr const & e) const = 0; + virtual message_builder mk_message(pos_info const &p, message_severity severity) const = 0; + virtual message_builder mk_message(message_severity severity) const = 0; + bool ignore_noncomputable() const { return m_ignore_noncomputable; } + void set_ignore_noncomputable() { m_ignore_noncomputable = true; } + virtual char const * get_file_name() const = 0; + virtual pos_info cmd_pos() const = 0; + virtual optional const & get_break_at_pos() const = 0; + virtual parser_pos_provider get_parser_pos_provider(pos_info const & some_pos) const = 0; + expr mk_sorry(pos_info const & p, bool synthetic = false); + bool has_error_recovery() const { return m_error_recovery; } +}; + +class parser : public abstract_parser, public parser_info { + name_generator m_ngen; + bool m_use_exceptions; module_loader m_import_fn; std::string m_file_name; scanner m_scanner; token_kind m_curr; - local_level_decls m_local_level_decls; - local_expr_decls m_local_decls; - bool m_has_params; // true context context contains parameters - name_set m_level_variables; - name_set m_variables; // subset of m_local_decls that is marked as variables - name_set m_include_vars; // subset of m_local_decls that is marked as include bool m_imports_parsed; bool m_scanner_inited = false; - parser_scope_stack m_parser_scope_stack; parser_scope_stack m_quote_stack; - bool m_in_quote; - bool m_in_pattern; pos_info m_last_cmd_pos; unsigned m_next_tag_idx; - unsigned m_next_inst_idx; pos_info_table m_pos_table; // By default, when the parser finds a unknown identifier, it signs an error. // When the following flag is true, it creates a constant. @@ -70,8 +168,6 @@ class parser : public abstract_parser { // auto completing bool m_complete{false}; - // error recovery - bool m_error_recovery = true; bool m_error_since_last_cmd = false; pos_info m_last_recovered_error_pos {0, 0}; optional m_backtracking_pos; @@ -79,13 +175,6 @@ class parser : public abstract_parser { // curr command token name m_cmd_token; - // profiling - bool m_profile; - - // If the following flag is true we do not raise error messages - // noncomputable definitions not tagged as noncomputable. - bool m_ignore_noncomputable; - void sync_command(); tag get_tag(expr e); @@ -182,13 +271,6 @@ class parser : public abstract_parser { friend environment namespace_cmd(parser & p); friend environment end_scoped_cmd(parser & p); - parser_scope mk_parser_scope(optional const & opts = optional()); - void restore_parser_scope(parser_scope const & s); - - bool has_local_scopes() const { return !is_nil(m_parser_scope_stack); } - void push_local_scope(bool save_options = true); - void pop_local_scope(); - std::shared_ptr mk_snapshot(); optional resolve_local(name const & id, pos_info const & p, list const & extra_locals, @@ -217,7 +299,7 @@ class parser : public abstract_parser { name next_name() { return m_ngen.next(); } void set_break_at_pos(pos_info const & pos) { m_break_at_pos = some(pos); } - optional const & get_break_at_pos() const { return m_break_at_pos; } + optional const & get_break_at_pos() const override { return m_break_at_pos; } template T without_break_at_pos(std::function const & f) { flet> l(m_break_at_pos, {}); @@ -239,9 +321,6 @@ class parser : public abstract_parser { position. */ void check_break_before(break_at_pos_exception::token_context ctxt = break_at_pos_exception::token_context::none); - bool ignore_noncomputable() const { return m_ignore_noncomputable; } - void set_ignore_noncomputable() { m_ignore_noncomputable = true; } - bool in_pattern() const { return m_in_pattern; } name mk_anonymous_inst_name(); @@ -250,34 +329,26 @@ class parser : public abstract_parser { cmd_table const & cmds() const { return get_cmd_table(env()); } - environment const & env() const { return m_env; } - void set_env(environment const & env) { m_env = env; } - io_state const & ios() const { return m_ios; } - - message_builder mk_message(pos_info const & p, message_severity severity) const; + message_builder mk_message(pos_info const & p, message_severity severity) const override; message_builder mk_message(pos_info const & start_pos, pos_info const & end_pos, message_severity severity) const; - message_builder mk_message(message_severity severity) const; + message_builder mk_message(message_severity severity) const override; local_level_decls const & get_local_level_decls() const { return m_local_level_decls; } local_expr_decls const & get_local_expr_decls() const { return m_local_decls; } - void updt_options(); - options get_options() const { return m_ios.get_options(); } - template void set_option(name const & n, T const & v) { m_ios.set_option(n, v); } - /** \brief Return the current position information */ virtual pos_info pos() const override final { return pos_info(m_scanner.get_line(), m_scanner.get_pos()); } virtual expr save_pos(expr const & e, pos_info p) override final; - expr rec_save_pos(expr const & e, pos_info p); - expr rec_save_pos(expr const & e, optional p) { return p ? rec_save_pos(e, *p) : e; } + expr rec_save_pos(expr const & e, pos_info p) override final; + expr rec_save_pos(expr const & e, optional p) override final { return p ? rec_save_pos(e, *p) : e; } expr update_pos(expr e, pos_info p); void erase_pos(expr const & e); pos_info pos_of(expr const & e, pos_info default_pos) const; pos_info pos_of(expr const & e) const { return pos_of(e, pos()); } - pos_info cmd_pos() const { return m_last_cmd_pos; } + pos_info cmd_pos() const override { return m_last_cmd_pos; } name const & get_cmd_token() const { return m_cmd_token; } - parser_pos_provider get_parser_pos_provider(pos_info const & some_pos) const { + parser_pos_provider get_parser_pos_provider(pos_info const & some_pos) const override { return parser_pos_provider(m_pos_table, m_file_name, some_pos, m_next_tag_idx); } @@ -451,14 +522,6 @@ class parser : public abstract_parser { void parse_command(cmd_meta const & meta); void parse_imports(unsigned & fingerprint, std::vector &); - struct local_scope { - parser & m_p; environment m_env; - local_scope(parser & p, bool save_options = false); - local_scope(parser & p, environment const & env); - local_scope(parser & p, optional const & env); - ~local_scope(); - }; - struct quote_scope { parser & m_p; id_behavior m_id_behavior; @@ -471,50 +534,11 @@ class parser : public abstract_parser { bool in_quote() const { return m_in_quote; } - void clear_expr_locals(); - bool has_locals() const { return !m_local_decls.empty() || !m_local_level_decls.empty(); } - void add_local_level(name const & n, level const & l, bool is_variable = false); - void add_local_expr(name const & n, expr const & p, bool is_variable = false); - environment add_local_ref(environment const & env, name const & n, expr const & ref); - void add_variable(name const & n, expr const & p); - void add_parameter(name const & n, expr const & p); - void add_local(expr const & p) { return add_local_expr(mlocal_pp_name(p), p); } - bool has_params() const { return m_has_params; } - bool is_local_decl_user_name(expr const & l) const { return is_local(l) && m_local_decls.contains(mlocal_pp_name(l)); } - bool is_local_decl(expr const & l); - bool is_local_level_variable(name const & n) const { return m_level_variables.contains(n); } - bool is_local_variable(expr const & e) const { return m_variables.contains(mlocal_name(e)); } - bool is_local_variable_user_name(name const & n) const { - if (expr const * d = m_local_decls.find(n)) - return is_local(*d) && m_variables.contains(mlocal_name(*d)); - else - return false; - } - /** \brief Update binder information for the section parameter n, return true if success, and false if n is not a section parameter. */ - bool update_local_binder_info(name const & n, binder_info const & bi); - void include_variable(name const & n) { m_include_vars.insert(n); } - void omit_variable(name const & n) { m_include_vars.erase(n); } - bool is_include_variable(name const & n) const { return m_include_vars.contains(n); } - void get_include_variables(buffer & vars) const; - /** \brief Position of the local level declaration named \c n in the sequence of local level decls. */ - unsigned get_local_level_index(name const & n) const { return m_local_level_decls.find_idx(n); } - bool is_local_level(name const & n) const { return m_local_level_decls.contains(n); } - /** \brief Position of the local declaration named \c n in the sequence of local decls. */ - unsigned get_local_index(name const & n) const; - unsigned get_local_index(expr const & e) const { return get_local_index(mlocal_pp_name(e)); } - /** \brief Return the local parameter named \c n */ - expr const * get_local(name const & n) const { return m_local_decls.find(n); } - /** \brief Return local declarations as a list of local constants. */ - list locals_to_context() const; - /** \brief Return all local declarations and aliases */ - list> const & get_local_entries() const { return m_local_decls.get_entries(); } - - void maybe_throw_error(parser_error && err); + void maybe_throw_error(parser_error && err) override; level parser_error_or_level(parser_error && err); expr parser_error_or_expr(parser_error && err); void throw_invalid_open_binder(pos_info const & pos); - bool has_error_recovery() const { return m_error_recovery; } flet error_recovery_scope(bool enable_recovery) { return flet(m_error_recovery, enable_recovery); } @@ -546,8 +570,6 @@ class parser : public abstract_parser { /* Elaborate \c e as a type using the given metavariable context, and using m_local_decls as the local context */ pair elaborate_type(name const & decl_name, metavar_context & mctx, expr const & e); - expr mk_sorry(pos_info const & p, bool synthetic = false); - /** return true iff profiling is enabled */ bool profiling() const { return m_profile; } @@ -566,10 +588,64 @@ class parser : public abstract_parser { virtual optional get_pos_info(expr const & e) const override; virtual pos_info get_some_pos() const override; virtual char const * get_file_name() const override; + +protected: + virtual std::tuple parse_definition(buffer & lp_names, buffer & params, + bool is_example, bool is_instance, bool, bool) override; }; bool parse_commands(environment & env, io_state & ios, char const * fname); +class dummy_def_parser : public parser_info { +public: + bool m_ignore_noncomputable; + pos_info m_pos; + std::string m_file_name; + name m_name; + buffer m_lp_params; + buffer m_params; + expr m_type; + buffer, expr>> m_val; + optional m_wf_tac; + optional m_break_at_pos; +public: + dummy_def_parser(environment const & env, options const & opts) : + parser_info(env, io_state(io_state(), opts)) + { m_error_recovery = false; } + char const * get_file_name() const override { return m_file_name.c_str(); } + bool ignore_noncomputable() const { return m_ignore_noncomputable; } + options get_options() const { return m_ios.get_options(); } + message_builder mk_message(pos_info const &p, message_severity severity) const override { + std::shared_ptr tc = std::make_shared(m_env, get_options()); + return message_builder(tc, m_env, m_ios, get_file_name(), p, severity); } + message_builder mk_message(message_severity severity) const override { + return mk_message(pos(), severity); } + pos_info pos() const override { return m_pos; } + pos_info cmd_pos() const override { return m_pos; } + environment const & env() const { return m_env; } + optional const & get_break_at_pos() const override { return m_break_at_pos; } + parser_pos_provider get_parser_pos_provider(pos_info const & some_pos) const override { + return parser_pos_provider(rb_map(), m_file_name, some_pos, 0); + } + bool is_local_level(name const & n) const { return m_local_level_decls.contains(n); } + bool is_local_level_variable(name const & n) const { return m_level_variables.contains(n); } + void maybe_throw_error(parser_error && err) override; + buffer const & get_univ_params() const { return m_lp_params; } + name get_name() const { return m_name; } + buffer const & get_binders() { return m_params; } + expr const & get_type() { return m_type; } + const buffer, expr>> & get_val() const { return m_val; } + virtual expr save_pos(expr const & e, pos_info) override { return e; } + virtual expr rec_save_pos(expr const & e, pos_info) override { return e; } + virtual expr rec_save_pos(expr const & e, optional) override { return e; } + virtual optional get_pos_info(expr const &) const override { return optional(m_pos); } + optional get_well_founded_tac() const { return m_wf_tac; } + +protected: + virtual std::tuple parse_definition(buffer & lp_names, buffer & params, + bool is_example, bool is_instance, bool, bool) override; +}; + void initialize_parser(); void finalize_parser(); } diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index c3a15dc5f9..d5a295efd0 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -140,8 +140,8 @@ levels remove_local_vars(parser const & p, levels const & ls) { } // TODO(Leo): delete these headers -void collect_annonymous_inst_implicit(parser const & p, collected_locals & locals); -void sort_locals(buffer const & locals, parser const & p, buffer & ps); +void collect_annonymous_inst_implicit(parser_info const & p, collected_locals & locals); +void sort_locals(buffer const & locals, parser_info const & p, buffer & ps); list locals_to_context(expr const & e, parser const & p) { collected_locals ls; @@ -213,22 +213,22 @@ expr update_local_ref(expr const & e, name_set const & lvls_to_remove, name_set } } -expr Fun(buffer const & locals, expr const & e, parser & p) { +expr Fun(buffer const & locals, expr const & e, parser_info & p) { bool use_cache = false; return p.rec_save_pos(Fun(locals, e, use_cache), p.get_pos_info(e)); } -expr Fun(expr const & local, expr const & e, parser & p) { +expr Fun(expr const & local, expr const & e, parser_info & p) { bool use_cache = false; return p.rec_save_pos(Fun(local, e, use_cache), p.get_pos_info(e)); } -expr Pi(buffer const & locals, expr const & e, parser & p) { +expr Pi(buffer const & locals, expr const & e, parser_info & p) { bool use_cache = false; return p.rec_save_pos(Pi(locals, e, use_cache), p.get_pos_info(e)); } -expr Pi(expr const & local, expr const & e, parser & p) { +expr Pi(expr const & local, expr const & e, parser_info & p) { bool use_cache = false; return p.rec_save_pos(Pi(local, e, use_cache), p.get_pos_info(e)); } diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index ac83f18818..a8b06ea36f 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -16,6 +16,7 @@ Author: Leonardo de Moura namespace lean { class parser; +class parser_info; /** \brief Consume tokens until 'end' token is consumed or a command/eof is found */ void consume_until_end_or_command(parser & p); @@ -37,10 +38,10 @@ bool is_eqn_prefix(parser & p, bool bar_only = false); levels collect_local_nonvar_levels(parser & p, level_param_names const & ls); /** \brief Collect local constants occurring in \c type and \c value, sort them, and store in ctx_ps */ void collect_locals(expr const & type, expr const & value, parser const & p, buffer & ctx_ps); -void collect_annonymous_inst_implicit(parser const & p, collected_locals & ls); +void collect_annonymous_inst_implicit(parser_info const & p, collected_locals & ls); name_set collect_univ_params_ignoring_tactics(expr const & e, name_set const & ls = name_set()); /** \brief Copy the local names to \c ps, then sort \c ps (using the order in which they were declared). */ -void sort_locals(buffer const & locals, parser const & p, buffer & ps); +void sort_locals(buffer const & locals, parser_info const & p, buffer & ps); /** \brief Remove from \c ps local constants that are tagged as variables. */ void remove_local_vars(parser const & p, buffer & ps); /** \brief Remove from \c ls any universe level that is tagged as variable in \c p */ @@ -71,11 +72,11 @@ bool is_local_ref(expr const & e); expr update_local_ref(expr const & e, name_set const & lvls_to_remove, name_set const & locals_to_remove); /** \brief Fun(locals, e), but also propagate \c e position to result */ -expr Fun(buffer const & locals, expr const & e, parser & p); -expr Fun(expr const & local, expr const & e, parser & p); +expr Fun(buffer const & locals, expr const & e, parser_info & p); +expr Fun(expr const & local, expr const & e, parser_info & p); /** \brief Pi(locals, e), but also propagate \c e position to result */ -expr Pi(buffer const & locals, expr const & e, parser & p); -expr Pi(expr const & local, expr const & e, parser & p); +expr Pi(buffer const & locals, expr const & e, parser_info & p); +expr Pi(expr const & local, expr const & e, parser_info & p); /** \brief Similar to Pi(locals, e, p), but the types are marked as 'as-is' (i.e., they are not processed by the elaborator. */ expr Pi_as_is(buffer const & locals, expr const & e, parser & p); expr Pi_as_is(expr const & local, expr const & e); diff --git a/src/library/io_state.cpp b/src/library/io_state.cpp index 08ebf4261e..be87e8e817 100644 --- a/src/library/io_state.cpp +++ b/src/library/io_state.cpp @@ -24,6 +24,8 @@ io_state::io_state(formatter_factory const & fmtf): m_diagnostic_channel(std::make_shared()) { } +io_state::io_state(options const & opts): io_state(opts, mk_print_formatter_factory()) {} + io_state::io_state(options const & opts, formatter_factory const & fmtf): m_options(opts), m_formatter_factory(fmtf), diff --git a/src/library/io_state.h b/src/library/io_state.h index 211cb13215..468c3ea8d8 100644 --- a/src/library/io_state.h +++ b/src/library/io_state.h @@ -27,6 +27,7 @@ class io_state { std::shared_ptr m_diagnostic_channel; public: io_state(); + io_state(options const & opts); io_state(formatter_factory const & fmtf); io_state(options const & opts, formatter_factory const & fmtf); io_state(io_state const & ios, std::shared_ptr const & r, std::shared_ptr const & d); diff --git a/tests/lean/add_defn_eqns.lean b/tests/lean/add_defn_eqns.lean new file mode 100644 index 0000000000..a15d69d1f5 --- /dev/null +++ b/tests/lean/add_defn_eqns.lean @@ -0,0 +1,126 @@ +open tactic expr + +run_cmd do + n ← mk_local_def `n `(bool → bool), + b ← mk_local_def `b `(bool), + a ← mk_local_def `a `(bool), + add_defn_equations [] [a,b] n + [ ([``(tt)], `(ff)), + ([``(ff)], `(tt)) ] + ff + +#print n._main +#print prefix n + +run_cmd do + m ← mk_local_def `m `(bool → bool), + add_defn_equations [] [] m + [ ([``(tt)], `(ff)), + ([``(ff)], `(tt)) ] + tt + +#print m +#print prefix m + +#eval m tt + +run_cmd do + m ← mk_local_def `mm `(bool → bool), + b ← mk_local_def `b `(bool), + a ← mk_local_def `a `(bool), + add_defn_equations [] [a,b] m + [ ([``(tt)], m `(ff)), + ([``(ff)], m `(tt)) ] + ff + +#print mm + +run_cmd do + mm ← mk_local_def `mm `(bool → bool), + b ← mk_local_def `b `(bool), + a ← mk_local_def `a `(bool), + add_defn_equations [] [a,b] mm + [ ] + ff + +#print mm._main + +run_cmd do + plus ← mk_local_def `plus' `(nat → nat), + x ← mk_local_def `x `(nat), + a ← mk_local_def `a `(nat), + b ← mk_local_def `b `(nat), + add_defn_equations [] [a,b] plus + [ ([ ``(nat.zero) ], b), + ([ ``(nat.succ %%x) ], plus x) ] ff + +#print plus' + +#print prefix plus' + +open level + +run_cmd do + let u := param `u, + α ← mk_local' `α binder_info.implicit (sort (succ u)), + let list_t := @const tt ``list [u] α, + append ← mk_local_def `foo_append $ imp list_t list_t, + xs ← mk_local_def `xs list_t, + y ← mk_local_def `y α, + ys ← mk_local_def `ys list_t, + let list_cons := @const tt ``list.cons [u], + add_defn_equations [`u] [α,xs] append + [ ([ ``(@list.nil %%α) ], xs), + ([ ``(%%y :: %%ys) ], list_cons α y $ append ys) ] ff + +#print foo_append._main + +#print prefix foo_append +universes u + +inductive vec (α : Type u) : ℕ → Type u +| nil {} : vec 0 +| cons {n : ℕ} : α → vec n → vec n.succ + +run_cmd do + let u := param `u, + let v := param `v, + α ← mk_local' `α binder_info.implicit (sort (succ u)), + β ← mk_local' `β binder_info.implicit (sort (succ v)), + f ← mk_local_def `f $ α.imp β, + n ← mk_local' `n binder_info.default `(nat), + let vec_t := @const tt ``vec [u] α n, + let vec_t' := @const tt ``vec [v] β n, + map ← mk_local_def `vec.map $ pis [n] $ imp vec_t vec_t', + y ← mk_local_def `y α, + ys ← mk_local_def `ys vec_t, + let vec_nil := @const tt ``vec.nil [v], + let vec_cons := @const tt ``vec.cons [v], + add_defn_equations [`u,`v] [α,β,f] map + [ ([ ``(._), ``(@vec.nil %%α) ], vec_nil β), + ([ ``(.(nat.succ %%n)), ``(@vec.cons %%α %%n %%y %%ys) ], vec_cons β n (f y) $ map n ys ) ] ff + +#print vec.map._main +#print prefix vec.map + +run_cmd do + let u := param `u, + let v := param `v, + α ← mk_local' `α binder_info.implicit (sort (succ u)), + β ← mk_local' `β binder_info.implicit (sort (succ v)), + f ← mk_local_def `f $ α.imp β, + n ← mk_local' `n binder_info.implicit `(nat), + let vec_t := @const tt ``vec [u] α n, + let vec_t' := @const tt ``vec [v] β n, + map ← mk_local_def `vec.map' $ pis [n] $ imp vec_t vec_t', + y ← mk_local_def `y α, + ys ← mk_local_def `ys vec_t, + let vec_nil := @const tt ``vec.nil [v], + let vec_cons := @const tt ``vec.cons [v], + add_defn_equations [`u,`v] [α,β,f] map + [ ([ ``(._), ``(@vec.nil %%α) ], vec_nil β), + ([ ``(.(nat.succ %%n)), ``(@vec.cons %%α %%n %%y %%ys) ], vec_cons β n (f y) $ map n ys ) ] ff + +#check vec.map'._main +#print vec.map'._main +#print prefix vec.map' diff --git a/tests/lean/add_defn_eqns.lean.expected.out b/tests/lean/add_defn_eqns.lean.expected.out new file mode 100644 index 0000000000..5f08f2e819 --- /dev/null +++ b/tests/lean/add_defn_eqns.lean.expected.out @@ -0,0 +1,140 @@ +def n._main : bool → bool := +λ (a : bool), bool.cases_on a (id_rhs bool tt) (id_rhs bool ff) +n : bool → bool → bool → bool +n._main : bool → bool +n._main.equations._eqn_1 : n._main ff = tt +n._main.equations._eqn_2 : n._main tt = ff +n._sunfold : bool → bool → bool → bool +n.equations._eqn_1 : ∀ (a b : bool), n a b ff = tt +n.equations._eqn_2 : ∀ (a b : bool), n a b tt = ff +meta def m : bool → bool := +λ (a : bool), bool.cases_on a (id_rhs bool tt) (id_rhs bool ff) +m : bool → bool +ff +add_defn_eqns.lean:27:0: error: failed to prove recursive application is decreasing, well founded relation + @has_well_founded.r bool (@has_well_founded_of_has_sizeof bool bool.has_sizeof) +Possible solutions: + - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs. + - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions. +The nested exception contains the failure state for the decreasing tactic. +nested exception message: +invalid apply tactic, failed to unify + 1 < 1 +with + ?m_1 < ?m_1 + ?m_2 +state: +a b : bool, +mm : bool → bool +⊢ 1 < 1 +state: +⊢ true +add_defn_eqns.lean:38:0: error: unknown identifier mm +add_defn_eqns.lean:38:0: error: non-exhaustive match, the following cases are missing: +mm ff +mm tt +state: +⊢ true +add_defn_eqns.lean:0:0: warning: declaration 'mm' uses sorry +add_defn_eqns.lean:48:0: error: unknown identifier mm._main +def plus' : ℕ → ℕ → ℕ → ℕ := +λ (a b : ℕ), plus'._main b +plus' : ℕ → ℕ → ℕ → ℕ +plus'._main : ℕ → ℕ → ℕ +plus'._main._meta_aux : ℕ → ℕ → ℕ +plus'._main.equations._eqn_1 : ∀ (b : ℕ), plus'._main b 0 = b +plus'._main.equations._eqn_2 : ∀ (b x : ℕ), plus'._main b (nat.succ x) = plus'._main b x +plus'._sunfold : ℕ → ℕ → ℕ → ℕ +plus'.equations._eqn_1 : ∀ (a b : ℕ), plus' a b 0 = b +plus'.equations._eqn_2 : ∀ (a b x : ℕ), plus' a b (nat.succ x) = plus' a b x +def foo_append._main : Π {α : Type u}, list α → list α → list α := +λ {α : Type u} (xs«_» : list α), + list.brec_on «_» + (λ («_» : list α) (_F : list.below α «_»), + (λ («_» : list α) (_F : list.below α «_»), + list.cases_on «_» (λ (_F : list.below α list.nil), id_rhs (list α) xs) + (λ (hd : α) (tl : list α) (_F : list.below α (hd :: tl)), id_rhs (list α) (hd :: (_F.fst).fst)) + _F) + «_» + _F) +foo_append : Π {α : Type u}, list α → list α → list α +foo_append._main : Π {α : Type u}, list α → list α → list α +foo_append._main._meta_aux : Π {α : Type u}, list α → list α → list α +foo_append._main.equations._eqn_1 : ∀ {α : Type u} (xs : list α), foo_append._main xs list.nil = xs +foo_append._main.equations._eqn_2 : ∀ {α : Type u} (xs : list α) (y : α) (ys : list α), foo_append._main xs (y :: ys) = y :: foo_append._main xs ys +foo_append._sunfold : Π {α : Type u}, list α → list α → list α +foo_append.equations._eqn_1 : ∀ {α : Type u} (xs : list α), foo_append xs list.nil = xs +foo_append.equations._eqn_2 : ∀ {α : Type u} (xs : list α) (y : α) (ys : list α), foo_append xs (y :: ys) = y :: foo_append xs ys +def vec.map._main : Π {α : Type u} {β : Type v}, (α → β) → Π (n : ℕ), vec α n → vec β n := +λ {α : Type u} {β : Type v} (f : α → β) (n : ℕ) («_» : vec α n), + nat.brec_on n + (λ (n : ℕ) (_F : nat.below (λ (n : ℕ), vec α n → vec β n) n) («_» : vec α n), + (λ (n : ℕ) («_» : vec α n) (_F : nat.below (λ (n : ℕ), vec α n → vec β n) n), + vec.cases_on «_» + (λ (a : n = 0), + eq.rec + (λ («_» : vec α 0) (_F : nat.below (λ (n : ℕ), vec α n → vec β n) 0) + (H_2 : «_» == vec.nil), eq.rec (id_rhs (vec β 0) vec.nil) _) + _ + «_» + _F) + (λ {n_1 : ℕ} (a : α) (a_1 : vec α n_1) (H_1 : n = nat.succ n_1), + eq.rec + (λ («_» : vec α (nat.succ n_1)) + (_F : nat.below (λ (n : ℕ), vec α n → vec β n) (nat.succ n_1)) (H_2 : «_» == vec.cons a a_1), + eq.rec (id_rhs (vec β (nat.succ n_1)) (vec.cons (f a) ((_F.fst).fst a_1))) _) + _ + «_» + _F) + _ + _) + n + «_» + _F) + «_» +vec.map : Π {α : Type u} {β : Type v}, (α → β) → Π (n : ℕ), vec α n → vec β n +vec.map._main : Π {α : Type u} {β : Type v}, (α → β) → Π (n : ℕ), vec α n → vec β n +vec.map._main._meta_aux : Π {α : Type u} {β : Type v}, (α → β) → Π (n : ℕ), vec α n → vec β n +vec.map._main.equations._eqn_1 : ∀ {α : Type u} {β : Type v} (f : α → β), vec.map._main f 0 vec.nil = vec.nil +vec.map._main.equations._eqn_2 : ∀ {α : Type u} {β : Type v} (f : α → β) (n : ℕ) (y : α) (ys : vec α n), + vec.map._main f (nat.succ n) (vec.cons y ys) = vec.cons (f y) (vec.map._main f n ys) +vec.map._sunfold : Π {α : Type u} {β : Type v}, (α → β) → Π (n : ℕ), vec α n → vec β n +vec.map.equations._eqn_1 : ∀ {α : Type u} {β : Type v} (f : α → β), vec.map f 0 vec.nil = vec.nil +vec.map.equations._eqn_2 : ∀ {α : Type u} {β : Type v} (f : α → β) (n : ℕ) (y : α) (ys : vec α n), + vec.map f (nat.succ n) (vec.cons y ys) = vec.cons (f y) (vec.map f n ys) +vec.map'._main : (?M_1 → ?M_2) → Π {n : ℕ}, vec ?M_1 n → vec ?M_2 n +def vec.map'._main : Π {α : Type u} {β : Type v}, (α → β) → Π {n : ℕ}, vec α n → vec β n := +λ {α : Type u} {β : Type v} (f : α → β) {n : ℕ} («_» : vec α n), + nat.brec_on n + (λ {n : ℕ} (_F : nat.below (λ {n : ℕ}, vec α n → vec β n) n) («_» : vec α n), + (λ {n : ℕ} («_» : vec α n) (_F : nat.below (λ {n : ℕ}, vec α n → vec β n) n), + vec.cases_on «_» + (λ (a : n = 0), + eq.rec + (λ («_» : vec α 0) (_F : nat.below (λ {n : ℕ}, vec α n → vec β n) 0) + (H_2 : «_» == vec.nil), eq.rec (id_rhs (vec β 0) vec.nil) _) + _ + «_» + _F) + (λ {n_1 : ℕ} (a : α) (a_1 : vec α n_1) (H_1 : n = nat.succ n_1), + eq.rec + (λ («_» : vec α (nat.succ n_1)) + (_F : nat.below (λ {n : ℕ}, vec α n → vec β n) (nat.succ n_1)) (H_2 : «_» == vec.cons a a_1), + eq.rec (id_rhs (vec β (nat.succ n_1)) (vec.cons (f a) ((_F.fst).fst a_1))) _) + _ + «_» + _F) + _ + _) + «_» + _F) + «_» +vec.map' : Π {α : Type u} {β : Type v}, (α → β) → Π {n : ℕ}, vec α n → vec β n +vec.map'._main : Π {α : Type u} {β : Type v}, (α → β) → Π {n : ℕ}, vec α n → vec β n +vec.map'._main._meta_aux : Π {α : Type u} {β : Type v}, (α → β) → Π {n : ℕ}, vec α n → vec β n +vec.map'._main.equations._eqn_1 : ∀ {α : Type u} {β : Type v} (f : α → β), vec.map'._main f vec.nil = vec.nil +vec.map'._main.equations._eqn_2 : ∀ {α : Type u} {β : Type v} (f : α → β) (n : ℕ) (y : α) (ys : vec α n), + vec.map'._main f (vec.cons y ys) = vec.cons (f y) (vec.map'._main f ys) +vec.map'._sunfold : Π {α : Type u} {β : Type v}, (α → β) → Π {n : ℕ}, vec α n → vec β n +vec.map'.equations._eqn_1 : ∀ {α : Type u} {β : Type v} (f : α → β), vec.map' f vec.nil = vec.nil +vec.map'.equations._eqn_2 : ∀ {α : Type u} {β : Type v} (f : α → β) (n : ℕ) (y : α) (ys : vec α n), + vec.map' f (vec.cons y ys) = vec.cons (f y) (vec.map' f ys) From 7acbd729f01a8b623f5306147d93d524a12472c1 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Mon, 6 May 2019 23:51:30 -0400 Subject: [PATCH 16/36] chore(build): fix ccache+clang++ on travis --- .travis.yml | 12 +++++++++++- script/ccache-clang++ | 2 ++ script/ccache-g++ | 2 ++ src/CMakeLists.txt | 1 + 4 files changed, 16 insertions(+), 1 deletion(-) create mode 100644 script/ccache-clang++ create mode 100644 script/ccache-g++ diff --git a/.travis.yml b/.travis.yml index 8d39b6ed35..2e63d402b5 100644 --- a/.travis.yml +++ b/.travis.yml @@ -7,6 +7,7 @@ dist: trusty branches: only: - master + - travis-ccache group: deprecated-2017Q3 addons: apt: @@ -119,12 +120,21 @@ before_install: brew update && (brew install gcc || brew link --overwrite gcc) && brew install gmp && + brew install ccache && # workaround for https://github.com/travis-ci/travis-ci/issues/6307 command curl -sSL https://rvm.io/mpapis.asc | gpg --import - command curl -sSL https://rvm.io/pkuczynski.asc | gpg --import - rvm get head || true fi +install: + - export CXX_FAMILY=`echo $CMAKE_CXX_COMPILER | sed -n "s/\([^\+]*++\).*/\1/p"` + # CXX_FAMILY is either `clang++` or `g++` + - mkdir -p ~/bin/ + - chmod +x script/ccache-$CXX_FAMILY + - cp script/ccache-$CXX_FAMILY ~/bin/ + - export PATH="~/bin/:$PATH" + script: - mkdir -p build - cd build @@ -142,7 +152,7 @@ script: . ../script/setup_nightly.sh fi - cmake -DCMAKE_BUILD_TYPE=$CMAKE_BUILD_TYPE - -DCMAKE_CXX_COMPILER=$CMAKE_CXX_COMPILER + -DCMAKE_CXX_COMPILER=ccache-$CXX_FAMILY -DTESTCOV=$TESTCOV -DTCMALLOC=$TCMALLOC -DMULTI_THREAD=$MULTI_THREAD diff --git a/script/ccache-clang++ b/script/ccache-clang++ new file mode 100644 index 0000000000..73fe3c40e8 --- /dev/null +++ b/script/ccache-clang++ @@ -0,0 +1,2 @@ +#!/bin/sh +ccache $CMAKE_CXX_COMPILER -Qunused-arguments -fcolor-diagnostics "$@" \ No newline at end of file diff --git a/script/ccache-g++ b/script/ccache-g++ new file mode 100644 index 0000000000..3f955af352 --- /dev/null +++ b/script/ccache-g++ @@ -0,0 +1,2 @@ +#!/bin/sh +ccache $CMAKE_CXX_COMPILER "$@" \ No newline at end of file diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7d95190156..7bab872677 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -607,3 +607,4 @@ endif() SET(CPACK_DEBIAN_PACKAGE_DESCRIPTION "Lean Theorem Prover") SET(CPACK_DEBIAN_PACKAGE_SECTION "devel") include(CPack) +# SET_PROPERTY(GLOBAL PROPERTY RULE_LAUNCH_COMPILE ccache) From abd06a912899c878b768d62da97812409043d0a4 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Fri, 3 May 2019 12:39:37 -0400 Subject: [PATCH 17/36] play around with libffi --- src/library/vm/vm_environment.cpp | 1 + tests/lean/vm_dynload/Makefile | 7 ++++-- tests/lean/vm_dynload/client.c | 40 ++++++++++++++++++++++++------- tests/lean/vm_dynload/some_file.c | 5 ++-- 4 files changed, 41 insertions(+), 12 deletions(-) diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp index 173e2fe905..67c7eba7da 100644 --- a/src/library/vm/vm_environment.cpp +++ b/src/library/vm/vm_environment.cpp @@ -331,6 +331,7 @@ vm_obj environment_bind_foreign_symbol(vm_obj const & _env, vm_obj const & _fo, environment env = to_env(_env); name fo = to_name(_fo); name fn = to_name(_fn); + expr type = env.get(fn).get_type(); unsigned arity = to_unsigned(_arity); std::string symbol = to_string(_symbol); return to_obj(bind_foreign_symbol(env,fo,fn,arity,symbol)); diff --git a/tests/lean/vm_dynload/Makefile b/tests/lean/vm_dynload/Makefile index 2a7f60de2e..122cc98c24 100644 --- a/tests/lean/vm_dynload/Makefile +++ b/tests/lean/vm_dynload/Makefile @@ -1,12 +1,15 @@ +INCLUDES=/usr/local/lib/libffi-3.2.1/include +LIB=/usr/local/lib/libffi-3.2.1/lib + all: some_file.so client ./client %.o: %.c - gcc -c -fPIC $< -o $@ + gcc -c -fPIC $< -o $@ -I$(INCLUDES) some_file.so: some_file.o gcc some_file.o -shared -o some_file.so client: client.c - gcc client.c -o client + gcc client.c -o client -I$(INCLUDES) -lffi diff --git a/tests/lean/vm_dynload/client.c b/tests/lean/vm_dynload/client.c index 811728b5fa..9c644b26cb 100644 --- a/tests/lean/vm_dynload/client.c +++ b/tests/lean/vm_dynload/client.c @@ -1,19 +1,43 @@ +#include #include #include +typedef int (*main_fn) (int, int); + +void call(main_fn fn, int x, int y) { + ffi_cif cif; + ffi_type *args[2] = {&ffi_type_sint32, &ffi_type_sint32}; + void *values[2] = {(void *) &x, (void *) &y}; + ffi_arg rc; + if (ffi_prep_cif(&cif, FFI_DEFAULT_ABI, 2, + &ffi_type_sint32, args) == FFI_OK) + { + /* s = "Hello World!"; */ + ffi_call(&cif, (void (*)(void)) fn, &rc, values); + printf("result: %d", (int) rc); + } + + /* char *s; */ + /* ffi_arg rc; */ + + /* Initialize the argument info vectors */ + /* args[0] = &ffi_int; */ + /* values[0] = &s; */ + +} int main () { - int (*my_main) (); - void* handle = dlopen("some_file.so", RTLD_LAZY); - if (!handle) { + main_fn my_main; + void* handle = dlopen("some_file.so", RTLD_LAZY); + if (!handle) { printf("Cannot load library: %s", dlerror()); return -1; - } - my_main = dlsym(handle, "main"); - if (!my_main) { + } + my_main = dlsym(handle, "my_fun"); + if (!my_main) { printf("Cannot load 'main': %s", dlerror()); return -1; - } - my_main(); + } + call(my_main,2,3); } diff --git a/tests/lean/vm_dynload/some_file.c b/tests/lean/vm_dynload/some_file.c index b6fb0c95d5..10c5f988bd 100644 --- a/tests/lean/vm_dynload/some_file.c +++ b/tests/lean/vm_dynload/some_file.c @@ -1,6 +1,7 @@ #include -int main () { - printf("hello world\n"); +int my_fun (int x, int y) { + printf("hello world: %d\n", x + y); + return x * y; } From 609afe895c7aaa193662622b13ec221a8c955251 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Sat, 4 May 2019 13:17:27 -0400 Subject: [PATCH 18/36] include ffi.h --- src/CMakeLists.txt | 1 + src/library/vm/vm_environment.cpp | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7bab872677..abc50bc7b5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -310,6 +310,7 @@ else() set(FFI_HEADER ffi.h CACHE INTERNAL "") set(HAVE_FFI_H 1 CACHE INTERNAL "") else() + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D USE_FFI_FFI_H") find_path(FFI_INCLUDE_PATH ffi/ffi.h PATHS ${FFI_INCLUDE_DIR}) if( EXISTS "${FFI_INCLUDE_PATH}/ffi/ffi.h" ) set(FFI_HEADER ffi/ffi.h CACHE INTERNAL "") diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp index 67c7eba7da..3361820d52 100644 --- a/src/library/vm/vm_environment.cpp +++ b/src/library/vm/vm_environment.cpp @@ -5,7 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#ifdef USE_FFI_FFI_H +#include +#else #include +#endif #include "library/unfold_macros.h" #include "kernel/type_checker.h" #include "kernel/inductive/inductive.h" From 353d4ab65a78dcee26b822cd6c75591cbc7eb767 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Sat, 11 May 2019 21:59:54 -0400 Subject: [PATCH 19/36] WIP --- library/init/meta/vm.lean | 2 +- src/library/tactic/vm_monitor.cpp | 1 + src/library/vm/init_module.cpp | 3 ++ src/library/vm/vm.cpp | 85 ++++++++++++++++++++++++++++--- src/library/vm/vm.h | 18 +++++-- src/library/vm/vm_dynload.cpp | 83 ++++++++++++++++++++++++++++-- src/library/vm/vm_dynload.h | 8 ++- src/library/vm/vm_environment.cpp | 27 ++++------ 8 files changed, 194 insertions(+), 33 deletions(-) diff --git a/library/init/meta/vm.lean b/library/init/meta/vm.lean index 9f2af579cd..fb0c43df60 100644 --- a/library/init/meta/vm.lean +++ b/library/init/meta/vm.lean @@ -47,7 +47,7 @@ end vm_obj meta constant vm_decl : Type inductive vm_decl_kind -| bytecode | builtin | cfun +| bytecode | builtin | cfun | ffi_call /-- Information for local variables and arguments on the VM stack. Remark: type is only available if it is a closed term at compilation time. -/ diff --git a/src/library/tactic/vm_monitor.cpp b/src/library/tactic/vm_monitor.cpp index c41e913aef..4cb550776f 100644 --- a/src/library/tactic/vm_monitor.cpp +++ b/src/library/tactic/vm_monitor.cpp @@ -191,6 +191,7 @@ vm_obj _vm_decl_kind(vm_obj const & d) { case vm_decl_kind::Bytecode: return mk_vm_simple(0); case vm_decl_kind::Builtin: return mk_vm_simple(1); case vm_decl_kind::CFun: return mk_vm_simple(2); + case vm_decl_kind::FFICall: return mk_vm_simple(3); } lean_unreachable(); } diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp index 6b055909ab..a70f8ac8cd 100644 --- a/src/library/vm/init_module.cpp +++ b/src/library/vm/init_module.cpp @@ -24,6 +24,7 @@ Author: Leonardo de Moura #include "library/vm/vm_parser.h" #include "library/vm/vm_array.h" #include "library/vm/vm_string.h" +#include "library/vm/vm_dynload.h" namespace lean { void initialize_vm_core_module() { @@ -47,9 +48,11 @@ void initialize_vm_core_module() { initialize_vm_parser(); initialize_vm_array(); initialize_vm_string(); + initialize_vm_ffi(); } void finalize_vm_core_module() { + finalize_vm_ffi(); finalize_vm_string(); finalize_vm_array(); finalize_vm_parser(); diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 2cd92afcda..bb2f2d830f 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include +#include #include #include #include @@ -28,6 +29,7 @@ Author: Leonardo de Moura #include "library/time_task.h" #include "library/vm/vm.h" #include "library/vm/vm_name.h" +#include "library/vm/vm_nat.h" #include "library/vm/vm_option.h" #include "library/vm/vm_expr.h" #include "library/vm/vm_dynload.h" @@ -1027,6 +1029,10 @@ vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_func vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_cfunction fn): m_rc(0), m_kind(vm_decl_kind::CFun), m_name(n), m_idx(idx), m_arity(arity), m_cfn(fn) {} +vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, + vm_cfun_sig && sig, vm_cfunction fn): + m_rc(0), m_kind(vm_decl_kind::CFun), m_name(n), m_idx(idx), m_sig(sig), m_cfn(fn) {} + vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, unsigned code_sz, vm_instr const * code, list const & args_info, optional const & pos, optional const & olean): @@ -1047,6 +1053,11 @@ void vm_decl_cell::dealloc() { delete this; } +vm_cfun_sig::vm_cfun_sig(ffi_abi abi, ffi_type & rtype, buffer && args) : + m_args(args) { + ffi_prep_cif(&m_cif, abi, m_args.size(), &rtype, args.data()); +} + /** \brief VM builtin functions */ static name_map> * g_vm_builtins = nullptr; static name_map> * g_vm_cbuiltins = nullptr; @@ -1154,11 +1165,11 @@ struct vm_decls : public environment_extension { m_foreign[n] = load_foreign_obj(file_name); } - void bind_foreign_symbol(name const & fo, name const & fn, string const & sym, unsigned arity) { - std::cout << "bind_foreign_symbol\n"; - auto c_fun = m_foreign[fo]->get_cfun(sym); - c_fun(mk_vm_none()); - add_native(fn,arity,c_fun); + void bind_foreign_symbol(name const & obj, name const & decl, string const & c_fun, buffer const & args, expr const & t) { + // std::cout << "bind_foreign_symbol\n"; + // c_fun(mk_vm_none()); + auto idx = get_vm_index(decl); + m_decls.insert(idx, m_foreign[obj]->get_cfun(decl, idx, c_fun, args, t)); } unsigned reserve(name const & n, unsigned arity) { @@ -1245,9 +1256,14 @@ environment load_foreign_object(environment const & env, name const & n, string return update(env, ext); } -environment bind_foreign_symbol(environment const & env, name const & fo, name const & fn, unsigned arity, string const & symbol) { +environment add_foreign_symbol(environment const & env, name const & obj, name const & decl, string const & c_fun) { auto ext = get_extension(env); - ext.bind_foreign_symbol(fo, fn, symbol, arity); + auto d = env.get(decl); + expr t = d.get_type(); + if (!d.is_constant_assumption()) throw exception("only constants can be bindings"); + buffer args; + auto rt = to_telescope(t, args); + ext.bind_foreign_symbol(obj, decl, c_fun, args, rt); return update(env, ext); } @@ -1574,6 +1590,46 @@ void vm_state::invoke_builtin(vm_decl const & d) { m_pc++; } +template +void ffi_push(T const & x, buffer & vals, buffer & supp) { + int last = supp.size(); + for (int i = 0; i < (sizeof(T) + sizeof(int) - 1) / sizeof(int); ++i) { + supp.push_back(i); + } + T *y = reinterpret_cast(&supp[last]); + *y = x; + vals.push_back(y); +} + +void conv_from_obj(ffi_type & t, vm_obj const & obj, + buffer & vals, buffer & supp) { + if (&t == &ffi_type_uint32) { + return to_unsigned(obj); + } else { + throw exception("unsupported argument type"); + } +} + +void vm_state::invoke_ffi_call(vm_cfunction fn, vm_cfun_sig const & sig) { + flet Set(g_vm_state, this); + auto & S = m_stack; + unsigned sz = S.size(); + unsigned arity = sig.m_args.size(); + ffi_arg rc; + lean_vm_check(arity <= sz); + vm_obj r; + buffer values; + buffer support; + for (int i = 0; i < arity; ++i) { + conv_from_obj(sig.m_args, S[sz - 1 - i], values, support); + } + ffi_call(&sig.m_cif, fn, &rc, values.data()); + m_stack.resize(sz - arity); + m_stack.push_back(r); + if (m_debugging) shrink_stack_info(); + m_pc++; +} + void vm_state::invoke_fn(vm_cfunction fn, unsigned arity) { flet Set(g_vm_state, this); auto & S = m_stack; @@ -1682,6 +1738,9 @@ vm_obj vm_state::invoke_closure(vm_obj const & fn, unsigned DEBUG_CODE(nargs)) { case vm_decl_kind::CFun: invoke_cfun(d); break; + case vm_decl_kind::FFICall: + invoke_ffi_call(d); + break; } m_pc = saved_pc; vm_obj r = m_stack.back(); @@ -2827,6 +2886,18 @@ void vm_state::invoke_cfun(vm_decl const & d) { } } +void vm_state::invoke_ffi_call(vm_decl const & d) { + if (m_profiling) { + unique_lock lk(m_call_stack_mtx); + push_frame_core(0, 0, d.get_idx()); + } + invoke_ffi_call(d.get_cfn(), d.m_sig); + if (m_profiling) { + unique_lock lk(m_call_stack_mtx); + m_call_stack.pop_back(); + } +} + void vm_state::invoke(vm_decl const & d) { switch (d.kind()) { case vm_decl_kind::Bytecode: diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index c9a78304b6..40418a8607 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include #include #include +#include #include "util/debug.h" #include "util/compiler_hints.h" #include "util/rc.h" @@ -527,7 +528,13 @@ vm_instr mk_local_info_instr(unsigned idx, name const & n, optional const class vm_state; class vm_instr; -enum class vm_decl_kind { Bytecode, Builtin, CFun }; +struct vm_cfun_sig { + buffer m_args; + ffi_cif m_cif; + vm_cfun_sig(ffi_abi abi, ffi_type & rtype, buffer && atypes); +}; + +enum class vm_decl_kind { Bytecode, Builtin, CFun, FFICall }; /** \brief VM function/constant declaration cell */ struct vm_decl_cell { @@ -539,6 +546,7 @@ struct vm_decl_cell { list m_args_info; optional m_pos; optional m_olean; + optional m_sig; union { struct { unsigned m_code_size; @@ -549,6 +557,7 @@ struct vm_decl_cell { }; vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_function fn); vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_cfunction fn); + vm_decl_cell(name const & n, unsigned idx, vm_cfun_sig && sig, vm_cfunction fn); vm_decl_cell(name const & n, unsigned idx, unsigned arity, unsigned code_sz, vm_instr const * code, list const & args_info, optional const & pos, optional const & olean); @@ -564,6 +573,8 @@ class vm_decl { vm_decl():m_ptr(nullptr) {} vm_decl(name const & n, unsigned idx, unsigned arity, vm_function fn): vm_decl(new vm_decl_cell(n, idx, arity, fn)) {} + vm_decl(name const & n, unsigned idx, vm_cfun_sig && sig, vm_cfunction fn): + vm_decl(new vm_decl_cell(n, idx, std::move(sig), fn)) {} vm_decl(name const & n, unsigned idx, unsigned arity, vm_cfunction fn): vm_decl(new vm_decl_cell(n, idx, arity, fn)) {} vm_decl(name const & n, unsigned idx, unsigned arity, unsigned code_sz, vm_instr const * code, @@ -661,6 +672,7 @@ class vm_state { unsigned pop_frame(); void invoke_builtin(vm_decl const & d); void invoke_fn(vm_cfunction fn, unsigned arity); + void invoke_ffi_call(vm_cfunction fn, vm_cfun_sig const & sig); void invoke_cfun(vm_decl const & d); void invoke_global(vm_decl const & d); void invoke(vm_decl const & d); @@ -901,8 +913,8 @@ environment add_native(environment const & env, name const & n, vm_cfunction_8 f environment add_native(environment const & env, name const & n, unsigned arity, vm_cfunction_N fn); environment load_foreign_object(environment const & env, name const & n, std::string const & file_name); -environment bind_foreign_symbol(environment const & env, name const & fo, name const & fn, - unsigned arity, std::string const & symbol); +environment add_foreign_symbol(environment const & env, name const & obj, name const & fn, + std::string const & symbol); unsigned get_vm_index(name const & n); unsigned get_vm_index_bound(); diff --git a/src/library/vm/vm_dynload.cpp b/src/library/vm/vm_dynload.cpp index f15e986855..43e1362332 100644 --- a/src/library/vm/vm_dynload.cpp +++ b/src/library/vm/vm_dynload.cpp @@ -3,14 +3,31 @@ Author: James King */ #include +#include #include #include #include -#include "util/sstream.h" -#include "library/vm/vm_io.h" -#include "library/vm/vm_string.h" +// #include "util/sstream.h" +// #include "library/vm/vm_name.h" +// #include "library/vm/vm_io.h" +// #include "library/vm/vm_string.h" #include "library/vm/vm_dynload.h" +// #include "library/attribute_manager.h" + +#include "kernel/abstract.h" +#include "library/constants.h" +#include "library/attribute_manager.h" +#include "library/scoped_ext.h" +#include "library/tactic/elaborator_exception.h" +#include "library/string.h" +#include "library/vm/vm.h" +#include "library/vm/vm_expr.h" +#include "library/vm/vm_parser.h" +#include "library/quote.h" +#include "library/placeholder.h" +#include "frontends/lean/elaborator.h" + // void get_shared_funcptr(string const & pathname) { // void* handle = dlopen(pathname.c_str(), RTLD_LAZY); @@ -22,8 +39,16 @@ Author: James King namespace lean { using namespace std; - vm_cfunction vm_foreign_obj::get_cfun(string const & fun_name) { - return reinterpret_cast(dlsym(m_handle, fun_name.c_str())); + ffi_type * to_ffi_type (expr const & e) { + } + + vm_decl vm_foreign_obj::get_cfun(name const & n, unsigned idx, string const & fun_name, + buffer const & _args, expr const & _t) { + vm_cfunction fn = reinterpret_cast(dlsym(m_handle, fun_name.c_str())); + buffer args; + ffi_type rt; + vm_cfun_sig sig(FFI_DEFAULT_ABI, rt, std::move(args)); + return vm_decl(n, idx, std::move(sig), fn); } vm_foreign_obj::~vm_foreign_obj() { @@ -38,4 +63,52 @@ using namespace std; return make_shared(vm_foreign_obj(handle, fname)); } + static name * g_vm_ffi; + struct vm_ffi_attribute_data : public attr_data { + name m_obj; + optional m_c_fun; + vm_ffi_attribute_data() {} + // vm_ffi_attribute_data(name const & n) : m_name(n) {} + // virtual unsigned hash() const override {return m_name.hash();} + void write(serializer & s) const {s << m_obj << m_c_fun;} + void read(deserializer & d) { + d >> m_obj >> m_c_fun; + } + void parse(abstract_parser & p) override { + lean_assert(dynamic_cast(&p)); + auto & p2 = *static_cast(&p); + m_obj = p2.check_constant_next("not a constant"); + if (p2.curr_is_identifier()) { + m_c_fun = optional(p2.get_name_val()); + p2.next(); + } else { + m_c_fun = optional(); + } + } + }; + // bool operator==(vm_ffi_attribute_data const & d1, vm_ffi_attribute_data const & d2) { + // return d1.m_name == d2.m_name; + // } + + template class typed_attribute; + typedef typed_attribute vm_ffi_attribute; + + static vm_ffi_attribute const & get_vm_ffi_attribute() { + return static_cast(get_system_attribute(*g_vm_ffi)); + } + + + void initialize_vm_ffi() { + register_system_attribute(basic_attribute( + "ffi", "Registers a binding to a foreign function.", + [](environment const & env, io_state const &, name const & d, unsigned, bool) -> environment { + auto data = get_vm_ffi_attribute().get(env, d); + name sym = data->m_c_fun? *data->m_c_fun : data->m_obj; + return add_foreign_symbol(env, d, data->m_obj, sym.to_string()); + })); + } + + void finalize_vm_ffi() { + } + } diff --git a/src/library/vm/vm_dynload.h b/src/library/vm/vm_dynload.h index a3559af625..a81f43ec01 100644 --- a/src/library/vm/vm_dynload.h +++ b/src/library/vm/vm_dynload.h @@ -1,5 +1,6 @@ #include #include +#include "library/vm/vm.h" #define FOREIGN_OBJ void * @@ -16,7 +17,8 @@ namespace lean { : m_handle(handle), m_filename(filename) {}; ~vm_foreign_obj(); - vm_cfunction get_cfun(string const & fun_name); + vm_decl get_cfun(name const & n, unsigned idx, string const & fun_name, + buffer const & _args, expr const & _t); /* virtual void dealloc() override { */ /* this->~vm_foreign_obj(); */ /* get_vm_allocator().deallocate(sizeof(vm_foreign_obj), this); */ @@ -31,4 +33,8 @@ namespace lean { std::shared_ptr load_foreign_obj(string const & fname); + void initialize_vm_ffi(); + + void finalize_vm_ffi(); + } diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp index 3361820d52..f8221e98da 100644 --- a/src/library/vm/vm_environment.cpp +++ b/src/library/vm/vm_environment.cpp @@ -330,23 +330,18 @@ vm_obj environment_load_foreign_object(vm_obj const & _env, vm_obj const & _n, v // environment bind_foreign_symbol(environment const & env, name const & fo, name const & fn, // unsigned arity, std::string const & symbol); -vm_obj environment_bind_foreign_symbol(vm_obj const & _env, vm_obj const & _fo, vm_obj const & _fn, - vm_obj const & _arity, vm_obj const & _symbol) { - environment env = to_env(_env); - name fo = to_name(_fo); - name fn = to_name(_fn); - expr type = env.get(fn).get_type(); - unsigned arity = to_unsigned(_arity); - std::string symbol = to_string(_symbol); - return to_obj(bind_foreign_symbol(env,fo,fn,arity,symbol)); -} +// vm_obj environment_bind_foreign_symbol(vm_obj const & _env, vm_obj const & _fo, vm_obj const & _fn, +// vm_obj const & _arity, vm_obj const & _symbol) { +// environment env = to_env(_env); +// name fo = to_name(_fo); +// name fn = to_name(_fn); +// expr type = env.get(fn).get_type(); +// unsigned arity = to_unsigned(_arity); +// std::string symbol = to_string(_symbol); +// return to_obj(bind_foreign_symbol(env,fo,fn,arity,symbol)); +// } void initialize_vm_environment() { - register_system_attribute(basic_attribute( - "ffi", "Registers a binding to a foreign function.", - [](environment const &, io_state const &, name const &, unsigned, bool) { - return; - })); DECLARE_VM_BUILTIN(name({"environment", "mk_std"}), environment_mk_std); DECLARE_VM_BUILTIN(name({"environment", "trust_lvl"}), environment_trust_lvl); DECLARE_VM_BUILTIN(name({"environment", "add"}), environment_add); @@ -380,7 +375,7 @@ void initialize_vm_environment() { DECLARE_VM_BUILTIN(name({"environment", "get_class_attribute_symbols"}), environment_get_class_attribute_symbols); DECLARE_VM_BUILTIN(name({"environment", "fingerprint"}), environment_fingerprint); DECLARE_VM_BUILTIN(name({"environment", "load_foreign_object"}), environment_load_foreign_object); - DECLARE_VM_BUILTIN(name({"environment", "bind_foreign_symbol"}), environment_bind_foreign_symbol); + // DECLARE_VM_BUILTIN(name({"environment", "bind_foreign_symbol"}), environment_bind_foreign_symbol); } void finalize_vm_environment() { From 490adbb61721ddf0d945f9e9a45b47657a96ffd4 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Sat, 11 May 2019 21:59:54 -0400 Subject: [PATCH 20/36] WIP --- .travis.yml | 2 +- library/init/meta/environment.lean | 2 - src/library/module.cpp | 2 +- src/library/vm/vm.cpp | 67 +++++++++++++++------- src/library/vm/vm.h | 21 +++++-- src/library/vm/vm_dynload.cpp | 91 ++++++++++++++++++++++++++---- src/library/vm/vm_dynload.h | 47 +++++++++++---- src/library/vm/vm_environment.cpp | 20 ------- src/util/path.cpp | 22 ++++++++ src/util/path.h | 12 ++++ tests/lean/vm_dynload/ffi.lean | 22 ++++++-- 11 files changed, 232 insertions(+), 76 deletions(-) diff --git a/.travis.yml b/.travis.yml index 2e63d402b5..015161cc09 100644 --- a/.travis.yml +++ b/.travis.yml @@ -7,7 +7,7 @@ dist: trusty branches: only: - master - - travis-ccache + - feature/vm-dynload group: deprecated-2017Q3 addons: apt: diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean index 4801e39a7c..8b7a40713e 100644 --- a/library/init/meta/environment.lean +++ b/library/init/meta/environment.lean @@ -161,8 +161,6 @@ meta constant fingerprint : environment → nat meta constant load_foreign_object (env : environment) (n : name) (file_name : string) : environment -meta constant bind_foreign_symbol(env : environment) (fo : name) (fn : name) - (arity : nat) (symbol : string) : environment open expr diff --git a/src/library/module.cpp b/src/library/module.cpp index 798e16e591..b9aa06dd9f 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -604,7 +604,7 @@ static void import_module(environment & env, std::string const & module_file_nam auto ext = get_extension(env); ext.m_imported.insert(res->m_module_name); env = update(env, ext); - } catch (throwable) { + } catch (throwable &) { import_errors.push_back({module_file_name, ref, std::current_exception()}); } } diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index bb2f2d830f..b0eb44b317 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -43,6 +43,18 @@ namespace lean { /* Reference to the VM that is currently running. */ LEAN_THREAD_VALUE(vm_state *, g_vm_state, nullptr); +std::ostream &operator << (std::ostream &out, vm_obj_kind x) { + switch (x) { + case vm_obj_kind::Simple: out << "Simple"; break; + case vm_obj_kind::Constructor: out << "Constructor"; break; + case vm_obj_kind::Closure: out << "Closure"; break; + case vm_obj_kind::NativeClosure: out << "NativeClosure"; break; + case vm_obj_kind::MPZ: out << "MPZ"; break; + case vm_obj_kind::External: out << "External"; break; + } + return out; +} + void vm_obj_cell::dec_ref(vm_obj & o, buffer & todelete) { if (LEAN_VM_IS_PTR(o.m_data)) { vm_obj_cell * c = o.steal_ptr(); @@ -1030,8 +1042,8 @@ vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_cfun m_rc(0), m_kind(vm_decl_kind::CFun), m_name(n), m_idx(idx), m_arity(arity), m_cfn(fn) {} vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, - vm_cfun_sig && sig, vm_cfunction fn): - m_rc(0), m_kind(vm_decl_kind::CFun), m_name(n), m_idx(idx), m_sig(sig), m_cfn(fn) {} + auto_ptr sig, vm_cfunction fn): + m_rc(0), m_kind(vm_decl_kind::CFun), m_name(n), m_idx(idx), m_arity(sig->arity()), m_sig(sig), m_cfn(fn) {} vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, unsigned code_sz, vm_instr const * code, list const & args_info, optional const & pos, @@ -1054,8 +1066,8 @@ void vm_decl_cell::dealloc() { } vm_cfun_sig::vm_cfun_sig(ffi_abi abi, ffi_type & rtype, buffer && args) : - m_args(args) { - ffi_prep_cif(&m_cif, abi, m_args.size(), &rtype, args.data()); + m_args(args), m_rtype(&rtype) { + ffi_prep_cif(&m_cif, abi, m_args.size(), &rtype, m_args.data()); } /** \brief VM builtin functions */ @@ -1132,7 +1144,7 @@ void declare_vm_cases_builtin(name const & n, char const * i, vm_cases_function struct vm_decls : public environment_extension { unsigned_map m_decls; unsigned_map m_cases; - std::unordered_map, name_hash> m_foreign; + std::unordered_map m_foreign; name m_monitor; @@ -1162,12 +1174,10 @@ struct vm_decls : public environment_extension { } void add_foreign_obj(name const & n, string const & file_name) { - m_foreign[n] = load_foreign_obj(file_name); + m_foreign[n] = vm_foreign_obj(file_name); } void bind_foreign_symbol(name const & obj, name const & decl, string const & c_fun, buffer const & args, expr const & t) { - // std::cout << "bind_foreign_symbol\n"; - // c_fun(mk_vm_none()); auto idx = get_vm_index(decl); m_decls.insert(idx, m_foreign[obj]->get_cfun(decl, idx, c_fun, args, t)); } @@ -1263,6 +1273,9 @@ environment add_foreign_symbol(environment const & env, name const & obj, name c if (!d.is_constant_assumption()) throw exception("only constants can be bindings"); buffer args; auto rt = to_telescope(t, args); + for (auto & e : args) { + e = mlocal_type(e); + } ext.bind_foreign_symbol(obj, decl, c_fun, args, rt); return update(env, ext); } @@ -1593,18 +1606,28 @@ void vm_state::invoke_builtin(vm_decl const & d) { template void ffi_push(T const & x, buffer & vals, buffer & supp) { int last = supp.size(); - for (int i = 0; i < (sizeof(T) + sizeof(int) - 1) / sizeof(int); ++i) { - supp.push_back(i); + for (unsigned i = 0; i < (sizeof(T) + sizeof(int) - 1) / sizeof(int); ++i) { + supp.push_back(0); } T *y = reinterpret_cast(&supp[last]); *y = x; vals.push_back(y); } -void conv_from_obj(ffi_type & t, vm_obj const & obj, +void ffi_from_obj(ffi_type const * t, vm_obj const & obj, buffer & vals, buffer & supp) { - if (&t == &ffi_type_uint32) { - return to_unsigned(obj); + if (t == &ffi_type_uint32) { + unsigned i = force_to_unsigned(obj, 0); + ffi_push(i, vals, supp); + } else { + throw exception("unsupported argument type"); + } +} + +vm_obj ffi_to_obj(ffi_type const * t, ffi_arg v) { + if (t == &ffi_type_uint32) { + unsigned *p = reinterpret_cast(&v); + return mk_vm_nat(*p); } else { throw exception("unsupported argument type"); } @@ -1617,15 +1640,15 @@ void vm_state::invoke_ffi_call(vm_cfunction fn, vm_cfun_sig const & sig) { unsigned arity = sig.m_args.size(); ffi_arg rc; lean_vm_check(arity <= sz); - vm_obj r; buffer values; buffer support; - for (int i = 0; i < arity; ++i) { - conv_from_obj(sig.m_args, S[sz - 1 - i], values, support); + for (unsigned i = 0; i < arity; ++i) { + ffi_from_obj(sig.m_args[i], S[sz - 1 - i], values, support); } - ffi_call(&sig.m_cif, fn, &rc, values.data()); m_stack.resize(sz - arity); - m_stack.push_back(r); + ffi_call(const_cast(&sig.m_cif), + reinterpret_cast(fn), &rc, values.data()); + m_stack.push_back(ffi_to_obj(sig.m_rtype, rc)); if (m_debugging) shrink_stack_info(); m_pc++; } @@ -2879,7 +2902,10 @@ void vm_state::invoke_cfun(vm_decl const & d) { unique_lock lk(m_call_stack_mtx); push_frame_core(0, 0, d.get_idx()); } - invoke_fn(d.get_cfn(), d.get_arity()); + if (d.is_ffi()) + invoke_ffi_call(d.get_cfn(), d.get_sig()); + else + invoke_fn(d.get_cfn(), d.get_arity()); if (m_profiling) { unique_lock lk(m_call_stack_mtx); m_call_stack.pop_back(); @@ -3413,8 +3439,7 @@ void vm_state::run() { Similar to InvokeBuiltin */ - vm_decl decl = get_decl(instr.get_fn_idx()); - invoke_cfun(decl); + invoke_cfun(get_decl(instr.get_fn_idx())); goto main_loop; }} } diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index 40418a8607..00d10781a8 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -10,7 +10,11 @@ Author: Leonardo de Moura #include #include #include +#ifdef USE_FFI_FFI_H #include +#else +#include +#endif #include "util/debug.h" #include "util/compiler_hints.h" #include "util/rc.h" @@ -26,6 +30,8 @@ class vm_obj; class ts_vm_obj; enum class vm_obj_kind { Simple, Constructor, Closure, NativeClosure, MPZ, External }; +std::ostream &operator << (std::ostream &out, vm_obj_kind x); + /** \brief Base class for VM objects. \remark Simple objects are encoded as tagged pointers. */ @@ -530,11 +536,14 @@ class vm_instr; struct vm_cfun_sig { buffer m_args; + ffi_type *m_rtype; ffi_cif m_cif; vm_cfun_sig(ffi_abi abi, ffi_type & rtype, buffer && atypes); + unsigned arity() const { return m_args.size(); } }; -enum class vm_decl_kind { Bytecode, Builtin, CFun, FFICall }; +enum class vm_decl_kind { Bytecode, Builtin, CFun }; +using std::auto_ptr; /** \brief VM function/constant declaration cell */ struct vm_decl_cell { @@ -546,7 +555,7 @@ struct vm_decl_cell { list m_args_info; optional m_pos; optional m_olean; - optional m_sig; + auto_ptr m_sig; union { struct { unsigned m_code_size; @@ -557,7 +566,7 @@ struct vm_decl_cell { }; vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_function fn); vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_cfunction fn); - vm_decl_cell(name const & n, unsigned idx, vm_cfun_sig && sig, vm_cfunction fn); + vm_decl_cell(name const & n, unsigned idx, auto_ptr sig, vm_cfunction fn); vm_decl_cell(name const & n, unsigned idx, unsigned arity, unsigned code_sz, vm_instr const * code, list const & args_info, optional const & pos, optional const & olean); @@ -573,8 +582,8 @@ class vm_decl { vm_decl():m_ptr(nullptr) {} vm_decl(name const & n, unsigned idx, unsigned arity, vm_function fn): vm_decl(new vm_decl_cell(n, idx, arity, fn)) {} - vm_decl(name const & n, unsigned idx, vm_cfun_sig && sig, vm_cfunction fn): - vm_decl(new vm_decl_cell(n, idx, std::move(sig), fn)) {} + vm_decl(name const & n, unsigned idx, auto_ptr sig, vm_cfunction fn): + vm_decl(new vm_decl_cell(n, idx, sig, fn)) {} vm_decl(name const & n, unsigned idx, unsigned arity, vm_cfunction fn): vm_decl(new vm_decl_cell(n, idx, arity, fn)) {} vm_decl(name const & n, unsigned idx, unsigned arity, unsigned code_sz, vm_instr const * code, @@ -596,8 +605,10 @@ class vm_decl { bool is_bytecode() const { lean_assert(m_ptr); return m_ptr->m_kind == vm_decl_kind::Bytecode; } bool is_builtin() const { lean_assert(m_ptr); return m_ptr->m_kind == vm_decl_kind::Builtin; } bool is_cfun() const { lean_assert(m_ptr); return m_ptr->m_kind == vm_decl_kind::CFun; } + bool is_ffi() const { lean_assert(m_ptr); return is_cfun() && m_ptr->m_sig.get() != nullptr; } unsigned get_idx() const { lean_assert(m_ptr); return m_ptr->m_idx; } name get_name() const { lean_assert(m_ptr); return m_ptr->m_name; } + vm_cfun_sig const & get_sig() const { lean_assert(m_ptr && is_ffi()); return *m_ptr->m_sig; } unsigned get_arity() const { lean_assert(m_ptr); return m_ptr->m_arity; } unsigned get_code_size() const { lean_assert(is_bytecode()); return m_ptr->m_code_size; } vm_instr const * get_code() const { lean_assert(is_bytecode()); return m_ptr->m_code; } diff --git a/src/library/vm/vm_dynload.cpp b/src/library/vm/vm_dynload.cpp index 43e1362332..160be48ca5 100644 --- a/src/library/vm/vm_dynload.cpp +++ b/src/library/vm/vm_dynload.cpp @@ -8,6 +8,8 @@ Author: James King #include #include +#include "util/lean_path.h" + // #include "util/sstream.h" // #include "library/vm/vm_name.h" // #include "library/vm/vm_io.h" @@ -26,7 +28,6 @@ Author: James King #include "library/vm/vm_parser.h" #include "library/quote.h" #include "library/placeholder.h" -#include "frontends/lean/elaborator.h" // void get_shared_funcptr(string const & pathname) { @@ -40,27 +41,97 @@ namespace lean { using namespace std; ffi_type * to_ffi_type (expr const & e) { + if (is_constant(e, name("unsigned"))) { + return &ffi_type_uint32; + } else { + throw exception(sstream() << "unsupported ffi type: " << e); + } } - vm_decl vm_foreign_obj::get_cfun(name const & n, unsigned idx, string const & fun_name, - buffer const & _args, expr const & _t) { + vm_decl vm_foreign_obj_cell::get_cfun(name const & n, unsigned idx, string const & fun_name, + buffer const & _args, expr const & _rt) { vm_cfunction fn = reinterpret_cast(dlsym(m_handle, fun_name.c_str())); + if (!fn) { + auto err = dlerror(); + throw exception(err); } buffer args; - ffi_type rt; - vm_cfun_sig sig(FFI_DEFAULT_ABI, rt, std::move(args)); - return vm_decl(n, idx, std::move(sig), fn); + for (auto e : _args) { args.push_back(to_ffi_type(e)); } + ffi_type * rt = to_ffi_type(_rt); + auto_ptr sig(new vm_cfun_sig(FFI_DEFAULT_ABI, *rt, std::move(args))); + return vm_decl(n, idx, sig, fn); } - vm_foreign_obj::~vm_foreign_obj() { + vm_foreign_obj_cell::~vm_foreign_obj_cell() { dlclose(m_handle); } - shared_ptr load_foreign_obj(string const & fname) { + void vm_foreign_obj_cell::dealloc() { + delete this; + } + + vm_foreign_obj::vm_foreign_obj(string const & fname) { + auto root = get_leanpkg_path_file(); + push_dir _(root ? dirname(*root) : lgetcwd()); FOREIGN_OBJ handle = dlopen(fname.c_str(), RTLD_LAZY); if (!handle) { - throw exception(sstream() << "failed to load foreign lib: " << dlerror()); + throw exception(sstream() << "failed to load foreign lib: " << dlerror() << "\n" << root->c_str()); + } + m_ptr = new vm_foreign_obj_cell(handle, fname); + m_ptr->inc_ref(); + } + + static name * g_vm_ffi; + struct vm_ffi_attribute_data : public attr_data { + name m_obj; + optional m_c_fun; + vm_ffi_attribute_data() {} + vm_ffi_attribute_data(name const & obj, optional const & fn) : + m_obj(obj), m_c_fun(fn) {} + virtual unsigned hash() const override {return m_obj.hash();} + void write(serializer & s) const {s << m_obj << m_c_fun;} + void read(deserializer & d) { + d >> m_obj >> m_c_fun; } - return make_shared(vm_foreign_obj(handle, fname)); + void parse(abstract_parser & p) override { + lean_assert(dynamic_cast(&p)); + auto & p2 = *static_cast(&p); + auto n = p2.check_id_next("not an identifier"); + m_obj = n; + if (p2.curr_is_identifier()) { + m_c_fun = optional(p2.get_name_val()); + p2.next(); + } else { + m_c_fun = optional(); + } + } + }; + bool operator==(vm_ffi_attribute_data const & d1, vm_ffi_attribute_data const & d2) { + return d1.m_obj == d2.m_obj && + d1.m_c_fun == d2.m_c_fun; + } + + template class typed_attribute; + typedef typed_attribute vm_ffi_attribute; + + static vm_ffi_attribute const & get_vm_ffi_attribute() { + return static_cast(get_system_attribute(*g_vm_ffi)); + } + + + void initialize_vm_ffi() { + g_vm_ffi = new name("ffi"); + register_system_attribute(vm_ffi_attribute( + *g_vm_ffi, "Registers a binding to a foreign function.", + [](environment const & env, io_state const &, name const & d, unsigned, bool) -> environment { + auto data = get_vm_ffi_attribute().get(env, d); + name sym = data->m_c_fun? *data->m_c_fun : d; + auto b = add_foreign_symbol(env, data->m_obj, d, sym.to_string()); + return b; + })); + } + + void finalize_vm_ffi() { + delete g_vm_ffi; } static name * g_vm_ffi; diff --git a/src/library/vm/vm_dynload.h b/src/library/vm/vm_dynload.h index a81f43ec01..94c29f0522 100644 --- a/src/library/vm/vm_dynload.h +++ b/src/library/vm/vm_dynload.h @@ -8,17 +8,20 @@ namespace lean { using std::string; - class vm_foreign_obj { - private: - FOREIGN_OBJ m_handle; - std::string m_filename; - public: - vm_foreign_obj(FOREIGN_OBJ handle, string const & filename) - : m_handle(handle), + struct vm_foreign_obj_cell { + MK_LEAN_RC(); + FOREIGN_OBJ m_handle; + std::string m_filename; + vm_foreign_obj_cell(FOREIGN_OBJ handle, string const & filename) + : m_rc(0), m_handle(handle), m_filename(filename) {}; - ~vm_foreign_obj(); - vm_decl get_cfun(name const & n, unsigned idx, string const & fun_name, - buffer const & _args, expr const & _t); + ~vm_foreign_obj_cell(); + vm_decl get_cfun(name const & n, unsigned idx, string const & fun_name, + buffer const & _args, expr const & _t); + void dealloc(); + private: + vm_foreign_obj_cell(vm_foreign_obj_cell const &); + /* virtual void dealloc() override { */ /* this->~vm_foreign_obj(); */ /* get_vm_allocator().deallocate(sizeof(vm_foreign_obj), this); */ @@ -31,7 +34,29 @@ namespace lean { /* } */ }; - std::shared_ptr load_foreign_obj(string const & fname); + class vm_foreign_obj { + private: + vm_foreign_obj_cell * m_ptr; + public: + vm_foreign_obj():m_ptr(nullptr) {} + vm_foreign_obj(string const & fname); + vm_foreign_obj(vm_foreign_obj const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } + vm_foreign_obj(vm_foreign_obj && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } + vm_decl get_cfun(name const & n, unsigned idx, string const & fun_name, + buffer const & _args, expr const & _t) { + lean_assert(m_ptr); return m_ptr->get_cfun(n, idx, fun_name, _args, _t); } + vm_foreign_obj & operator=(vm_foreign_obj const & s) { LEAN_COPY_REF(s); } + vm_foreign_obj & operator=(vm_foreign_obj && s) { LEAN_MOVE_REF(s); } + + ~vm_foreign_obj() { if (m_ptr) { m_ptr->dec_ref(); } } + }; + + + /* std::shared_ptr load_foreign_obj(string const & fname); */ + + void initialize_vm_ffi(); + + void finalize_vm_ffi(); void initialize_vm_ffi(); diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp index f8221e98da..b8e8b2c53c 100644 --- a/src/library/vm/vm_environment.cpp +++ b/src/library/vm/vm_environment.cpp @@ -5,11 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#ifdef USE_FFI_FFI_H -#include -#else -#include -#endif #include "library/unfold_macros.h" #include "kernel/type_checker.h" #include "kernel/inductive/inductive.h" @@ -320,7 +315,6 @@ vm_obj environment_fingerprint(vm_obj const & env) { return mk_vm_nat(mpz(get_fingerprint(to_env(env)))); } -// environment load_foreign_object(environment const & env, name const & n, std::string const & file_name); vm_obj environment_load_foreign_object(vm_obj const & _env, vm_obj const & _n, vm_obj const & _file_name) { environment env = to_env(_env); name n = to_name(_n); @@ -328,19 +322,6 @@ vm_obj environment_load_foreign_object(vm_obj const & _env, vm_obj const & _n, v return to_obj(load_foreign_object(env,n,file_name)); } -// environment bind_foreign_symbol(environment const & env, name const & fo, name const & fn, -// unsigned arity, std::string const & symbol); -// vm_obj environment_bind_foreign_symbol(vm_obj const & _env, vm_obj const & _fo, vm_obj const & _fn, -// vm_obj const & _arity, vm_obj const & _symbol) { -// environment env = to_env(_env); -// name fo = to_name(_fo); -// name fn = to_name(_fn); -// expr type = env.get(fn).get_type(); -// unsigned arity = to_unsigned(_arity); -// std::string symbol = to_string(_symbol); -// return to_obj(bind_foreign_symbol(env,fo,fn,arity,symbol)); -// } - void initialize_vm_environment() { DECLARE_VM_BUILTIN(name({"environment", "mk_std"}), environment_mk_std); DECLARE_VM_BUILTIN(name({"environment", "trust_lvl"}), environment_trust_lvl); @@ -375,7 +356,6 @@ void initialize_vm_environment() { DECLARE_VM_BUILTIN(name({"environment", "get_class_attribute_symbols"}), environment_get_class_attribute_symbols); DECLARE_VM_BUILTIN(name({"environment", "fingerprint"}), environment_fingerprint); DECLARE_VM_BUILTIN(name({"environment", "load_foreign_object"}), environment_load_foreign_object); - // DECLARE_VM_BUILTIN(name({"environment", "bind_foreign_symbol"}), environment_bind_foreign_symbol); } void finalize_vm_environment() { diff --git a/src/util/path.cpp b/src/util/path.cpp index cb3d77c30e..b0faa21305 100644 --- a/src/util/path.cpp +++ b/src/util/path.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura, Gabriel Ebner #if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN) #include #endif +#include #include #include #include @@ -243,4 +244,25 @@ std::string lrealpath(std::string const & fname) { } #endif } + +std::string lgetcwd() { + char cd[PATH_MAX]; + getcwd(cd, sizeof(cd)); + return std::string(cd); +} + + +push_dir::push_dir(std::string const & cd) : push_dir(cd.c_str()) { } + +push_dir::push_dir(char const * cd) { + char parent[PATH_MAX]; + getcwd(parent, PATH_MAX); + m_parent = std::string(parent); + chdir(cd); +} + +push_dir::~push_dir() { + chdir(m_parent.c_str()); +} + } diff --git a/src/util/path.h b/src/util/path.h index 53f28b4cc2..24c67eb794 100644 --- a/src/util/path.h +++ b/src/util/path.h @@ -44,4 +44,16 @@ std::vector read_dir(std::string const & dirname); time_t get_mtime(std::string const & fname); std::string lrealpath(std::string const & fname); + +std::string lgetcwd(); + +class push_dir { + std::string m_parent; +public: + push_dir(std::string const &); + push_dir(char const *parent); + std::string const & parent() const { return m_parent; } + ~push_dir(); +}; + } diff --git a/tests/lean/vm_dynload/ffi.lean b/tests/lean/vm_dynload/ffi.lean index 6f34207350..84d208f198 100644 --- a/tests/lean/vm_dynload/ffi.lean +++ b/tests/lean/vm_dynload/ffi.lean @@ -1,3 +1,4 @@ +import system.io namespace tactic @@ -6,17 +7,28 @@ open environment meta def load_foreign_object (n : name) (str : string) : tactic unit := updateex_env $ λ env, pure $ env.load_foreign_object n str -meta def bind_foreign_symbol (fo fn : name) (arity : ℕ) (sym : string) : tactic unit := -updateex_env $ λ env, pure $ env.bind_foreign_symbol fo fn arity sym end tactic open tactic def main : unit → unit → unit := λ _, id +-- run_cmd file + run_cmd -do load_foreign_object `foo "/Users/simon/lean/lean-master/tests/lean/vm_dynload/some_file.so", - bind_foreign_symbol `foo `main 2 "main", +do + unsafe_run_io $ do + { io.env.get_cwd >>= io.print_ln, + (io.cmd { cmd := "make", args := ["some_file.so"] }) >>= io.print_ln }, + load_foreign_object `foo "vm_dynload/some_file.so", + -- bind_foreign_symbol `foo `main 2 "main", return () -#eval main () () +run_cmd trace "\nnext!\n" + +@[ffi foo] +constant my_fun : unsigned → unsigned → unsigned + +run_cmd trace "\nnext!\n" + +#eval my_fun 7 3 From e3d3d59699c2a85ddf76f15dfabc47b278daedbd Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Tue, 14 May 2019 13:43:22 -0400 Subject: [PATCH 21/36] fix lint issues --- src/cmake/Modules/cpplint.py | 7 +++ src/library/vm/CMakeLists.txt | 2 +- src/library/vm/init_module.cpp | 2 +- src/library/vm/vm.cpp | 6 +-- src/library/vm/vm.h | 10 ++--- src/library/vm/{vm_dynload.cpp => vm_ffi.cpp} | 44 ++++--------------- src/library/vm/{vm_dynload.h => vm_ffi.h} | 27 ++++-------- src/library/vm/vm_io.cpp | 3 +- src/util/path.cpp | 18 ++++---- src/util/path.h | 3 ++ 10 files changed, 49 insertions(+), 73 deletions(-) rename src/library/vm/{vm_dynload.cpp => vm_ffi.cpp} (82%) rename src/library/vm/{vm_dynload.h => vm_ffi.h} (66%) diff --git a/src/cmake/Modules/cpplint.py b/src/cmake/Modules/cpplint.py index 8f12409fea..21644bb450 100755 --- a/src/cmake/Modules/cpplint.py +++ b/src/cmake/Modules/cpplint.py @@ -3596,6 +3596,13 @@ def CheckCStyleCast(filename, linenum, line, raw_line, cast_type, pattern, # 'All parameters should be named in a function') # return True + # Added by Simon Hudon, 2019/05/14 + # e.g., sizeof(int) + # do not treat as a cast + sizeof_match = Match(r'.*sizeof\s*$', line[0:match.start(1) - 1]) + if sizeof_match: + return False + # At this point, all that should be left is actual casts. error(filename, linenum, 'readability/casting', 4, 'Using C-style cast. Use %s<%s>(...) instead' % diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt index 572f59ae06..f2f6e70b68 100644 --- a/src/library/vm/CMakeLists.txt +++ b/src/library/vm/CMakeLists.txt @@ -2,4 +2,4 @@ add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm vm_options.cpp vm_format.cpp vm_rb_map.cpp vm_level.cpp vm_expr.cpp vm_exceptional.cpp vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp vm_task.cpp vm_int.cpp init_module.cpp vm_parser.cpp vm_array.cpp - vm_pos_info.cpp vm_dynload.cpp) + vm_pos_info.cpp vm_ffi.cpp) diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp index a70f8ac8cd..bf88c84f7a 100644 --- a/src/library/vm/init_module.cpp +++ b/src/library/vm/init_module.cpp @@ -24,7 +24,7 @@ Author: Leonardo de Moura #include "library/vm/vm_parser.h" #include "library/vm/vm_array.h" #include "library/vm/vm_string.h" -#include "library/vm/vm_dynload.h" +#include "library/vm/vm_ffi.h" namespace lean { void initialize_vm_core_module() { diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index b0eb44b317..1a9edc3c82 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -32,7 +32,7 @@ Author: Leonardo de Moura #include "library/vm/vm_nat.h" #include "library/vm/vm_option.h" #include "library/vm/vm_expr.h" -#include "library/vm/vm_dynload.h" +#include "library/vm/vm_ffi.h" #include "library/normalize.h" #ifndef LEAN_DEFAULT_PROFILER_FREQ @@ -1042,8 +1042,8 @@ vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_cfun m_rc(0), m_kind(vm_decl_kind::CFun), m_name(n), m_idx(idx), m_arity(arity), m_cfn(fn) {} vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, - auto_ptr sig, vm_cfunction fn): - m_rc(0), m_kind(vm_decl_kind::CFun), m_name(n), m_idx(idx), m_arity(sig->arity()), m_sig(sig), m_cfn(fn) {} + unique_ptr sig, vm_cfunction fn): + m_rc(0), m_kind(vm_decl_kind::CFun), m_name(n), m_idx(idx), m_arity(sig->arity()), m_sig(std::move(sig)), m_cfn(fn) {} vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, unsigned code_sz, vm_instr const * code, list const & args_info, optional const & pos, diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index 00d10781a8..d8ec58075f 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -543,7 +543,7 @@ struct vm_cfun_sig { }; enum class vm_decl_kind { Bytecode, Builtin, CFun }; -using std::auto_ptr; +using std::unique_ptr; /** \brief VM function/constant declaration cell */ struct vm_decl_cell { @@ -555,7 +555,7 @@ struct vm_decl_cell { list m_args_info; optional m_pos; optional m_olean; - auto_ptr m_sig; + unique_ptr m_sig; union { struct { unsigned m_code_size; @@ -566,7 +566,7 @@ struct vm_decl_cell { }; vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_function fn); vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_cfunction fn); - vm_decl_cell(name const & n, unsigned idx, auto_ptr sig, vm_cfunction fn); + vm_decl_cell(name const & n, unsigned idx, unique_ptr sig, vm_cfunction fn); vm_decl_cell(name const & n, unsigned idx, unsigned arity, unsigned code_sz, vm_instr const * code, list const & args_info, optional const & pos, optional const & olean); @@ -582,8 +582,8 @@ class vm_decl { vm_decl():m_ptr(nullptr) {} vm_decl(name const & n, unsigned idx, unsigned arity, vm_function fn): vm_decl(new vm_decl_cell(n, idx, arity, fn)) {} - vm_decl(name const & n, unsigned idx, auto_ptr sig, vm_cfunction fn): - vm_decl(new vm_decl_cell(n, idx, sig, fn)) {} + vm_decl(name const & n, unsigned idx, unique_ptr sig, vm_cfunction fn): + vm_decl(new vm_decl_cell(n, idx, std::move(sig), fn)) {} vm_decl(name const & n, unsigned idx, unsigned arity, vm_cfunction fn): vm_decl(new vm_decl_cell(n, idx, arity, fn)) {} vm_decl(name const & n, unsigned idx, unsigned arity, unsigned code_sz, vm_instr const * code, diff --git a/src/library/vm/vm_dynload.cpp b/src/library/vm/vm_ffi.cpp similarity index 82% rename from src/library/vm/vm_dynload.cpp rename to src/library/vm/vm_ffi.cpp index 160be48ca5..3f99d03b5c 100644 --- a/src/library/vm/vm_dynload.cpp +++ b/src/library/vm/vm_ffi.cpp @@ -1,44 +1,19 @@ /* -Author: James King +Copyright (c) 2019 James King. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: James King , Simon Hudon */ #include #include #include -#include -#include #include "util/lean_path.h" - -// #include "util/sstream.h" -// #include "library/vm/vm_name.h" -// #include "library/vm/vm_io.h" -// #include "library/vm/vm_string.h" -#include "library/vm/vm_dynload.h" -// #include "library/attribute_manager.h" - -#include "kernel/abstract.h" -#include "library/constants.h" -#include "library/attribute_manager.h" -#include "library/scoped_ext.h" -#include "library/tactic/elaborator_exception.h" -#include "library/string.h" -#include "library/vm/vm.h" -#include "library/vm/vm_expr.h" +#include "library/vm/vm_ffi.h" #include "library/vm/vm_parser.h" -#include "library/quote.h" -#include "library/placeholder.h" - - -// void get_shared_funcptr(string const & pathname) { -// void* handle = dlopen(pathname.c_str(), RTLD_LAZY); -// if (!handle) { -// std::cerr << "Cannot load library: " << dlerror() << '\n'; -// } -// } namespace lean { -using namespace std; ffi_type * to_ffi_type (expr const & e) { if (is_constant(e, name("unsigned"))) { @@ -57,8 +32,8 @@ using namespace std; buffer args; for (auto e : _args) { args.push_back(to_ffi_type(e)); } ffi_type * rt = to_ffi_type(_rt); - auto_ptr sig(new vm_cfun_sig(FFI_DEFAULT_ABI, *rt, std::move(args))); - return vm_decl(n, idx, sig, fn); + unique_ptr sig(new vm_cfun_sig(FFI_DEFAULT_ABI, *rt, std::move(args))); + return vm_decl(n, idx, std::move(sig), fn); } vm_foreign_obj_cell::~vm_foreign_obj_cell() { @@ -72,9 +47,9 @@ using namespace std; vm_foreign_obj::vm_foreign_obj(string const & fname) { auto root = get_leanpkg_path_file(); push_dir _(root ? dirname(*root) : lgetcwd()); - FOREIGN_OBJ handle = dlopen(fname.c_str(), RTLD_LAZY); + vm_foreign_obj_cell::handle_t handle = dlopen(fname.c_str(), RTLD_LAZY); if (!handle) { - throw exception(sstream() << "failed to load foreign lib: " << dlerror() << "\n" << root->c_str()); + throw exception(sstream() << "failed to load foreign lib: " << dlerror()); } m_ptr = new vm_foreign_obj_cell(handle, fname); m_ptr->inc_ref(); @@ -117,7 +92,6 @@ using namespace std; return static_cast(get_system_attribute(*g_vm_ffi)); } - void initialize_vm_ffi() { g_vm_ffi = new name("ffi"); register_system_attribute(vm_ffi_attribute( diff --git a/src/library/vm/vm_dynload.h b/src/library/vm/vm_ffi.h similarity index 66% rename from src/library/vm/vm_dynload.h rename to src/library/vm/vm_ffi.h index 94c29f0522..593da019a9 100644 --- a/src/library/vm/vm_dynload.h +++ b/src/library/vm/vm_ffi.h @@ -1,18 +1,23 @@ +/* +Copyright (c) 2019 James King. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: James King , Simon Hudon +*/ #include #include #include "library/vm/vm.h" -#define FOREIGN_OBJ void * - namespace lean { using std::string; struct vm_foreign_obj_cell { MK_LEAN_RC(); - FOREIGN_OBJ m_handle; + typedef void * handle_t; + handle_t m_handle; std::string m_filename; - vm_foreign_obj_cell(FOREIGN_OBJ handle, string const & filename) + vm_foreign_obj_cell(handle_t handle, string const & filename) : m_rc(0), m_handle(handle), m_filename(filename) {}; ~vm_foreign_obj_cell(); @@ -21,17 +26,6 @@ namespace lean { void dealloc(); private: vm_foreign_obj_cell(vm_foreign_obj_cell const &); - - /* virtual void dealloc() override { */ - /* this->~vm_foreign_obj(); */ - /* get_vm_allocator().deallocate(sizeof(vm_foreign_obj), this); */ - /* } */ - /* virtual vm_external * clone(vm_clone_fn const &) override { */ - /* return new vm_foreign_obj(m_handle, m_filename); */ - /* } */ - /* virtual vm_external * ts_clone(vm_clone_fn const &) override { */ - /* return new (get_vm_allocator().allocate(sizeof(vm_foreign_obj))) vm_foreign_obj(m_handle, m_filename); */ - /* } */ }; class vm_foreign_obj { @@ -51,9 +45,6 @@ namespace lean { ~vm_foreign_obj() { if (m_ptr) { m_ptr->dec_ref(); } } }; - - /* std::shared_ptr load_foreign_obj(string const & fname); */ - void initialize_vm_ffi(); void finalize_vm_ffi(); diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp index d65d6e0a87..bdef91ce9f 100644 --- a/src/library/vm/vm_io.cpp +++ b/src/library/vm/vm_io.cpp @@ -59,6 +59,7 @@ Author: Leonardo de Moura #include #include "util/sstream.h" #include "util/utf8.h" +#include "util/path.h" #include "library/handle.h" #include "library/io_state.h" #include "library/constants.h" @@ -608,7 +609,7 @@ static vm_obj serial_deserialize(vm_obj const & h, vm_obj const &) { fseek(f, 0, SEEK_SET); char *data = reinterpret_cast(malloc(fsize)); - fread(data, fsize, 1, f); + ignore(fread(data, fsize, 1, f)); if (ferror(f)) { clearerr(f); return mk_io_failure("deserialize failed"); diff --git a/src/util/path.cpp b/src/util/path.cpp index b0faa21305..e5a861dbf1 100644 --- a/src/util/path.cpp +++ b/src/util/path.cpp @@ -71,7 +71,6 @@ std::string get_exe_location() { bool is_path_sep(char c) { return c == g_path_sep; } #else // Linux version -#include #include #include // NOLINT #include @@ -246,23 +245,24 @@ std::string lrealpath(std::string const & fname) { } std::string lgetcwd() { - char cd[PATH_MAX]; - getcwd(cd, sizeof(cd)); - return std::string(cd); + if (char * cd = getcwd(nullptr, 0)) { + std::string res(cd); + free(cd); + return res; + } else { + throw exception(strerror(errno)); + } } - push_dir::push_dir(std::string const & cd) : push_dir(cd.c_str()) { } push_dir::push_dir(char const * cd) { - char parent[PATH_MAX]; - getcwd(parent, PATH_MAX); - m_parent = std::string(parent); + m_parent = lgetcwd(); chdir(cd); } push_dir::~push_dir() { - chdir(m_parent.c_str()); + ignore(chdir(m_parent.c_str())); } } diff --git a/src/util/path.h b/src/util/path.h index 24c67eb794..317814e124 100644 --- a/src/util/path.h +++ b/src/util/path.h @@ -47,6 +47,9 @@ std::string lrealpath(std::string const & fname); std::string lgetcwd(); +template +void ignore(T) { } + class push_dir { std::string m_parent; public: From 71a550f7d3a55a5d4722d7bacdd92e8636186962 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Thu, 16 May 2019 15:06:32 -0400 Subject: [PATCH 22/36] add basic C data types --- library/init/data/int/basic.lean | 10 +++- library/init/data/int/order.lean | 32 +++++++++++++ library/init/meta/well_founded_tactics.lean | 5 ++ src/library/vm/vm.cpp | 51 +++++++++++++++++++-- src/library/vm/vm.h | 3 ++ src/library/vm/vm_ffi.cpp | 46 ++++++++++++++++++- src/library/vm/vm_int.cpp | 26 +++++++++++ src/library/vm/vm_int.h | 6 ++- src/library/vm/vm_nat.cpp | 26 +++++++++++ src/library/vm/vm_nat.h | 3 ++ tests/lean/{vm_dynload => }/ffi.lean | 14 +++--- tests/lean/ffi.lean.expected.out | 7 +++ tests/lean/vm_dynload/some_file.c | 4 +- 13 files changed, 216 insertions(+), 17 deletions(-) rename tests/lean/{vm_dynload => }/ffi.lean (58%) create mode 100644 tests/lean/ffi.lean.expected.out diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean index 4c10c0217f..9aa4339328 100644 --- a/library/init/data/int/basic.lean +++ b/library/init/data/int/basic.lean @@ -103,7 +103,7 @@ protected lemma coe_nat_zero : ↑(0 : ℕ) = (0 : ℤ) := rfl protected lemma coe_nat_one : ↑(1 : ℕ) = (1 : ℤ) := rfl protected lemma coe_nat_succ (n : ℕ) : (↑(succ n) : ℤ) = ↑n + 1 := rfl -protected lemma coe_nat_add_out (m n : ℕ) : ↑m + ↑n = (m + n : ℤ) := rfl +protected lemma coe_nat_add_out (m n : ℕ) : ↑m + ↑n = (↑(m + n) : ℤ) := rfl protected lemma coe_nat_mul_out (m n : ℕ) : ↑m * ↑n = (↑(m * n) : ℤ) := rfl protected lemma coe_nat_add_one_out (n : ℕ) : ↑n + (1 : ℤ) = ↑(succ n) := rfl @@ -265,7 +265,7 @@ protected def div : ℤ → ℤ → ℤ | -[1+ m] -[1+ n] := of_nat (succ (m / succ n)) protected def mod : ℤ → ℤ → ℤ -| (m : ℕ) n := (m % nat_abs n : ℕ) +| (of_nat m) n := of_nat (m % nat_abs n) | -[1+ m] n := sub_nat_nat (nat_abs n) (succ (m % nat_abs n)) -- F-rounding: This pair satisfies fdiv x y = floor (x / y) @@ -304,6 +304,12 @@ instance : has_mod ℤ := ⟨int.mod⟩ def gcd (m n : ℤ) : ℕ := gcd (nat_abs m) (nat_abs n) +/- div / mod -/ + +protected lemma coe_nat_div_out (m n : ℕ) : ↑m / ↑n = (↑(m / n) : ℤ) := rfl + +protected lemma coe_nat_mod_out (m n : ℕ) : ↑m % ↑n = (↑(m % n) : ℤ) := rfl + /- int is a ring -/ diff --git a/library/init/data/int/order.lean b/library/init/data/int/order.lean index b3f566eff3..f5006532fd 100644 --- a/library/init/data/int/order.lean +++ b/library/init/data/int/order.lean @@ -304,4 +304,36 @@ eq_of_mul_eq_mul_right Hpos (by rw [one_mul, H]) theorem eq_one_of_mul_eq_self_right {a b : ℤ} (Hpos : b ≠ 0) (H : b * a = b) : a = 1 := eq_of_mul_eq_mul_left Hpos (by rw [mul_one, H]) +lemma mod_lt {p q : ℤ} (h : 0 < q) : p % q < q := +begin + cases q; [ skip, cases h ], + have h₀ := lt_of_coe_nat_lt_coe_nat h, + cases p; dsimp [(%),int.mod,sub_nat_nat], + { apply coe_nat_lt_coe_nat_of_lt, apply nat.mod_lt _ h₀ }, + cases h' : (nat.succ (nat.mod p q) - q); + dsimp [sub_nat_nat._match_1], + { apply coe_nat_lt_coe_nat_of_lt, + apply nat.sub_lt h₀ (nat.zero_lt_succ _), }, + transitivity (0 : ℤ), apply neg_succ_lt_zero, + exact h, +end + +lemma nonneg_mod {p q : ℤ} (h : q ≠ 0) : 0 ≤ p % q := +begin + cases p; dsimp [(%),int.mod,sub_nat_nat], + apply of_nat_nonneg, + cases h₀ : (nat.succ (nat.mod p (nat_abs q)) - nat_abs q); + dsimp [sub_nat_nat._match_1,has_neg.neg], + { apply of_nat_nonneg }, + suffices h₁ : nat.succ (nat.mod p (nat_abs q)) - nat_abs q = 0, + { rw h₁ at h₀, cases h₀ }, + apply nat.sub_eq_zero_of_le, + apply nat.mod_lt, apply nat.pos_of_ne_zero, + intro h', apply h, + cases q, + { dsimp [nat_abs] at h', + rw h', refl }, + { cases h' } +end + end int diff --git a/library/init/meta/well_founded_tactics.lean b/library/init/meta/well_founded_tactics.lean index 9118d8fbab..b85072a2fb 100644 --- a/library/init/meta/well_founded_tactics.lean +++ b/library/init/meta/well_founded_tactics.lean @@ -12,6 +12,11 @@ lemma nat.lt_add_of_zero_lt_left (a b : nat) (h : 0 < b) : a < a + b := suffices a + 0 < a + b, by {simp at this, assumption}, by {apply nat.add_lt_add_left, assumption} +/- TODO(Leo): move this lemma, or delete it after we add algebraic normalizer. -/ +lemma nat.lt_add_of_zero_lt_right (a b : nat) (h : 0 < b) : a < b + a := +suffices 0 + a < b + a, by {simp at this ⊢, assumption}, +by {apply nat.add_lt_add_right, assumption} + /- TODO(Leo): move this lemma, or delete it after we add algebraic normalizer. -/ lemma nat.zero_lt_one_add (a : nat) : 0 < 1 + a := suffices 0 < a + 1, by {simp, assumption}, diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 1a9edc3c82..bf5d7110b9 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -30,6 +30,7 @@ Author: Leonardo de Moura #include "library/vm/vm.h" #include "library/vm/vm_name.h" #include "library/vm/vm_nat.h" +#include "library/vm/vm_int.h" #include "library/vm/vm_option.h" #include "library/vm/vm_expr.h" #include "library/vm/vm_ffi.h" @@ -1616,8 +1617,29 @@ void ffi_push(T const & x, buffer & vals, buffer & supp) { void ffi_from_obj(ffi_type const * t, vm_obj const & obj, buffer & vals, buffer & supp) { - if (t == &ffi_type_uint32) { - unsigned i = force_to_unsigned(obj, 0); + if (t == &ffi_type_sint8) { + char i = force_to_int(obj, 0); + ffi_push(i, vals, supp); + } else if (t == &ffi_type_sint16) { + short i = force_to_int(obj, 0); + ffi_push(i, vals, supp); + } else if (t == &ffi_type_sint32) { + int i = force_to_int(obj, 0); + ffi_push(i, vals, supp); + } else if (t == &ffi_type_sint64) { + long i = force_to_long(obj, 0); + ffi_push(i, vals, supp); + } else if (t == &ffi_type_uint8) { + unsigned char i = force_to_unsigned(obj, 0); + ffi_push(i, vals, supp); + } else if (t == &ffi_type_uint16) { + unsigned short i = force_to_unsigned(obj, 0); + ffi_push(i, vals, supp); + } else if (t == &ffi_type_uint32) { + unsigned int i = force_to_unsigned(obj, 0); + ffi_push(i, vals, supp); + } else if (t == &ffi_type_uint64) { + unsigned long i = force_to_unsigned_long(obj, 0); ffi_push(i, vals, supp); } else { throw exception("unsupported argument type"); @@ -1625,8 +1647,29 @@ void ffi_from_obj(ffi_type const * t, vm_obj const & obj, } vm_obj ffi_to_obj(ffi_type const * t, ffi_arg v) { - if (t == &ffi_type_uint32) { - unsigned *p = reinterpret_cast(&v); + if (t == &ffi_type_sint8) { + char *p = reinterpret_cast(&v); + return mk_vm_int(*p); + } else if (t == &ffi_type_sint16) { + short *p = reinterpret_cast(&v); + return mk_vm_int(*p); + } else if (t == &ffi_type_sint32) { + int *p = reinterpret_cast(&v); + return mk_vm_int(*p); + } else if (t == &ffi_type_sint64) { + long *p = reinterpret_cast(&v); + return mk_vm_int(*p); + } else if (t == &ffi_type_uint8) { + unsigned char *p = reinterpret_cast(&v); + return mk_vm_nat(*p); + } else if (t == &ffi_type_uint16) { + unsigned short *p = reinterpret_cast(&v); + return mk_vm_nat(*p); + } else if (t == &ffi_type_uint32) { + unsigned int *p = reinterpret_cast(&v); + return mk_vm_nat(*p); + } else if (t == &ffi_type_uint64) { + unsigned long *p = reinterpret_cast(&v); return mk_vm_nat(*p); } else { throw exception("unsupported argument type"); diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index d8ec58075f..9c315b9a48 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -265,6 +265,9 @@ inline vm_obj mk_vm_external(vm_external * obj) { lean_assert(obj && obj->get_rc /* helper functions for creating natural numbers */ vm_obj mk_vm_nat(unsigned n); vm_obj mk_vm_nat(mpz const & n); +vm_obj mk_vm_int(int n); +vm_obj mk_vm_int(mpz const & n); + inline vm_obj mk_vm_unit() { return mk_vm_simple(0); } inline vm_obj mk_vm_false() { return mk_vm_simple(0); } inline vm_obj mk_vm_true() { return mk_vm_simple(1); } diff --git a/src/library/vm/vm_ffi.cpp b/src/library/vm/vm_ffi.cpp index 3f99d03b5c..c643cfb82d 100644 --- a/src/library/vm/vm_ffi.cpp +++ b/src/library/vm/vm_ffi.cpp @@ -15,9 +15,35 @@ Author: James King , Simon Hudon namespace lean { + static name * g_vm_ffi; + + // types + static name * g_uint8_name; + static name * g_uint16_name; + static name * g_uint32_name; + static name * g_uint64_name; + static name * g_int8_name; + static name * g_int16_name; + static name * g_int32_name; + static name * g_int64_name; + ffi_type * to_ffi_type (expr const & e) { - if (is_constant(e, name("unsigned"))) { + if (is_constant(e, *g_uint8_name)) { + return &ffi_type_uint8; + } else if (is_constant(e, *g_uint16_name)) { + return &ffi_type_uint16; + } else if (is_constant(e, *g_uint32_name)) { return &ffi_type_uint32; + } else if (is_constant(e, *g_uint64_name)) { + return &ffi_type_uint64; + } else if (is_constant(e, *g_int8_name)) { + return &ffi_type_sint8; + } else if (is_constant(e, *g_int16_name)) { + return &ffi_type_sint16; + } else if (is_constant(e, *g_int32_name)) { + return &ffi_type_sint32; + } else if (is_constant(e, *g_int64_name)) { + return &ffi_type_sint64; } else { throw exception(sstream() << "unsupported ffi type: " << e); } @@ -55,7 +81,6 @@ namespace lean { m_ptr->inc_ref(); } - static name * g_vm_ffi; struct vm_ffi_attribute_data : public attr_data { name m_obj; optional m_c_fun; @@ -94,6 +119,15 @@ namespace lean { void initialize_vm_ffi() { g_vm_ffi = new name("ffi"); + g_uint8_name = new name ({"foreign", "uint_8"}); + g_uint16_name = new name ({"foreign", "uint_16"}); + g_uint32_name = new name ({"foreign", "uint_32"}); + g_uint64_name = new name ({"foreign", "uint_64"}); + g_int8_name = new name ({"foreign", "int_8"}); + g_int16_name = new name ({"foreign", "int_16"}); + g_int32_name = new name ({"foreign", "int_32"}); + g_int64_name = new name ({"foreign", "int_64"}); + register_system_attribute(vm_ffi_attribute( *g_vm_ffi, "Registers a binding to a foreign function.", [](environment const & env, io_state const &, name const & d, unsigned, bool) -> environment { @@ -106,6 +140,14 @@ namespace lean { void finalize_vm_ffi() { delete g_vm_ffi; + delete g_uint8_name; + delete g_uint16_name; + delete g_uint32_name; + delete g_uint64_name; + delete g_int8_name; + delete g_int16_name; + delete g_int32_name; + delete g_int64_name; } static name * g_vm_ffi; diff --git a/src/library/vm/vm_int.cpp b/src/library/vm/vm_int.cpp index fd6fc95494..c15c552e17 100644 --- a/src/library/vm/vm_int.cpp +++ b/src/library/vm/vm_int.cpp @@ -73,6 +73,32 @@ int force_to_int(vm_obj const & o, int def) { return def; } +long int to_long(vm_obj const & o) { + if (is_simple(o)) + return to_small_int(o); + else + return to_mpz(o).get_long_int(); +} + +optional try_to_long(vm_obj const & o) { + if (is_simple(o)) { + return optional(to_small_int(o)); + } else { + mpz const & v = to_mpz(o); + if (v.is_long_int()) + return optional(v.get_long_int()); + else + return optional(); + } +} + +long force_to_long(vm_obj const & o, long def) { + if (auto r = try_to_long(o)) + return *r; + else + return def; +} + MK_THREAD_LOCAL_GET_DEF(mpz, get_mpz1); MK_THREAD_LOCAL_GET_DEF(mpz, get_mpz2); diff --git a/src/library/vm/vm_int.h b/src/library/vm/vm_int.h index dd1f73ea27..8a04b103b3 100644 --- a/src/library/vm/vm_int.h +++ b/src/library/vm/vm_int.h @@ -5,12 +5,16 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #include "library/vm/vm.h" namespace lean { int to_int(vm_obj const & o); optional try_to_int(vm_obj const & o); -int force_to_int(vm_obj const & o, int def); +int force_to_int(vm_obj const & o, int def = std::numeric_limits::max()); +long to_long(vm_obj const & o); +optional try_to_long(vm_obj const & o); +long force_to_long(vm_obj const & o, long def = std::numeric_limits::max()); void initialize_vm_int(); void finalize_vm_int(); } diff --git a/src/library/vm/vm_nat.cpp b/src/library/vm/vm_nat.cpp index fac32dcc9d..f4c55c7082 100644 --- a/src/library/vm/vm_nat.cpp +++ b/src/library/vm/vm_nat.cpp @@ -52,6 +52,32 @@ unsigned force_to_unsigned(vm_obj const & o, unsigned def) { return def; } +unsigned long to_unsigned_long(vm_obj const & o) { + if (LEAN_LIKELY(is_simple(o))) + return cidx(o); + else + return to_mpz(o).get_unsigned_long_int(); +} + +optional try_to_unsigned_long(vm_obj const & o) { + if (LEAN_LIKELY(is_simple(o))) { + return optional(cidx(o)); + } else { + mpz const & v = to_mpz(o); + if (v.is_unsigned_long_int()) + return optional(v.get_unsigned_long_int()); + else + return optional(); + } +} + +unsigned long force_to_unsigned_long(vm_obj const & o, unsigned long def) { + if (auto r = try_to_unsigned_long(o)) + return *r; + else + return def; +} + size_t force_to_size_t(vm_obj const & o, size_t def) { // TODO(Leo): fix size_t is 8 bytes in 64-bit machines if (auto r = try_to_unsigned(o)) diff --git a/src/library/vm/vm_nat.h b/src/library/vm/vm_nat.h index a422c89a61..7b9188dfab 100644 --- a/src/library/vm/vm_nat.h +++ b/src/library/vm/vm_nat.h @@ -12,6 +12,9 @@ namespace lean { unsigned to_unsigned(vm_obj const & o); optional try_to_unsigned(vm_obj const & o); unsigned force_to_unsigned(vm_obj const & o, unsigned def = std::numeric_limits::max()); +unsigned long to_unsigned_long(vm_obj const & o); +optional try_to_unsigned_long(vm_obj const & o); +unsigned long force_to_unsigned_long(vm_obj const & o, unsigned long def = std::numeric_limits::max()); size_t force_to_size_t(vm_obj const & o, size_t def = std::numeric_limits::max()); /* Auxiliary function for converting vm_obj representing numerals into mpz. diff --git a/tests/lean/vm_dynload/ffi.lean b/tests/lean/ffi.lean similarity index 58% rename from tests/lean/vm_dynload/ffi.lean rename to tests/lean/ffi.lean index 84d208f198..b9f318ad96 100644 --- a/tests/lean/vm_dynload/ffi.lean +++ b/tests/lean/ffi.lean @@ -1,4 +1,5 @@ import system.io +import system.foreign namespace tactic @@ -9,17 +10,19 @@ updateex_env $ λ env, pure $ env.load_foreign_object n str end tactic -open tactic +open tactic foreign def main : unit → unit → unit := λ _, id --- run_cmd file - run_cmd do unsafe_run_io $ do { io.env.get_cwd >>= io.print_ln, - (io.cmd { cmd := "make", args := ["some_file.so"] }) >>= io.print_ln }, + b ← io.fs.dir_exists "vm_dynload", + io.env.set_cwd "vm_dynload", + b ← io.fs.file_exists "some_file.so", + if b then io.fs.remove "some_file.so" else pure (), + (io.cmd { cmd := "make", args := ["some_file.so"] }) >>= io.print_ln }, load_foreign_object `foo "vm_dynload/some_file.so", -- bind_foreign_symbol `foo `main 2 "main", return () @@ -27,8 +30,7 @@ do run_cmd trace "\nnext!\n" @[ffi foo] -constant my_fun : unsigned → unsigned → unsigned +constant my_fun : uint_32 → int_64 → int_64 -run_cmd trace "\nnext!\n" #eval my_fun 7 3 diff --git a/tests/lean/ffi.lean.expected.out b/tests/lean/ffi.lean.expected.out new file mode 100644 index 0000000000..2e275c7cd4 --- /dev/null +++ b/tests/lean/ffi.lean.expected.out @@ -0,0 +1,7 @@ +/Users/simon/lean/lean-master/tests/lean +gcc some_file.o -shared -o some_file.so + + +next! + +21 diff --git a/tests/lean/vm_dynload/some_file.c b/tests/lean/vm_dynload/some_file.c index 10c5f988bd..a3a600ff4f 100644 --- a/tests/lean/vm_dynload/some_file.c +++ b/tests/lean/vm_dynload/some_file.c @@ -1,7 +1,7 @@ #include -int my_fun (int x, int y) { - printf("hello world: %d\n", x + y); +long my_fun (int x, long y) { + printf("hello world: %ld\n", (long)x + y); return x * y; } From 9131709818afa8882f5a7d75a90f8cea2ba7821e Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Thu, 16 May 2019 16:59:28 -0400 Subject: [PATCH 23/36] fix merging issues --- library/system/foreign.lean | 176 ++++++++++++++++++++++++++++++ src/library/tactic/vm_monitor.cpp | 1 - src/library/vm/vm.cpp | 17 +-- src/library/vm/vm_ffi.cpp | 48 -------- 4 files changed, 177 insertions(+), 65 deletions(-) create mode 100644 library/system/foreign.lean diff --git a/library/system/foreign.lean b/library/system/foreign.lean new file mode 100644 index 0000000000..9f8e37ee1b --- /dev/null +++ b/library/system/foreign.lean @@ -0,0 +1,176 @@ +namespace foreign + +open nat + +def bounded (a p q : ℤ) := p ≤ a ∧ a < q + +structure irange (l u : ℤ) := +(val : ℤ) +(bounded : bounded val l u) + +namespace irange + +protected def lt {p q} (a b : irange p q) : Prop := +a.val < b.val + +protected def le {p q} (a b : irange p q) : Prop := +a.val ≤ b.val + +instance {p q} : has_lt (irange p q) := ⟨irange.lt⟩ +instance {p q} : has_le (irange p q) := ⟨irange.le⟩ + +instance decidable_lt {p q} (a b : irange p q) : decidable (a < b) := +int.decidable_lt _ _ + +instance decidable_le {p q} (a b : irange p q) : decidable (a ≤ b) := +int.decidable_le _ _ + +def {u} elim0 {α : Sort u} {p} : irange p p → α +| ⟨_, h₀, h₁⟩ := false.elim (not_lt_of_ge h₀ h₁) + +variable {n : nat} + +lemma eq_of_veq {p q} : ∀ {i j : irange p q}, (val i) = (val j) → i = j +| ⟨iv, ilt₁, glt₁⟩ ⟨.(iv), ilt₂, glt₂⟩ rfl := rfl + +lemma veq_of_eq {p q} : ∀ {i j : irange p q}, i = j → (val i) = (val j) +| ⟨iv, ilt, igt⟩ .(_) rfl := rfl + +lemma ne_of_vne {p q} {i j : irange p q} (h : val i ≠ val j) : i ≠ j := +λ h', absurd (veq_of_eq h') h + +lemma vne_of_ne {p q} {i j : irange p q} (h : i ≠ j) : val i ≠ val j := +λ h', absurd (eq_of_veq h') h + +end irange + +open irange + +instance (p q : ℤ) : decidable_eq (irange p q) := +λ i j, decidable_of_decidable_of_iff + (int.decidable_eq i.val j.val) ⟨eq_of_veq, veq_of_eq⟩ + +namespace irange +open int +variables {p q : int} + +protected def succ : irange p q → irange p (q+1) +| ⟨a, h, h'⟩ := ⟨a+1, le_trans h (le_add_of_nonneg_right zero_le_one), add_lt_add_right h' _⟩ + +section truncate + +def truncate (x p q : ℤ) := (x - p) % (q - p) + p + +variables {x : ℤ} {p q} +variables (y : ℤ) (h : p ≤ y) (h' : y < q) + +private lemma pos_q_sub_p : 0 < (q - p) := +sub_pos_of_lt (lt_of_le_of_lt h h') + +private lemma q_sub_p_ne_zero : (q - p) ≠ 0 := +ne_of_gt (pos_q_sub_p _ h h') + +lemma le_truncate : p ≤ truncate x p q := +le_add_of_sub_right_le $ +suffices 0 ≤ (x - p) % (q - p), by simp * at *, +int.nonneg_mod (q_sub_p_ne_zero _ h h') + +lemma truncate_lt : truncate x p q < q := +add_lt_of_lt_sub_right $ int.mod_lt $ pos_q_sub_p y h h' + +lemma bounded_truncate (h : foreign.bounded y p q) : foreign.bounded (truncate x p q) p q := +⟨ le_truncate _ h.1 h.2, truncate_lt _ h.1 h.2 ⟩ + +lemma bounded_zero {p q : ℕ} : foreign.bounded 0 (-p) q.succ := +⟨ neg_le_of_neg_le (coe_nat_le_coe_nat_of_le $ nat.zero_le _), coe_nat_lt_coe_nat_of_lt (nat.zero_lt_succ _) ⟩ + +end truncate + +def of_int {p q : ℕ} (a : int) : irange (- p) q.succ := +⟨ truncate a (-p) (succ q), bounded_truncate 0 bounded_zero ⟩ + +protected def add : irange p q → irange p q → irange p q +| ⟨a, h⟩ ⟨b, _⟩ := ⟨truncate (a + b) p q, bounded_truncate _ h⟩ + +protected def mul : irange p q → irange p q → irange p q +| ⟨a, h⟩ ⟨b, _⟩ := ⟨truncate (a * b) p q, bounded_truncate _ h⟩ + +protected def sub : irange p q → irange p q → irange p q +| ⟨a, h⟩ ⟨b, _⟩ := ⟨truncate (a - b) p q, bounded_truncate _ h⟩ + +protected def mod : irange p q → irange p q → irange p q +| ⟨a, h⟩ ⟨b, _⟩ := ⟨truncate (a % b) p q, bounded_truncate _ h⟩ + +protected def div : irange p q → irange p q → irange p q +| ⟨a, h⟩ ⟨b, _⟩ := ⟨truncate (a / b) p q, bounded_truncate _ h⟩ + +instance {p q : ℕ} : has_zero (irange (-p) q.succ) := ⟨of_int 0⟩ +instance {p q : ℕ} : has_one (irange (-p) q.succ) := ⟨of_int 1⟩ +instance : has_add (irange p q) := ⟨irange.add⟩ +instance : has_sub (irange p q) := ⟨irange.sub⟩ +instance : has_mul (irange p q) := ⟨irange.mul⟩ +instance : has_mod (irange p q) := ⟨irange.mod⟩ +instance : has_div (irange p q) := ⟨irange.div⟩ +instance : has_repr (irange p q) := ⟨repr ∘ irange.val⟩ + +lemma of_int_zero {p q : ℕ} : @of_int p q 0 = 0 := rfl + +lemma add_def (a b : irange p q) : (a + b).val = truncate (a.val + b.val) p q := +show (irange.add a b).val = truncate (a.val + b.val) p q, from +by cases a; cases b; simp [irange.add] + +lemma mul_def (a b : irange p q) : (a * b).val = truncate (a.val * b.val) p q := +show (irange.mul a b).val = truncate (a.val * b.val) p q, from +by cases a; cases b; simp [irange.mul] + +lemma sub_def (a b : irange p q) : (a - b).val = truncate (a.val - b.val) p q := +show (irange.sub a b).val = truncate (a.val - b.val) p q, from +by cases a; cases b; simp [irange.sub] + +lemma mod_def (a b : irange p q) : (a % b).val = truncate (a.val % b.val) p q := +show (irange.mod a b).val = truncate (a.val % b.val) p q, from +by cases a; cases b; simp [irange.mod] + +lemma div_def (a b : irange p q) : (a / b).val = truncate (a.val / b.val) p q := +show (irange.div a b).val = truncate (a.val / b.val) p q, from +by cases a; cases b; simp [irange.div] + +lemma lt_def (a b : irange p q) : (a < b) = (a.val < b.val) := +show (irange.lt a b) = (a.val < b.val), from +by cases a; cases b; simp [irange.lt] + +lemma le_def (a b : irange p q) : (a ≤ b) = (a.val ≤ b.val) := +show (irange.le a b) = (a.val ≤ b.val), from +by cases a; cases b; simp [irange.le] + +lemma val_zero {p q : ℕ} : (0 : irange (-p) q.succ).val = 0 := +show truncate 0 _ _ = 0, from +sub_eq_zero_of_eq $ +begin + suffices : p % (q.succ + p) = p, + { conv { to_rhs, rw ← this }, simp, refl }, + apply mod_eq_of_lt, apply lt_add_of_zero_lt_right, + apply zero_lt_succ, +end + +end irange + +@[reducible] +def uint_8 := fin $ succ 255 +@[reducible] +def uint_16 := fin $ succ 65535 +@[reducible] +def uint_32 := unsigned +@[reducible] +def uint_64 := fin $ succ 18446744073709551615 + +@[reducible] +def int_8 := irange (-succ 127) (succ 127) +@[reducible] +def int_16 := irange (-succ 32767) (succ 32767) +@[reducible] +def int_32 := irange (-succ 2147483647) (succ 2147483647) +@[reducible] +def int_64 := irange (-succ 9223372036854775807) (succ 9223372036854775807) + +end foreign diff --git a/src/library/tactic/vm_monitor.cpp b/src/library/tactic/vm_monitor.cpp index 4cb550776f..c41e913aef 100644 --- a/src/library/tactic/vm_monitor.cpp +++ b/src/library/tactic/vm_monitor.cpp @@ -191,7 +191,6 @@ vm_obj _vm_decl_kind(vm_obj const & d) { case vm_decl_kind::Bytecode: return mk_vm_simple(0); case vm_decl_kind::Builtin: return mk_vm_simple(1); case vm_decl_kind::CFun: return mk_vm_simple(2); - case vm_decl_kind::FFICall: return mk_vm_simple(3); } lean_unreachable(); } diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index bf5d7110b9..db66c9483e 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -1180,7 +1180,7 @@ struct vm_decls : public environment_extension { void bind_foreign_symbol(name const & obj, name const & decl, string const & c_fun, buffer const & args, expr const & t) { auto idx = get_vm_index(decl); - m_decls.insert(idx, m_foreign[obj]->get_cfun(decl, idx, c_fun, args, t)); + m_decls.insert(idx, m_foreign[obj].get_cfun(decl, idx, c_fun, args, t)); } unsigned reserve(name const & n, unsigned arity) { @@ -1804,9 +1804,6 @@ vm_obj vm_state::invoke_closure(vm_obj const & fn, unsigned DEBUG_CODE(nargs)) { case vm_decl_kind::CFun: invoke_cfun(d); break; - case vm_decl_kind::FFICall: - invoke_ffi_call(d); - break; } m_pc = saved_pc; vm_obj r = m_stack.back(); @@ -2955,18 +2952,6 @@ void vm_state::invoke_cfun(vm_decl const & d) { } } -void vm_state::invoke_ffi_call(vm_decl const & d) { - if (m_profiling) { - unique_lock lk(m_call_stack_mtx); - push_frame_core(0, 0, d.get_idx()); - } - invoke_ffi_call(d.get_cfn(), d.m_sig); - if (m_profiling) { - unique_lock lk(m_call_stack_mtx); - m_call_stack.pop_back(); - } -} - void vm_state::invoke(vm_decl const & d) { switch (d.kind()) { case vm_decl_kind::Bytecode: diff --git a/src/library/vm/vm_ffi.cpp b/src/library/vm/vm_ffi.cpp index c643cfb82d..e692ae9f6b 100644 --- a/src/library/vm/vm_ffi.cpp +++ b/src/library/vm/vm_ffi.cpp @@ -150,52 +150,4 @@ namespace lean { delete g_int64_name; } - static name * g_vm_ffi; - struct vm_ffi_attribute_data : public attr_data { - name m_obj; - optional m_c_fun; - vm_ffi_attribute_data() {} - // vm_ffi_attribute_data(name const & n) : m_name(n) {} - // virtual unsigned hash() const override {return m_name.hash();} - void write(serializer & s) const {s << m_obj << m_c_fun;} - void read(deserializer & d) { - d >> m_obj >> m_c_fun; - } - void parse(abstract_parser & p) override { - lean_assert(dynamic_cast(&p)); - auto & p2 = *static_cast(&p); - m_obj = p2.check_constant_next("not a constant"); - if (p2.curr_is_identifier()) { - m_c_fun = optional(p2.get_name_val()); - p2.next(); - } else { - m_c_fun = optional(); - } - } - }; - // bool operator==(vm_ffi_attribute_data const & d1, vm_ffi_attribute_data const & d2) { - // return d1.m_name == d2.m_name; - // } - - template class typed_attribute; - typedef typed_attribute vm_ffi_attribute; - - static vm_ffi_attribute const & get_vm_ffi_attribute() { - return static_cast(get_system_attribute(*g_vm_ffi)); - } - - - void initialize_vm_ffi() { - register_system_attribute(basic_attribute( - "ffi", "Registers a binding to a foreign function.", - [](environment const & env, io_state const &, name const & d, unsigned, bool) -> environment { - auto data = get_vm_ffi_attribute().get(env, d); - name sym = data->m_c_fun? *data->m_c_fun : data->m_obj; - return add_foreign_symbol(env, d, data->m_obj, sym.to_string()); - })); - } - - void finalize_vm_ffi() { - } - } From c2205e4dfa7b579039d5ac558f650a6040a8566d Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Thu, 16 May 2019 22:23:00 -0400 Subject: [PATCH 24/36] Add conditional include paths for libffi on linux --- src/library/vm/vm.cpp | 6 +++++- src/library/vm/vm.h | 6 +++--- src/library/vm/vm_ffi.cpp | 6 +++++- 3 files changed, 13 insertions(+), 5 deletions(-) diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index db66c9483e..032e47601e 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -8,7 +8,11 @@ Author: Leonardo de Moura #include #include #include -#include +#ifdef __linux__ + #include +#else + #include +#endif #include #include #include diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index 9c315b9a48..c3bfc5e9f7 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -10,10 +10,10 @@ Author: Leonardo de Moura #include #include #include -#ifdef USE_FFI_FFI_H -#include -#else +#ifdef __linux__ #include +#else +#include #endif #include "util/debug.h" #include "util/compiler_hints.h" diff --git a/src/library/vm/vm_ffi.cpp b/src/library/vm/vm_ffi.cpp index e692ae9f6b..5da3692512 100644 --- a/src/library/vm/vm_ffi.cpp +++ b/src/library/vm/vm_ffi.cpp @@ -6,7 +6,11 @@ Author: James King , Simon Hudon */ #include -#include +#ifdef __linux__ + #include +#else + #include +#endif #include #include "util/lean_path.h" From 88ef7cc93b83f45a6ce0df92b2cbe01e3fd91065 Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Thu, 16 May 2019 22:23:23 -0400 Subject: [PATCH 25/36] Update tests/lean/ffi.lean Fix relative paths to work on linux --- tests/lean/ffi.lean | 5 +++-- tests/lean/vm_dynload/Makefile | 2 +- tests/lean/vm_dynload/client.c | 2 +- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/tests/lean/ffi.lean b/tests/lean/ffi.lean index b9f318ad96..d48358e0c2 100644 --- a/tests/lean/ffi.lean +++ b/tests/lean/ffi.lean @@ -22,8 +22,9 @@ do io.env.set_cwd "vm_dynload", b ← io.fs.file_exists "some_file.so", if b then io.fs.remove "some_file.so" else pure (), - (io.cmd { cmd := "make", args := ["some_file.so"] }) >>= io.print_ln }, - load_foreign_object `foo "vm_dynload/some_file.so", + (io.cmd { cmd := "make", args := ["some_file.so"] }) >>= io.print_ln, + io.env.set_cwd ".." }, + load_foreign_object `foo "./vm_dynload/some_file.so", -- bind_foreign_symbol `foo `main 2 "main", return () diff --git a/tests/lean/vm_dynload/Makefile b/tests/lean/vm_dynload/Makefile index 122cc98c24..22a0a01409 100644 --- a/tests/lean/vm_dynload/Makefile +++ b/tests/lean/vm_dynload/Makefile @@ -12,4 +12,4 @@ some_file.so: some_file.o gcc some_file.o -shared -o some_file.so client: client.c - gcc client.c -o client -I$(INCLUDES) -lffi + gcc client.c -o client -I$(INCLUDES) -lffi -ldl diff --git a/tests/lean/vm_dynload/client.c b/tests/lean/vm_dynload/client.c index 9c644b26cb..043465e970 100644 --- a/tests/lean/vm_dynload/client.c +++ b/tests/lean/vm_dynload/client.c @@ -29,7 +29,7 @@ void call(main_fn fn, int x, int y) { int main () { main_fn my_main; - void* handle = dlopen("some_file.so", RTLD_LAZY); + void* handle = dlopen("./some_file.so", RTLD_LAZY); if (!handle) { printf("Cannot load library: %s", dlerror()); return -1; From 35ebbcdc0bc7a5dac50c486c846808eb4be61d41 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Thu, 16 May 2019 16:59:28 -0400 Subject: [PATCH 26/36] fix merging issues --- library/system/foreign.lean | 176 ++++++++++++++++++++++++++++++ src/library/tactic/vm_monitor.cpp | 1 - src/library/vm/vm.cpp | 18 +-- src/library/vm/vm_ffi.cpp | 49 --------- 4 files changed, 177 insertions(+), 67 deletions(-) create mode 100644 library/system/foreign.lean diff --git a/library/system/foreign.lean b/library/system/foreign.lean new file mode 100644 index 0000000000..9f8e37ee1b --- /dev/null +++ b/library/system/foreign.lean @@ -0,0 +1,176 @@ +namespace foreign + +open nat + +def bounded (a p q : ℤ) := p ≤ a ∧ a < q + +structure irange (l u : ℤ) := +(val : ℤ) +(bounded : bounded val l u) + +namespace irange + +protected def lt {p q} (a b : irange p q) : Prop := +a.val < b.val + +protected def le {p q} (a b : irange p q) : Prop := +a.val ≤ b.val + +instance {p q} : has_lt (irange p q) := ⟨irange.lt⟩ +instance {p q} : has_le (irange p q) := ⟨irange.le⟩ + +instance decidable_lt {p q} (a b : irange p q) : decidable (a < b) := +int.decidable_lt _ _ + +instance decidable_le {p q} (a b : irange p q) : decidable (a ≤ b) := +int.decidable_le _ _ + +def {u} elim0 {α : Sort u} {p} : irange p p → α +| ⟨_, h₀, h₁⟩ := false.elim (not_lt_of_ge h₀ h₁) + +variable {n : nat} + +lemma eq_of_veq {p q} : ∀ {i j : irange p q}, (val i) = (val j) → i = j +| ⟨iv, ilt₁, glt₁⟩ ⟨.(iv), ilt₂, glt₂⟩ rfl := rfl + +lemma veq_of_eq {p q} : ∀ {i j : irange p q}, i = j → (val i) = (val j) +| ⟨iv, ilt, igt⟩ .(_) rfl := rfl + +lemma ne_of_vne {p q} {i j : irange p q} (h : val i ≠ val j) : i ≠ j := +λ h', absurd (veq_of_eq h') h + +lemma vne_of_ne {p q} {i j : irange p q} (h : i ≠ j) : val i ≠ val j := +λ h', absurd (eq_of_veq h') h + +end irange + +open irange + +instance (p q : ℤ) : decidable_eq (irange p q) := +λ i j, decidable_of_decidable_of_iff + (int.decidable_eq i.val j.val) ⟨eq_of_veq, veq_of_eq⟩ + +namespace irange +open int +variables {p q : int} + +protected def succ : irange p q → irange p (q+1) +| ⟨a, h, h'⟩ := ⟨a+1, le_trans h (le_add_of_nonneg_right zero_le_one), add_lt_add_right h' _⟩ + +section truncate + +def truncate (x p q : ℤ) := (x - p) % (q - p) + p + +variables {x : ℤ} {p q} +variables (y : ℤ) (h : p ≤ y) (h' : y < q) + +private lemma pos_q_sub_p : 0 < (q - p) := +sub_pos_of_lt (lt_of_le_of_lt h h') + +private lemma q_sub_p_ne_zero : (q - p) ≠ 0 := +ne_of_gt (pos_q_sub_p _ h h') + +lemma le_truncate : p ≤ truncate x p q := +le_add_of_sub_right_le $ +suffices 0 ≤ (x - p) % (q - p), by simp * at *, +int.nonneg_mod (q_sub_p_ne_zero _ h h') + +lemma truncate_lt : truncate x p q < q := +add_lt_of_lt_sub_right $ int.mod_lt $ pos_q_sub_p y h h' + +lemma bounded_truncate (h : foreign.bounded y p q) : foreign.bounded (truncate x p q) p q := +⟨ le_truncate _ h.1 h.2, truncate_lt _ h.1 h.2 ⟩ + +lemma bounded_zero {p q : ℕ} : foreign.bounded 0 (-p) q.succ := +⟨ neg_le_of_neg_le (coe_nat_le_coe_nat_of_le $ nat.zero_le _), coe_nat_lt_coe_nat_of_lt (nat.zero_lt_succ _) ⟩ + +end truncate + +def of_int {p q : ℕ} (a : int) : irange (- p) q.succ := +⟨ truncate a (-p) (succ q), bounded_truncate 0 bounded_zero ⟩ + +protected def add : irange p q → irange p q → irange p q +| ⟨a, h⟩ ⟨b, _⟩ := ⟨truncate (a + b) p q, bounded_truncate _ h⟩ + +protected def mul : irange p q → irange p q → irange p q +| ⟨a, h⟩ ⟨b, _⟩ := ⟨truncate (a * b) p q, bounded_truncate _ h⟩ + +protected def sub : irange p q → irange p q → irange p q +| ⟨a, h⟩ ⟨b, _⟩ := ⟨truncate (a - b) p q, bounded_truncate _ h⟩ + +protected def mod : irange p q → irange p q → irange p q +| ⟨a, h⟩ ⟨b, _⟩ := ⟨truncate (a % b) p q, bounded_truncate _ h⟩ + +protected def div : irange p q → irange p q → irange p q +| ⟨a, h⟩ ⟨b, _⟩ := ⟨truncate (a / b) p q, bounded_truncate _ h⟩ + +instance {p q : ℕ} : has_zero (irange (-p) q.succ) := ⟨of_int 0⟩ +instance {p q : ℕ} : has_one (irange (-p) q.succ) := ⟨of_int 1⟩ +instance : has_add (irange p q) := ⟨irange.add⟩ +instance : has_sub (irange p q) := ⟨irange.sub⟩ +instance : has_mul (irange p q) := ⟨irange.mul⟩ +instance : has_mod (irange p q) := ⟨irange.mod⟩ +instance : has_div (irange p q) := ⟨irange.div⟩ +instance : has_repr (irange p q) := ⟨repr ∘ irange.val⟩ + +lemma of_int_zero {p q : ℕ} : @of_int p q 0 = 0 := rfl + +lemma add_def (a b : irange p q) : (a + b).val = truncate (a.val + b.val) p q := +show (irange.add a b).val = truncate (a.val + b.val) p q, from +by cases a; cases b; simp [irange.add] + +lemma mul_def (a b : irange p q) : (a * b).val = truncate (a.val * b.val) p q := +show (irange.mul a b).val = truncate (a.val * b.val) p q, from +by cases a; cases b; simp [irange.mul] + +lemma sub_def (a b : irange p q) : (a - b).val = truncate (a.val - b.val) p q := +show (irange.sub a b).val = truncate (a.val - b.val) p q, from +by cases a; cases b; simp [irange.sub] + +lemma mod_def (a b : irange p q) : (a % b).val = truncate (a.val % b.val) p q := +show (irange.mod a b).val = truncate (a.val % b.val) p q, from +by cases a; cases b; simp [irange.mod] + +lemma div_def (a b : irange p q) : (a / b).val = truncate (a.val / b.val) p q := +show (irange.div a b).val = truncate (a.val / b.val) p q, from +by cases a; cases b; simp [irange.div] + +lemma lt_def (a b : irange p q) : (a < b) = (a.val < b.val) := +show (irange.lt a b) = (a.val < b.val), from +by cases a; cases b; simp [irange.lt] + +lemma le_def (a b : irange p q) : (a ≤ b) = (a.val ≤ b.val) := +show (irange.le a b) = (a.val ≤ b.val), from +by cases a; cases b; simp [irange.le] + +lemma val_zero {p q : ℕ} : (0 : irange (-p) q.succ).val = 0 := +show truncate 0 _ _ = 0, from +sub_eq_zero_of_eq $ +begin + suffices : p % (q.succ + p) = p, + { conv { to_rhs, rw ← this }, simp, refl }, + apply mod_eq_of_lt, apply lt_add_of_zero_lt_right, + apply zero_lt_succ, +end + +end irange + +@[reducible] +def uint_8 := fin $ succ 255 +@[reducible] +def uint_16 := fin $ succ 65535 +@[reducible] +def uint_32 := unsigned +@[reducible] +def uint_64 := fin $ succ 18446744073709551615 + +@[reducible] +def int_8 := irange (-succ 127) (succ 127) +@[reducible] +def int_16 := irange (-succ 32767) (succ 32767) +@[reducible] +def int_32 := irange (-succ 2147483647) (succ 2147483647) +@[reducible] +def int_64 := irange (-succ 9223372036854775807) (succ 9223372036854775807) + +end foreign diff --git a/src/library/tactic/vm_monitor.cpp b/src/library/tactic/vm_monitor.cpp index 4cb550776f..c41e913aef 100644 --- a/src/library/tactic/vm_monitor.cpp +++ b/src/library/tactic/vm_monitor.cpp @@ -191,7 +191,6 @@ vm_obj _vm_decl_kind(vm_obj const & d) { case vm_decl_kind::Bytecode: return mk_vm_simple(0); case vm_decl_kind::Builtin: return mk_vm_simple(1); case vm_decl_kind::CFun: return mk_vm_simple(2); - case vm_decl_kind::FFICall: return mk_vm_simple(3); } lean_unreachable(); } diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index bf5d7110b9..549bac0751 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -8,7 +8,6 @@ Author: Leonardo de Moura #include #include #include -#include #include #include #include @@ -1180,7 +1179,7 @@ struct vm_decls : public environment_extension { void bind_foreign_symbol(name const & obj, name const & decl, string const & c_fun, buffer const & args, expr const & t) { auto idx = get_vm_index(decl); - m_decls.insert(idx, m_foreign[obj]->get_cfun(decl, idx, c_fun, args, t)); + m_decls.insert(idx, m_foreign[obj].get_cfun(decl, idx, c_fun, args, t)); } unsigned reserve(name const & n, unsigned arity) { @@ -1804,9 +1803,6 @@ vm_obj vm_state::invoke_closure(vm_obj const & fn, unsigned DEBUG_CODE(nargs)) { case vm_decl_kind::CFun: invoke_cfun(d); break; - case vm_decl_kind::FFICall: - invoke_ffi_call(d); - break; } m_pc = saved_pc; vm_obj r = m_stack.back(); @@ -2955,18 +2951,6 @@ void vm_state::invoke_cfun(vm_decl const & d) { } } -void vm_state::invoke_ffi_call(vm_decl const & d) { - if (m_profiling) { - unique_lock lk(m_call_stack_mtx); - push_frame_core(0, 0, d.get_idx()); - } - invoke_ffi_call(d.get_cfn(), d.m_sig); - if (m_profiling) { - unique_lock lk(m_call_stack_mtx); - m_call_stack.pop_back(); - } -} - void vm_state::invoke(vm_decl const & d) { switch (d.kind()) { case vm_decl_kind::Bytecode: diff --git a/src/library/vm/vm_ffi.cpp b/src/library/vm/vm_ffi.cpp index c643cfb82d..6734a10c0e 100644 --- a/src/library/vm/vm_ffi.cpp +++ b/src/library/vm/vm_ffi.cpp @@ -6,7 +6,6 @@ Author: James King , Simon Hudon */ #include -#include #include #include "util/lean_path.h" @@ -150,52 +149,4 @@ namespace lean { delete g_int64_name; } - static name * g_vm_ffi; - struct vm_ffi_attribute_data : public attr_data { - name m_obj; - optional m_c_fun; - vm_ffi_attribute_data() {} - // vm_ffi_attribute_data(name const & n) : m_name(n) {} - // virtual unsigned hash() const override {return m_name.hash();} - void write(serializer & s) const {s << m_obj << m_c_fun;} - void read(deserializer & d) { - d >> m_obj >> m_c_fun; - } - void parse(abstract_parser & p) override { - lean_assert(dynamic_cast(&p)); - auto & p2 = *static_cast(&p); - m_obj = p2.check_constant_next("not a constant"); - if (p2.curr_is_identifier()) { - m_c_fun = optional(p2.get_name_val()); - p2.next(); - } else { - m_c_fun = optional(); - } - } - }; - // bool operator==(vm_ffi_attribute_data const & d1, vm_ffi_attribute_data const & d2) { - // return d1.m_name == d2.m_name; - // } - - template class typed_attribute; - typedef typed_attribute vm_ffi_attribute; - - static vm_ffi_attribute const & get_vm_ffi_attribute() { - return static_cast(get_system_attribute(*g_vm_ffi)); - } - - - void initialize_vm_ffi() { - register_system_attribute(basic_attribute( - "ffi", "Registers a binding to a foreign function.", - [](environment const & env, io_state const &, name const & d, unsigned, bool) -> environment { - auto data = get_vm_ffi_attribute().get(env, d); - name sym = data->m_c_fun? *data->m_c_fun : data->m_obj; - return add_foreign_symbol(env, d, data->m_obj, sym.to_string()); - })); - } - - void finalize_vm_ffi() { - } - } From ffb85f6e92329b6f13b3011245e7e2e4808a9899 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Fri, 17 May 2019 21:13:05 -0400 Subject: [PATCH 27/36] some fixes --- src/library/vm/vm_environment.cpp | 2 +- tests/lean/ffi.lean | 3 ++- tests/lean/ffi.lean.expected.out | 1 + tests/lean/vm_dynload/some_file.c | 3 --- 4 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp index b8e8b2c53c..dfc4af286e 100644 --- a/src/library/vm/vm_environment.cpp +++ b/src/library/vm/vm_environment.cpp @@ -319,7 +319,7 @@ vm_obj environment_load_foreign_object(vm_obj const & _env, vm_obj const & _n, v environment env = to_env(_env); name n = to_name(_n); std::string file_name = to_string(_file_name); - return to_obj(load_foreign_object(env,n,file_name)); + return to_obj(load_foreign_object(env, n, file_name)); } void initialize_vm_environment() { diff --git a/tests/lean/ffi.lean b/tests/lean/ffi.lean index b9f318ad96..407dec8466 100644 --- a/tests/lean/ffi.lean +++ b/tests/lean/ffi.lean @@ -22,9 +22,10 @@ do io.env.set_cwd "vm_dynload", b ← io.fs.file_exists "some_file.so", if b then io.fs.remove "some_file.so" else pure (), + b ← io.fs.file_exists "some_file.o", + if b then io.fs.remove "some_file.o" else pure (), (io.cmd { cmd := "make", args := ["some_file.so"] }) >>= io.print_ln }, load_foreign_object `foo "vm_dynload/some_file.so", - -- bind_foreign_symbol `foo `main 2 "main", return () run_cmd trace "\nnext!\n" diff --git a/tests/lean/ffi.lean.expected.out b/tests/lean/ffi.lean.expected.out index 2e275c7cd4..847d2e4925 100644 --- a/tests/lean/ffi.lean.expected.out +++ b/tests/lean/ffi.lean.expected.out @@ -1,4 +1,5 @@ /Users/simon/lean/lean-master/tests/lean +gcc -c -fPIC some_file.c -o some_file.o -I/usr/local/lib/libffi-3.2.1/include gcc some_file.o -shared -o some_file.so diff --git a/tests/lean/vm_dynload/some_file.c b/tests/lean/vm_dynload/some_file.c index a3a600ff4f..28d0da2491 100644 --- a/tests/lean/vm_dynload/some_file.c +++ b/tests/lean/vm_dynload/some_file.c @@ -1,7 +1,4 @@ -#include - long my_fun (int x, long y) { - printf("hello world: %ld\n", (long)x + y); return x * y; } From f743e1b31e2f3e3f9d9f38c2358fac1434138111 Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Fri, 17 May 2019 21:58:13 -0400 Subject: [PATCH 28/36] Modify src/library/vm/vm_environment.cpp Normalize the file path handed to `load_foreign_object` --- src/library/vm/vm_environment.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp index b8e8b2c53c..de86098df3 100644 --- a/src/library/vm/vm_environment.cpp +++ b/src/library/vm/vm_environment.cpp @@ -32,6 +32,7 @@ Author: Leonardo de Moura #include "library/vm/vm_pos_info.h" #include "library/vm/vm_rb_map.h" #include "frontends/lean/structure_cmd.h" +#include "util/path.h" namespace lean { struct vm_environment : public vm_external { @@ -319,7 +320,7 @@ vm_obj environment_load_foreign_object(vm_obj const & _env, vm_obj const & _n, v environment env = to_env(_env); name n = to_name(_n); std::string file_name = to_string(_file_name); - return to_obj(load_foreign_object(env,n,file_name)); + return to_obj(load_foreign_object(env, n, normalize_path(file_name))); } void initialize_vm_environment() { From 14df4156193a59e93a5d817f8f36076b1920506a Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Sat, 18 May 2019 16:11:20 -0400 Subject: [PATCH 29/36] remove absolute path from ffi test --- tests/lean/ffi.lean | 7 +++---- tests/lean/ffi.lean.expected.out | 1 - 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/tests/lean/ffi.lean b/tests/lean/ffi.lean index a84c4099d5..e9679144af 100644 --- a/tests/lean/ffi.lean +++ b/tests/lean/ffi.lean @@ -17,11 +17,10 @@ def main : unit → unit → unit := λ _, id run_cmd do unsafe_run_io $ do - { io.env.get_cwd >>= io.print_ln, - b ← io.fs.dir_exists "vm_dynload", + { b ← io.fs.dir_exists "vm_dynload", io.env.set_cwd "vm_dynload", - b ← io.fs.file_exists "some_file.so", - if b then io.fs.remove "some_file.so" else pure (), + io.catch (io.fs.remove "some_file.so") (λ _, pure ()), + io.catch (io.fs.remove "some_file.o") (λ _, pure ()), (io.cmd { cmd := "make", args := ["some_file.so"] }) >>= io.print_ln, io.env.set_cwd ".." }, load_foreign_object `foo "./vm_dynload/some_file.so", diff --git a/tests/lean/ffi.lean.expected.out b/tests/lean/ffi.lean.expected.out index 847d2e4925..ca92140d4d 100644 --- a/tests/lean/ffi.lean.expected.out +++ b/tests/lean/ffi.lean.expected.out @@ -1,4 +1,3 @@ -/Users/simon/lean/lean-master/tests/lean gcc -c -fPIC some_file.c -o some_file.o -I/usr/local/lib/libffi-3.2.1/include gcc some_file.o -shared -o some_file.so From 03a3e523626f705ed0c876a0063dd7b2aecc4c56 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Sat, 18 May 2019 16:30:30 -0400 Subject: [PATCH 30/36] install libffi on windows [skip travis] --- .appveyor.yml | 61 ++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 60 insertions(+), 1 deletion(-) diff --git a/.appveyor.yml b/.appveyor.yml index 2081038d2a..24aa57b044 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -1,7 +1,11 @@ image: Visual Studio 2017 - +skip_branch_with_pr: true environment: MSYSTEM: MINGW64 # use MSYS2 shell + CYG_ROOT: C:/cygwin + CYG_CACHE: C:/cygwin/var/cache/setup + CYG_MIRROR: http://mirrors.kernel.org/sourceware/cygwin/ + VSVER: 15 matrix: - CFG: MINGW64 UPLOAD: ON @@ -13,6 +17,61 @@ install: # upgrade git for vcpkg: https://github.com/appveyor/ci/issues/2097 - if %CFG% == MSVC (choco upgrade git -y & vcpkg install mpir:x64-windows) + # install cygwin + - ps: >- + If ($env:Platform -Match "x86") { + $env:VCVARS_PLATFORM="x86" + $env:BUILD="i686-pc-cygwin" + $env:HOST="i686-pc-cygwin" + $env:MSVCC="/cygdrive/c/projects/lean/libffi-3.3-rc0/msvcc.sh" + $env:SRC_ARCHITECTURE="x86" + } ElseIf ($env:Platform -Match "arm") { + $env:VCVARS_PLATFORM="x86_arm" + $env:BUILD="i686-pc-cygwin" + $env:HOST="arm-w32-cygwin" + $env:MSVCC="/cygdrive/c/projects/lean/libffi-3.3-rc0/msvcc.sh -marm" + $env:SRC_ARCHITECTURE="arm" + } Else { + $env:VCVARS_PLATFORM="amd64" + $env:BUILD="x86_64-w64-cygwin" + $env:HOST="x86_64-w64-cygwin" + $env:MSVCC="/cygdrive/c/projects/lean/libffi-3.3-rc0/msvcc.sh -m64" + $env:SRC_ARCHITECTURE="x86" + } + - 'appveyor DownloadFile https://cygwin.com/setup-x86.exe -FileName setup.exe' + - 'setup.exe -qnNdO -R "%CYG_ROOT%" -s "%CYG_MIRROR%" -l "%CYG_CACHE%" -P dejagnu >NUL' + - '%CYG_ROOT%/bin/bash -lc "cygcheck -dc cygwin"' + - echo call VsDevCmd to set VS150COMNTOOLS + - call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\Common7\Tools\VsDevCmd.bat" + - ps: $env:VSCOMNTOOLS=(Get-Content ("env:VS" + "$env:VSVER" + "0COMNTOOLS")) + - echo "Using Visual Studio %VSVER%.0 at %VSCOMNTOOLS%" + - call "%VSCOMNTOOLS%..\..\vc\Auxiliary\Build\vcvarsall.bat" %VCVARS_PLATFORM% + + # through cyg-get + # - alias cyg-get="setup.exe -q -P" + - pip install paramiko --force-reinstall + - choco install libffi-dev + # - setup.exe -q -P cygwin32-gcc-g++ + # - gcc-core gcc-g++ git libffi-devel nano openssl openssl-devel python-crypto python2 python2-devel python2-openssl python2-pip python2-setuptools tree + + # # install libffi + # - 'appveyor DownloadFile https://github.com/libffi/libffi/releases/download/v3.3-rc0/libffi-3.3-rc0.tar.gz -FileName libffi-3.3-rc0.tar.gz' + # - pwd + # - c:\cygwin\bin\sh -lc 'pwd' + # - c:\cygwin\bin\sh -lc 'echo $OLDPWD' + # - c:\cygwin\bin\sh -lc '(cd $OLDPWD; tar xvzf libffi-3.3-rc0.tar.gz)' + # - cd libffi-3.3-rc0 + # - ls + # # - sh ./configure --disable-docs CC='%MSVCC%' CXX='%MSVCC%' LD=link CPP="cl -nologo -EP" + # # - sh -lc 'make' + # # - sh -lc 'make install' + # # - c:\cygwin\bin\sh -lc "(cd $OLDPWD; ./configure CC='%MSVCC%' CXX='%MSVCC%' LD='link' CPP='cl -nologo -EP' CXXCPP='cl -nologo -EP' CPPFLAGS='-DFFI_BUILDING_DLL' AR='/cygdrive/c/projects/lean/libffi-3.3-rc0/.travis/ar-lib lib' NM='dumpbin -symbols' STRIP=':' --build=$BUILD --host=$HOST;)" + # - c:\cygwin\bin\sh -lc "(cd $OLDPWD; ./configure CC='%MSVCC%' CXX='%MSVCC%' LD='link' CPP='cl -nologo -EP' CXXCPP='cl -nologo -EP' AR='/cygdrive/c/projects/lean/libffi-3.3-rc0/.travis/ar-lib lib' NM='dumpbin -symbols' STRIP=':' --build=$BUILD --host=$HOST;)" + # - c:\cygwin\bin\sh -lc '(cd $OLDPWD; make;)' + # - c:\cygwin\bin\sh -lc "(cd $OLDPWD; cp src/%SRC_ARCHITECTURE%/ffitarget.h include; make; find .;)" + # # - c:\cygwin\bin\sh -lc "(cd $OLDPWD; cp `find . -name 'libffi-?.dll'` $HOST/testsuite/; make check; cat `find ./ -name libffi.log`)" + # - c:\cygwin\bin\sh -lc '(cd $OLDPWD; make install;)' + build_script: - call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\VC\Auxiliary\Build\vcvars64.bat" - cd %APPVEYOR_BUILD_FOLDER% && mkdir build && cd build From 45de7d136f3eea4597e2297765ea9a4de816d79d Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Sun, 19 May 2019 19:28:03 -0400 Subject: [PATCH 31/36] get libffi from ftp [skip travis] --- .appveyor.yml | 31 ++++++++++++++++++------------- 1 file changed, 18 insertions(+), 13 deletions(-) diff --git a/.appveyor.yml b/.appveyor.yml index 24aa57b044..7e0ec2701d 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -6,6 +6,7 @@ environment: CYG_CACHE: C:/cygwin/var/cache/setup CYG_MIRROR: http://mirrors.kernel.org/sourceware/cygwin/ VSVER: 15 + LIBFFI_V: 3.2 matrix: - CFG: MINGW64 UPLOAD: ON @@ -23,19 +24,19 @@ install: $env:VCVARS_PLATFORM="x86" $env:BUILD="i686-pc-cygwin" $env:HOST="i686-pc-cygwin" - $env:MSVCC="/cygdrive/c/projects/lean/libffi-3.3-rc0/msvcc.sh" + $env:MSVCC="/cygdrive/c/projects/lean/libffi-%LIBFFI_V%/msvcc.sh" $env:SRC_ARCHITECTURE="x86" } ElseIf ($env:Platform -Match "arm") { $env:VCVARS_PLATFORM="x86_arm" $env:BUILD="i686-pc-cygwin" $env:HOST="arm-w32-cygwin" - $env:MSVCC="/cygdrive/c/projects/lean/libffi-3.3-rc0/msvcc.sh -marm" + $env:MSVCC="/cygdrive/c/projects/lean/libffi-%LIBFFI_V%/msvcc.sh -marm" $env:SRC_ARCHITECTURE="arm" } Else { $env:VCVARS_PLATFORM="amd64" $env:BUILD="x86_64-w64-cygwin" $env:HOST="x86_64-w64-cygwin" - $env:MSVCC="/cygdrive/c/projects/lean/libffi-3.3-rc0/msvcc.sh -m64" + $env:MSVCC="/cygdrive/c/projects/lean/libffi-%LIBFFI_V%/msvcc.sh -m64" $env:SRC_ARCHITECTURE="x86" } - 'appveyor DownloadFile https://cygwin.com/setup-x86.exe -FileName setup.exe' @@ -49,28 +50,32 @@ install: # through cyg-get # - alias cyg-get="setup.exe -q -P" - - pip install paramiko --force-reinstall - - choco install libffi-dev + # - pip install paramiko --force-reinstall + # - choco install libffi-dev # - setup.exe -q -P cygwin32-gcc-g++ # - gcc-core gcc-g++ git libffi-devel nano openssl openssl-devel python-crypto python2 python2-devel python2-openssl python2-pip python2-setuptools tree # # install libffi - # - 'appveyor DownloadFile https://github.com/libffi/libffi/releases/download/v3.3-rc0/libffi-3.3-rc0.tar.gz -FileName libffi-3.3-rc0.tar.gz' + # - 'appveyor DownloadFile https://github.com/libffi/libffi/releases/download/v3.3-rc0/libffi-3.3-rc0.tar.gz -FileName libffi.tar.gz' + # - 'appveyor DownloadFile ftp://sourceware.org/pub/libffi/libffi-%LIBFFI_V%.tar.gz -FileName libffi.tar.gz' + # - 'Install-Package libffi -Version 3.2.1.1' + - 'nuget install libffi' + - curl -fsS -o libffi.tar.gz ftp://sourceware.org/pub/libffi/libffi-%LIBFFI_V%.tar.gz # - pwd # - c:\cygwin\bin\sh -lc 'pwd' # - c:\cygwin\bin\sh -lc 'echo $OLDPWD' - # - c:\cygwin\bin\sh -lc '(cd $OLDPWD; tar xvzf libffi-3.3-rc0.tar.gz)' - # - cd libffi-3.3-rc0 + - c:\cygwin\bin\sh -lc '(cd $OLDPWD; tar xvzf libffi-rc0.tar.gz)' + # - cd libffi-%LIBFFI_V% # - ls # # - sh ./configure --disable-docs CC='%MSVCC%' CXX='%MSVCC%' LD=link CPP="cl -nologo -EP" # # - sh -lc 'make' # # - sh -lc 'make install' - # # - c:\cygwin\bin\sh -lc "(cd $OLDPWD; ./configure CC='%MSVCC%' CXX='%MSVCC%' LD='link' CPP='cl -nologo -EP' CXXCPP='cl -nologo -EP' CPPFLAGS='-DFFI_BUILDING_DLL' AR='/cygdrive/c/projects/lean/libffi-3.3-rc0/.travis/ar-lib lib' NM='dumpbin -symbols' STRIP=':' --build=$BUILD --host=$HOST;)" - # - c:\cygwin\bin\sh -lc "(cd $OLDPWD; ./configure CC='%MSVCC%' CXX='%MSVCC%' LD='link' CPP='cl -nologo -EP' CXXCPP='cl -nologo -EP' AR='/cygdrive/c/projects/lean/libffi-3.3-rc0/.travis/ar-lib lib' NM='dumpbin -symbols' STRIP=':' --build=$BUILD --host=$HOST;)" - # - c:\cygwin\bin\sh -lc '(cd $OLDPWD; make;)' - # - c:\cygwin\bin\sh -lc "(cd $OLDPWD; cp src/%SRC_ARCHITECTURE%/ffitarget.h include; make; find .;)" + # # - c:\cygwin\bin\sh -lc "(cd $OLDPWD; ./configure CC='%MSVCC%' CXX='%MSVCC%' LD='link' CPP='cl -nologo -EP' CXXCPP='cl -nologo -EP' CPPFLAGS='-DFFI_BUILDING_DLL' AR='/cygdrive/c/projects/lean/libffi-%LIBFFI_V%/.travis/ar-lib lib' NM='dumpbin -symbols' STRIP=':' --build=$BUILD --host=$HOST;)" + - c:\cygwin\bin\sh -lc "(cd $OLDPWD; ./configure CC='%MSVCC%' CXX='%MSVCC%' LD='link' CPP='cl -nologo -EP' CXXCPP='cl -nologo -EP' AR='/cygdrive/c/projects/lean/libffi-%LIBFFI_V%/.travis/ar-lib lib' NM='dumpbin -symbols' STRIP=':' --build=$BUILD --host=$HOST;)" + - c:\cygwin\bin\sh -lc '(cd $OLDPWD; make;)' + - c:\cygwin\bin\sh -lc "(cd $OLDPWD; cp src/%SRC_ARCHITECTURE%/ffitarget.h include; make; find .;)" # # - c:\cygwin\bin\sh -lc "(cd $OLDPWD; cp `find . -name 'libffi-?.dll'` $HOST/testsuite/; make check; cat `find ./ -name libffi.log`)" - # - c:\cygwin\bin\sh -lc '(cd $OLDPWD; make install;)' + - c:\cygwin\bin\sh -lc '(cd $OLDPWD; make install;)' build_script: - call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\VC\Auxiliary\Build\vcvars64.bat" From 55307ac7893e8583e98ec0589649aafcf3365ad0 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Sun, 19 May 2019 19:54:31 -0400 Subject: [PATCH 32/36] with nuget [skip travis] --- .appveyor.yml | 72 ++++++++++++++------------------------- src/CMakeLists.txt | 7 ++-- src/library/vm/vm.cpp | 6 ++-- src/library/vm/vm.h | 6 ++-- src/library/vm/vm_ffi.cpp | 6 ++-- 5 files changed, 40 insertions(+), 57 deletions(-) diff --git a/.appveyor.yml b/.appveyor.yml index 7e0ec2701d..1340c6efea 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -18,35 +18,13 @@ install: # upgrade git for vcpkg: https://github.com/appveyor/ci/issues/2097 - if %CFG% == MSVC (choco upgrade git -y & vcpkg install mpir:x64-windows) - # install cygwin - - ps: >- - If ($env:Platform -Match "x86") { - $env:VCVARS_PLATFORM="x86" - $env:BUILD="i686-pc-cygwin" - $env:HOST="i686-pc-cygwin" - $env:MSVCC="/cygdrive/c/projects/lean/libffi-%LIBFFI_V%/msvcc.sh" - $env:SRC_ARCHITECTURE="x86" - } ElseIf ($env:Platform -Match "arm") { - $env:VCVARS_PLATFORM="x86_arm" - $env:BUILD="i686-pc-cygwin" - $env:HOST="arm-w32-cygwin" - $env:MSVCC="/cygdrive/c/projects/lean/libffi-%LIBFFI_V%/msvcc.sh -marm" - $env:SRC_ARCHITECTURE="arm" - } Else { - $env:VCVARS_PLATFORM="amd64" - $env:BUILD="x86_64-w64-cygwin" - $env:HOST="x86_64-w64-cygwin" - $env:MSVCC="/cygdrive/c/projects/lean/libffi-%LIBFFI_V%/msvcc.sh -m64" - $env:SRC_ARCHITECTURE="x86" - } - - 'appveyor DownloadFile https://cygwin.com/setup-x86.exe -FileName setup.exe' - - 'setup.exe -qnNdO -R "%CYG_ROOT%" -s "%CYG_MIRROR%" -l "%CYG_CACHE%" -P dejagnu >NUL' - - '%CYG_ROOT%/bin/bash -lc "cygcheck -dc cygwin"' - - echo call VsDevCmd to set VS150COMNTOOLS - - call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\Common7\Tools\VsDevCmd.bat" - - ps: $env:VSCOMNTOOLS=(Get-Content ("env:VS" + "$env:VSVER" + "0COMNTOOLS")) - - echo "Using Visual Studio %VSVER%.0 at %VSCOMNTOOLS%" - - call "%VSCOMNTOOLS%..\..\vc\Auxiliary\Build\vcvarsall.bat" %VCVARS_PLATFORM% + - 'nuget install libffi' + - pwd + - ls + - ls libffi.3.2.1.1/build/native + - ls libffi.3.2.1.1/build/native/* + - ls libffi.3.2.1.1/build/native/*/*/ + - ls libffi.3.2.1.1/build/native/*/*/* # through cyg-get # - alias cyg-get="setup.exe -q -P" @@ -59,30 +37,32 @@ install: # - 'appveyor DownloadFile https://github.com/libffi/libffi/releases/download/v3.3-rc0/libffi-3.3-rc0.tar.gz -FileName libffi.tar.gz' # - 'appveyor DownloadFile ftp://sourceware.org/pub/libffi/libffi-%LIBFFI_V%.tar.gz -FileName libffi.tar.gz' # - 'Install-Package libffi -Version 3.2.1.1' - - 'nuget install libffi' - - curl -fsS -o libffi.tar.gz ftp://sourceware.org/pub/libffi/libffi-%LIBFFI_V%.tar.gz - # - pwd - # - c:\cygwin\bin\sh -lc 'pwd' - # - c:\cygwin\bin\sh -lc 'echo $OLDPWD' - - c:\cygwin\bin\sh -lc '(cd $OLDPWD; tar xvzf libffi-rc0.tar.gz)' - # - cd libffi-%LIBFFI_V% - # - ls - # # - sh ./configure --disable-docs CC='%MSVCC%' CXX='%MSVCC%' LD=link CPP="cl -nologo -EP" - # # - sh -lc 'make' - # # - sh -lc 'make install' - # # - c:\cygwin\bin\sh -lc "(cd $OLDPWD; ./configure CC='%MSVCC%' CXX='%MSVCC%' LD='link' CPP='cl -nologo -EP' CXXCPP='cl -nologo -EP' CPPFLAGS='-DFFI_BUILDING_DLL' AR='/cygdrive/c/projects/lean/libffi-%LIBFFI_V%/.travis/ar-lib lib' NM='dumpbin -symbols' STRIP=':' --build=$BUILD --host=$HOST;)" - - c:\cygwin\bin\sh -lc "(cd $OLDPWD; ./configure CC='%MSVCC%' CXX='%MSVCC%' LD='link' CPP='cl -nologo -EP' CXXCPP='cl -nologo -EP' AR='/cygdrive/c/projects/lean/libffi-%LIBFFI_V%/.travis/ar-lib lib' NM='dumpbin -symbols' STRIP=':' --build=$BUILD --host=$HOST;)" - - c:\cygwin\bin\sh -lc '(cd $OLDPWD; make;)' - - c:\cygwin\bin\sh -lc "(cd $OLDPWD; cp src/%SRC_ARCHITECTURE%/ffitarget.h include; make; find .;)" - # # - c:\cygwin\bin\sh -lc "(cd $OLDPWD; cp `find . -name 'libffi-?.dll'` $HOST/testsuite/; make check; cat `find ./ -name libffi.log`)" - - c:\cygwin\bin\sh -lc '(cd $OLDPWD; make install;)' +# - curl -fsS -o libffi.tar.gz ftp://sourceware.org/pub/libffi/libffi-%LIBFFI_V%.tar.gz +# # - pwd +# # - c:\cygwin\bin\sh -lc 'pwd' +# # - c:\cygwin\bin\sh -lc 'echo $OLDPWD' +# - c:\cygwin\bin\sh -lc '(cd $OLDPWD; tar xvzf libffi-rc0.tar.gz)' +# # - cd libffi-%LIBFFI_V% +# # - ls +# # # - sh ./configure --disable-docs CC='%MSVCC%' CXX='%MSVCC%' LD=link CPP="cl -nologo -EP" +# # # - sh -lc 'make' +# # # - sh -lc 'make install' +# # # - c:\cygwin\bin\sh -lc "(cd $OLDPWD; ./configure CC='%MSVCC%' CXX='%MSVCC%' LD='link' CPP='cl -nologo -EP' CXXCPP='cl -nologo -EP' CPPFLAGS='-DFFI_BUILDING_DLL' AR='/cygdrive/c/projects/lean/libffi-%LIBFFI_V%/.travis/ar-lib lib' NM='dumpbin -symbols' STRIP=':' --build=$BUILD --host=$HOST;)" +# - c:\cygwin\bin\sh -lc "(cd $OLDPWD; ./configure CC='%MSVCC%' CXX='%MSVCC%' LD='link' CPP='cl -nologo -EP' CXXCPP='cl -nologo -EP' AR='/cygdrive/c/projects/lean/libffi-%LIBFFI_V%/.travis/ar-lib lib' NM='dumpbin -symbols' STRIP=':' --build=$BUILD --host=$HOST;)" +# - c:\cygwin\bin\sh -lc '(cd $OLDPWD; make;)' +# - c:\cygwin\bin\sh -lc "(cd $OLDPWD; cp src/%SRC_ARCHITECTURE%/ffitarget.h include; make; find .;)" +# # # - c:\cygwin\bin\sh -lc "(cd $OLDPWD; cp `find . -name 'libffi-?.dll'` $HOST/testsuite/; make check; cat `find ./ -name libffi.log`)" +# - c:\cygwin\bin\sh -lc '(cd $OLDPWD; make install;)' build_script: - call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\VC\Auxiliary\Build\vcvars64.bat" - cd %APPVEYOR_BUILD_FOLDER% && mkdir build && cd build + - ls c:/projects/lean/libffi.3.2.1.1/build/native/include # disable slow LTO - if %CFG% == MSVC (cmake ../src -DCMAKE_BUILD_TYPE=Release + -DFFI_INCLUDE_DIR=c:/projects/lean/libffi.3.2.1.1/build/native/include + '-DFFI_LIBRARY_DIR=%APPVEYOR_BUILD_FOLDER%\libffi.3.2.1.1\build\native\lib' -DCMAKE_TOOLCHAIN_FILE=c:/tools/vcpkg/scripts/buildsystems/vcpkg.cmake -DLEAN_EXTRA_CXX_FLAGS=/GL- -DLEAN_EXTRA_LINKER_FLAGS_MSVC=/LTCG:OFF diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index abc50bc7b5..5cb4c8368b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -17,6 +17,7 @@ endif() set(LEAN_EXTRA_LINKER_FLAGS "" CACHE STRING "Additional flags used by the linker") set(LEAN_EXTRA_CXX_FLAGS "" CACHE STRING "Additional flags used by the C++ compiler") +set(FFI_INCLUDE_DIR "" CACHE STRING "Location of the libffi include files") if (NOT CMAKE_BUILD_TYPE) message(STATUS "No build type selected, default to Release") @@ -305,14 +306,16 @@ else() include_directories(${GMP_INCLUDE_DIR}) set(EXTRA_LIBS ${EXTRA_LIBS} ${GMP_LIBRARIES}) # libffi - find_path(FFI_INCLUDE_PATH ffi.h PATHS ${FFI_INCLUDE_DIR}) + message(STATUS "looking for libffi in ${FFI_INCLUDE_DIR}.") + find_path(FFI_INCLUDE_PATH ffi.h PATHS ${FFI_INCLUDE_DIR} ${LEAN_SOURCE_DIR}/../libffi.3.2.1.1/build/native/include) + message(STATUS "looking for libffi in ${FFI_INCLUDE_PATH}.") if( EXISTS "${FFI_INCLUDE_PATH}/ffi.h" ) set(FFI_HEADER ffi.h CACHE INTERNAL "") set(HAVE_FFI_H 1 CACHE INTERNAL "") else() - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D USE_FFI_FFI_H") find_path(FFI_INCLUDE_PATH ffi/ffi.h PATHS ${FFI_INCLUDE_DIR}) if( EXISTS "${FFI_INCLUDE_PATH}/ffi/ffi.h" ) + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D USE_FFI_FFI_H") set(FFI_HEADER ffi/ffi.h CACHE INTERNAL "") set(HAVE_FFI_FFI_H 1 CACHE INTERNAL "") endif() diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 032e47601e..0e62cc4cd2 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -8,10 +8,10 @@ Author: Leonardo de Moura #include #include #include -#ifdef __linux__ - #include -#else +#ifdef USE_FFI_FFI_H #include +#else + #include #endif #include #include diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index c3bfc5e9f7..87b67fbc7b 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -10,10 +10,10 @@ Author: Leonardo de Moura #include #include #include -#ifdef __linux__ -#include +#ifdef USE_FFI_FFI_H + #include #else -#include + #include #endif #include "util/debug.h" #include "util/compiler_hints.h" diff --git a/src/library/vm/vm_ffi.cpp b/src/library/vm/vm_ffi.cpp index 5da3692512..83f387287c 100644 --- a/src/library/vm/vm_ffi.cpp +++ b/src/library/vm/vm_ffi.cpp @@ -6,10 +6,10 @@ Author: James King , Simon Hudon */ #include -#ifdef __linux__ - #include -#else +#ifdef USE_FFI_FFI_H #include +#else + #include #endif #include From a40aeb9ed00fe3013ca8284e4c8772e3dede81c4 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Tue, 21 May 2019 12:41:36 -0400 Subject: [PATCH 33/36] use vcpkg [skip travis] --- .appveyor.yml | 35 +++++++---------------------------- 1 file changed, 7 insertions(+), 28 deletions(-) diff --git a/.appveyor.yml b/.appveyor.yml index 1340c6efea..01819134d8 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -18,6 +18,13 @@ install: # upgrade git for vcpkg: https://github.com/appveyor/ci/issues/2097 - if %CFG% == MSVC (choco upgrade git -y & vcpkg install mpir:x64-windows) + - cd .. + - git clone https://github.com/Microsoft/vcpkg + - cd vcpkg + - .\bootstrap-vcpkg.bat + - vcpkg.exe install dlfcn-win32 + - cd %APPVEYOR_BUILD_FOLDER% + - 'nuget install libffi' - pwd - ls @@ -26,34 +33,6 @@ install: - ls libffi.3.2.1.1/build/native/*/*/ - ls libffi.3.2.1.1/build/native/*/*/* - # through cyg-get - # - alias cyg-get="setup.exe -q -P" - # - pip install paramiko --force-reinstall - # - choco install libffi-dev - # - setup.exe -q -P cygwin32-gcc-g++ - # - gcc-core gcc-g++ git libffi-devel nano openssl openssl-devel python-crypto python2 python2-devel python2-openssl python2-pip python2-setuptools tree - - # # install libffi - # - 'appveyor DownloadFile https://github.com/libffi/libffi/releases/download/v3.3-rc0/libffi-3.3-rc0.tar.gz -FileName libffi.tar.gz' - # - 'appveyor DownloadFile ftp://sourceware.org/pub/libffi/libffi-%LIBFFI_V%.tar.gz -FileName libffi.tar.gz' - # - 'Install-Package libffi -Version 3.2.1.1' -# - curl -fsS -o libffi.tar.gz ftp://sourceware.org/pub/libffi/libffi-%LIBFFI_V%.tar.gz -# # - pwd -# # - c:\cygwin\bin\sh -lc 'pwd' -# # - c:\cygwin\bin\sh -lc 'echo $OLDPWD' -# - c:\cygwin\bin\sh -lc '(cd $OLDPWD; tar xvzf libffi-rc0.tar.gz)' -# # - cd libffi-%LIBFFI_V% -# # - ls -# # # - sh ./configure --disable-docs CC='%MSVCC%' CXX='%MSVCC%' LD=link CPP="cl -nologo -EP" -# # # - sh -lc 'make' -# # # - sh -lc 'make install' -# # # - c:\cygwin\bin\sh -lc "(cd $OLDPWD; ./configure CC='%MSVCC%' CXX='%MSVCC%' LD='link' CPP='cl -nologo -EP' CXXCPP='cl -nologo -EP' CPPFLAGS='-DFFI_BUILDING_DLL' AR='/cygdrive/c/projects/lean/libffi-%LIBFFI_V%/.travis/ar-lib lib' NM='dumpbin -symbols' STRIP=':' --build=$BUILD --host=$HOST;)" -# - c:\cygwin\bin\sh -lc "(cd $OLDPWD; ./configure CC='%MSVCC%' CXX='%MSVCC%' LD='link' CPP='cl -nologo -EP' CXXCPP='cl -nologo -EP' AR='/cygdrive/c/projects/lean/libffi-%LIBFFI_V%/.travis/ar-lib lib' NM='dumpbin -symbols' STRIP=':' --build=$BUILD --host=$HOST;)" -# - c:\cygwin\bin\sh -lc '(cd $OLDPWD; make;)' -# - c:\cygwin\bin\sh -lc "(cd $OLDPWD; cp src/%SRC_ARCHITECTURE%/ffitarget.h include; make; find .;)" -# # # - c:\cygwin\bin\sh -lc "(cd $OLDPWD; cp `find . -name 'libffi-?.dll'` $HOST/testsuite/; make check; cat `find ./ -name libffi.log`)" -# - c:\cygwin\bin\sh -lc '(cd $OLDPWD; make install;)' - build_script: - call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\VC\Auxiliary\Build\vcvars64.bat" - cd %APPVEYOR_BUILD_FOLDER% && mkdir build && cd build From d2cc6e00b62fb9cd8642b6befd9746e1ecd0675a Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Tue, 21 May 2019 12:54:25 -0400 Subject: [PATCH 34/36] address warnings --- src/frontends/lean/calc.cpp | 2 +- src/frontends/lean/parser.cpp | 4 ++-- src/frontends/lean/pp.cpp | 4 ++-- src/frontends/lean/print_cmd.cpp | 2 +- src/frontends/lean/tactic_notation.cpp | 2 +- src/library/library_task_builder.cpp | 2 +- src/library/module_mgr.cpp | 6 +++--- src/shell/server.cpp | 4 ++-- 8 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp index 0b5e9af49a..da84a1ce1a 100644 --- a/src/frontends/lean/calc.cpp +++ b/src/frontends/lean/calc.cpp @@ -154,7 +154,7 @@ expr parse_calc(parser & p) { new_pred = calc_pred(pred_op(new_pred), pred_rhs(pred), pred_rhs(new_pred)); calc_step new_step = parse_calc_proof(p, new_pred); step = join(p, step, new_step, pos); - } catch (parser_error ex) { + } catch (parser_error & ex) { p.maybe_throw_error(std::move(ex)); } } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 1c7035faf6..44d8c42c70 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -2092,7 +2092,7 @@ name parser::check_constant_next(char const * msg) { name id = check_id_next(msg); try { return to_constant(id, msg, p); - } catch (parser_error e) { + } catch (parser_error & e) { maybe_throw_error(std::move(e)); return id; } @@ -2466,7 +2466,7 @@ void parser::process_imports() { auto begin_pos = pos(); try { parse_imports(fingerprint, imports); - } catch (parser_exception) { + } catch (parser_exception &) { exception_during_scanning = std::current_exception(); } diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 0aac2ecde5..0eceff0cd6 100755 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -1783,7 +1783,7 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result { if (!m_proofs && !is_constant(e) && !is_mlocal(e) && closed(e) && is_prop(m_ctx.infer(e))) { return result(format("_")); } - } catch (exception) {} + } catch (exception &) {} if (auto r = pp_notation(e)) return *r; @@ -1911,7 +1911,7 @@ format pretty_fn::operator()(expr const & e) { if (!m_options.contains(get_pp_proofs_name()) && !get_pp_all(m_options)) { try { m_proofs = !closed(purified) || is_prop(m_ctx.infer(purified)); - } catch (exception) { + } catch (exception &) { m_proofs = true; } } diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index ddabc4e21e..a60dcd933a 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -349,7 +349,7 @@ void print_id_info(parser & p, message_builder & out, name const & id, bool show try { cs = p.to_constants(id, "", pos); found = true; - } catch (parser_error) {} + } catch (parser_error &) {} bool first = true; for (name const & c : cs) { if (first) first = false; else out << "\n"; diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp index c713f61862..59f049a40a 100644 --- a/src/frontends/lean/tactic_notation.cpp +++ b/src/frontends/lean/tactic_notation.cpp @@ -193,7 +193,7 @@ static expr parse_interactive_tactic(parser & p, name const & decl_name, name co args.push_back(p.parse_expr(get_max_prec())); } p.check_break_before(); - } catch (break_at_pos_exception) { + } catch (break_at_pos_exception &) { throw; } catch (...) { p.check_break_before(); diff --git a/src/library/library_task_builder.cpp b/src/library/library_task_builder.cpp index f6f4fac03a..9d57c3cfa7 100644 --- a/src/library/library_task_builder.cpp +++ b/src/library/library_task_builder.cpp @@ -25,7 +25,7 @@ struct library_scopes_imp : public delegating_task_imp { if (m_lt) m_lt.set_state(log_tree::state::Running); try { delegating_task_imp::execute(result); - } catch (interrupted) { + } catch (interrupted &) { if (m_lt) m_lt.set_state(log_tree::state::Cancelled); throw; } diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp index cd8d88ec6a..cf3b1e7fd3 100644 --- a/src/library/module_mgr.cpp +++ b/src/library/module_mgr.cpp @@ -86,7 +86,7 @@ static module_loader mk_loader(module_id const & cur_mod, std::vectorm_result).m_loaded_module; } } - } catch (std::out_of_range) { + } catch (std::out_of_range &) { // In files with syntax errors, it can happen that the // initial dependency scan does not find all dependencies. } @@ -132,7 +132,7 @@ static module_id resolve(search_path const & path, auto base_dir = dirname(module_file_name); try { return find_file(path, base_dir, ref.m_relative, ref.m_name, ".lean"); - } catch (lean_file_not_found_exception) { + } catch (lean_file_not_found_exception &) { return olean_file_to_lean_file(find_file(path, base_dir, ref.m_relative, ref.m_name, ".olean")); } } @@ -454,7 +454,7 @@ std::shared_ptr fs_module_vfs::load_module(module_id const & id, bo is_candidate_olean_file(olean_fn)) { return std::make_shared(id, read_file(olean_fn, std::ios_base::binary), module_src::OLEAN, olean_mtime); } - } catch (exception) {} + } catch (exception &) {} return std::make_shared(id, read_file(lean_fn), module_src::LEAN, lean_mtime); } diff --git a/src/shell/server.cpp b/src/shell/server.cpp index f350f1db53..f533c71cea 100644 --- a/src/shell/server.cpp +++ b/src/shell/server.cpp @@ -421,7 +421,7 @@ void server::handle_request(json const & jreq) { handle_request(req); } catch (std::exception & ex) { send_msg(cmd_res(req.m_seq_num, std::string(ex.what()))); - } catch (interrupted) { + } catch (interrupted &) { send_msg(cmd_res(req.m_seq_num, std::string("interrupted"))); } catch (...) { send_msg(cmd_res(req.m_seq_num, std::string("unknown exception"))); @@ -468,7 +468,7 @@ void server::handle_async_response(server::cmd_req const & req, task co send_msg(msg); } catch (throwable & ex) { send_msg(cmd_res(req.m_seq_num, std::string(ex.what()))); - } catch (interrupted) { + } catch (interrupted &) { send_msg(cmd_res(req.m_seq_num, std::string("interrupted"))); } catch (...) { send_msg(cmd_res(req.m_seq_num, std::string("unknown exception"))); From 718d132f99fa0545d6f033fda5642c6c78c70980 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Tue, 21 May 2019 13:56:04 -0400 Subject: [PATCH 35/36] look for `dlfcn.h` in cmake files [skip travis] --- .appveyor.yml | 26 ++++++++++++++++++++------ src/CMakeLists.txt | 22 ++++++++++++++++++++++ 2 files changed, 42 insertions(+), 6 deletions(-) diff --git a/.appveyor.yml b/.appveyor.yml index 01819134d8..e740f7fe1c 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -7,6 +7,7 @@ environment: CYG_MIRROR: http://mirrors.kernel.org/sourceware/cygwin/ VSVER: 15 LIBFFI_V: 3.2 + dlfcn-win32_DIR: C:\projects\vcpkg\installed\x86-windows matrix: - CFG: MINGW64 UPLOAD: ON @@ -23,15 +24,28 @@ install: - cd vcpkg - .\bootstrap-vcpkg.bat - vcpkg.exe install dlfcn-win32 + - ls C:\projects\vcpkg\downloads + - ls C:\projects\vcpkg\installed\x86-windows + - ls C:\projects\vcpkg\installed\vcpkg + - ls C:\projects\vcpkg\installed + + - ls C:\projects\vcpkg\installed\* || true + - ls C:\projects\vcpkg\downloads\tools || true + - ls C:\projects\vcpkg\downloads\*\* || true + # - ls C:\projects\vcpkg\downloads\*\*\* + - ls %HOME% + - ls %HOME%\installed || true + - ls %HOME%\packages || true + - ls %HOME%\ports || true - cd %APPVEYOR_BUILD_FOLDER% - 'nuget install libffi' - - pwd - - ls - - ls libffi.3.2.1.1/build/native - - ls libffi.3.2.1.1/build/native/* - - ls libffi.3.2.1.1/build/native/*/*/ - - ls libffi.3.2.1.1/build/native/*/*/* + # - pwd + # - ls + # - ls libffi.3.2.1.1/build/native + # - ls libffi.3.2.1.1/build/native/* + # - ls libffi.3.2.1.1/build/native/*/*/ + # - ls libffi.3.2.1.1/build/native/*/*/* build_script: - call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\VC\Auxiliary\Build\vcvars64.bat" diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5cb4c8368b..1ed7cebabd 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -337,6 +337,28 @@ else() list(REMOVE_ITEM CMAKE_REQUIRED_LIBRARIES ${FFI_LIBRARY_PATH}) set(EXTRA_LIBS ${EXTRA_LIBS} ${FFI_LIBRARY_PATH}) include_directories(${FFI_INCLUDE_PATH}) + + # dlfcn.h + if (WIN32) + find_path(DLFCN_INCLUDE_PATH dlfcn.h PATHS C:/projects/vcpkg/installed) + find_package(dlfcn-win32 REQUIRED PATHS C:/projects/vcpkg/installed) + if( NOT DLFCN_INCLUDE_PATH ) + message(FATAL_ERROR "dlfcn.h is not found.") + endif() + set(EXTRA_LIBS ${EXTRA_LIBS} dlfcn-win32::dl) + include_directories(${DLFCN_INCLUDE_PATH}) + endif () + # find_path(DLFCN_INCLUDE_PATH dlfcn.h PATHS ${DLFCN_INCLUDE_DIR}) + # if( NOT (EXISTS "${DLFCN_INCLUDE_PATH}/dlfcn.h") ) + # message(FATAL_ERROR "dlfcn.h not found.") + # endif() + # find_library(DLFCN_LIBRARY_PATH dlfcn PATHS ${DLFCN_LIBRARY_DIR}) + # if( NOT DLFCN_LIBRARY_PATH ) + # message(FATAL_ERROR "dlfcn library is not found.") + # endif() + # set(EXTRA_LIBS ${EXTRA_LIBS} ${DLFCN_LIBRARY_PATH}) + # include_directories(${DLFCN_INCLUDE_PATH}) + endif() # DL From c409a4fd7676267cec377b452406af20497ab3bb Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Thu, 23 May 2019 16:48:54 -0400 Subject: [PATCH 36/36] add dlfcn-win32 as a submodule [skip travis] --- .appveyor.yml | 1 + .gitmodules | 3 +++ src/CMakeLists.txt | 21 ++++++++++++++------- src/library/vm/vm_ffi.cpp | 4 ++++ thirdparty/dlfcn-win32 | 1 + 5 files changed, 23 insertions(+), 7 deletions(-) create mode 100644 .gitmodules create mode 160000 thirdparty/dlfcn-win32 diff --git a/.appveyor.yml b/.appveyor.yml index e740f7fe1c..5657717bf6 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -48,6 +48,7 @@ install: # - ls libffi.3.2.1.1/build/native/*/*/* build_script: + - git submodule update --init --recursive - call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\VC\Auxiliary\Build\vcvars64.bat" - cd %APPVEYOR_BUILD_FOLDER% && mkdir build && cd build - ls c:/projects/lean/libffi.3.2.1.1/build/native/include diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000000..1de738da6c --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "thirdparty/dlfcn-win32"] + path = thirdparty/dlfcn-win32 + url = https://github.com/dlfcn-win32/dlfcn-win32 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1ed7cebabd..2019a116fb 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -340,13 +340,20 @@ else() # dlfcn.h if (WIN32) - find_path(DLFCN_INCLUDE_PATH dlfcn.h PATHS C:/projects/vcpkg/installed) - find_package(dlfcn-win32 REQUIRED PATHS C:/projects/vcpkg/installed) - if( NOT DLFCN_INCLUDE_PATH ) - message(FATAL_ERROR "dlfcn.h is not found.") - endif() - set(EXTRA_LIBS ${EXTRA_LIBS} dlfcn-win32::dl) - include_directories(${DLFCN_INCLUDE_PATH}) + # find_path(DLFCN_INCLUDE_PATH dlfcn.h PATHS C:/projects/vcpkg/installed) + # find_package(dlfcn-win32 REQUIRED PATHS C:/projects/vcpkg/installed) + # if( NOT DLFCN_INCLUDE_PATH ) + # message(FATAL_ERROR "dlfcn.h is not found.") + # endif() + # set(EXTRA_LIBS ${EXTRA_LIBS} dlfcn-win32::dl) + set(WIN32_DIR ${LEAN_SOURCE_DIR}/../thirdparty/dlfcn-win32) + include_directories(${WIN32_DIR}) + set(WIN32_SOURCE ${WIN32_DIR}/dlfcn.c) + add_custom_command( + OUTPUT ${WIN32_SOURCE} ${WIN32_DIR}/dlfcn.h + COMMAND git submodule init) + add_library(win32 OBJECT ${WIN32_SOURCE}) + set(LEAN_OBJS ${LEAN_OBJS} $) endif () # find_path(DLFCN_INCLUDE_PATH dlfcn.h PATHS ${DLFCN_INCLUDE_DIR}) # if( NOT (EXISTS "${DLFCN_INCLUDE_PATH}/dlfcn.h") ) diff --git a/src/library/vm/vm_ffi.cpp b/src/library/vm/vm_ffi.cpp index 83f387287c..a423f82e5f 100644 --- a/src/library/vm/vm_ffi.cpp +++ b/src/library/vm/vm_ffi.cpp @@ -5,7 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: James King , Simon Hudon */ +#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN) +#include +#else #include +#endif #ifdef USE_FFI_FFI_H #include #else diff --git a/thirdparty/dlfcn-win32 b/thirdparty/dlfcn-win32 new file mode 160000 index 0000000000..1488731c81 --- /dev/null +++ b/thirdparty/dlfcn-win32 @@ -0,0 +1 @@ +Subproject commit 1488731c810ed76589170909da9ef07f060cef46