Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Plugin Support #59

Closed
wants to merge 6 commits into from
Closed

Plugin Support #59

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
3a05f1a
fix: leanc: use cc when compiling a .c file
Kha Nov 7, 2019
47c8184
chore: remove outdated macOS cmake setup
Kha Nov 7, 2019
7e95669
feat: add --plugin for loading shared libraries
Kha Nov 9, 2019
6641d10
feat: simplistic linter framework
Kha Nov 9, 2019
083fb9a
feat: call linters on non-mutual definitions
Kha Nov 9, 2019
0865fd2
test: trivial linter test
Kha Nov 6, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 7 additions & 5 deletions bin/leanc.in
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,13 @@ bindir=$(dirname $0)
# Final linking still has to be done by a C++ compiler because we need to link against the
# Lean runtime written in C++ (https://isocpp.org/wiki/faq/mixing-c-and-cpp#overview-mixing-langs).
use_c=maybe
# NOTE: leanstatic and leanstdlib are cyclically dependent
linker_flags="-lleanstatic -lleanstdlib -lleanstatic -lleanstdlib"
for arg in "$@"; do
[[ $use_c == maybe && $arg == "-c" ]] && use_c=yes
[[ $arg == "*.cpp" ]] && use_c=no
[[ $arg == *.c ]] && use_c=yes
[[ $arg == *.cpp ]] && use_c=no
[[ $arg == "-shared" ]] && linker_flags="@LEANC_SHARED_LINKER_FLAGS@"
done

if [[ $use_c == yes ]]; then
Expand All @@ -30,8 +34,7 @@ if [[ $use_c == yes ]]; then
done
[ -f $LEAN_CC ] || command -v $LEAN_CC || error "no suitable C compiler found!"

# NOTE: leanstatic and leanstdlib are cyclically dependent
$LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
$LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
else
# Check C++ compiler
for cxx in $LEAN_CXX @CMAKE_CXX_COMPILER@ /usr/bin/g++; do
Expand All @@ -41,6 +44,5 @@ else
done
[ -f $LEAN_CXX ] || command -v $LEAN_CXX || error "no suitable C++ compiler found!"

# NOTE: leanstatic and leanstdlib are cyclically dependent
$LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
$LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
fi
1 change: 1 addition & 0 deletions library/Init/Lean/Default.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,3 +21,4 @@ import Init.Lean.MetavarContext
import Init.Lean.TypeClass
import Init.Lean.Trace
import Init.Lean.AuxRecursor
import Init.Lean.Linter
28 changes: 28 additions & 0 deletions library/Init/Lean/Linter.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
prelude
import Init.System.IO
import Init.Lean.Attributes
import Init.Lean.Message
import Init.Lean.Syntax

namespace Lean

def Linter := Environment → Name → /-Syntax → -/IO MessageLog

def mkLintersRef : IO (IO.Ref (Array Linter)) :=
IO.mkRef #[]

/- Linters should be loadable as plugins, so store in a global IO ref instead of an attribute managed by the
environment (which only contains `import`ed objects). -/
@[init mkLintersRef, export lean_linters_ref]
constant lintersRef : IO.Ref (Array Linter) := arbitrary _

def addLinter (l : Linter) : IO Unit := do
ls ← lintersRef.get;
lintersRef.set (ls.push l)

end Lean
23 changes: 13 additions & 10 deletions src/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -285,13 +285,6 @@ set(CPACK_BUNDLE_NAME "Lean-${LEAN_VERSION_STRING}")
set(CPACK_PACKAGE_ICON "${LEAN_SOURCE_DIR}/../images/lean.png")
##################

# Set a consistent MACOSX_RPATH default across all CMake versions.
# When CMake 2.8.12 is required, change this default to 1.
# When CMake 3.0.0 is required, remove this block (see CMP0042).
if (NOT DEFINED CMAKE_MACOSX_RPATH)
set(CMAKE_MACOSX_RPATH 0)
endif()

if (${CMAKE_SYSTEM_NAME} MATCHES "Linux")
# The following options is needed to generate a shared library
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fPIC")
Expand Down Expand Up @@ -434,18 +427,28 @@ include_directories(${LEAN_SOURCE_DIR})
# export all symbols for the interpreter
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS} -Wl,--export-all")
set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -Wl,--export-all")
set(LEANC_SHARED_LINKER_FLAGS "${LEANC_SHARED_LINKER_FLAGS} -Wl,--export-all")
else()
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS} -rdynamic")
set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -ldl")
endif()

# Allow `lean` symbols in plugins without linking directly against it. If we linked against the
# executable or `leanshared`, plugins would try to look them up at load time (even though they
# are already loaded) and probably fail unless we set up LD_LIBRARY_PATH.
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
# import library created by the `lean` target (and copied by `bin_lean`)
set(LEANC_SHARED_LINKER_FLAGS "$bindir/liblean.dll.a")
elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
set(LEANC_SHARED_LINKER_FLAGS "${LEANC_EXTRA_FLAGS} -Wl,-undefined,dynamic_lookup")
endif()
# Linux ignores undefined symbols in shared libraries by default

if(MULTI_THREAD AND NOT MSVC AND (NOT ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")))
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread")
endif()
set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage")
if ((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -Wl,--export-all")
endif()

# Git HASH
set(LEAN_PACKAGE_VERSION "NOT-FOUND")
Expand Down
15 changes: 15 additions & 0 deletions src/frontends/lean/definition_cmds.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,9 @@ Author: Leonardo de Moura
#include "frontends/lean/decl_attributes.h"
#include "frontends/lean/definition_cmds.h"
#include "frontends/lean/typed_expr.h"
#include "library/compiler/ir_interpreter.h"
#include "util/array_ref.h"
#include "util/io.h"

namespace lean {
environment ensure_decl_namespaces(environment const & env, name const & full_n) {
Expand Down Expand Up @@ -495,6 +498,8 @@ static bool is_rfl_preexpr(expr const & e) {
return is_constant(e, get_rfl_name());
}

extern "C" object * lean_linters_ref;

static environment elab_single_def(parser & p, decl_cmd_kind const & kind, cmd_meta meta, buffer <name> lp_names,
buffer <expr> params, expr fn, expr val, pos_info const & header_pos,
name const & prv_name) {
Expand Down Expand Up @@ -580,6 +585,16 @@ static environment elab_single_def(parser & p, decl_cmd_kind const & kind, cmd_m
new_env = compile_decl(p, new_env, c_name, c_real_name, header_pos);
}
new_env = meta.m_attrs.apply_after_comp(new_env, c_real_name);

// temporary code that should soon be removed together with the whole C++ frontend
object_ref r(io_ref_get(lean_linters_ref, io_mk_world()));
lean_assert(io_result_is_ok(r.raw()));
array_ref<object *> linters(io_result_get_value(r.raw()), true);
for (object * const & linter : linters) {
object * r2 = apply_3(linter, new_env.to_obj_arg(), local_name_p(fn).to_obj_arg(), io_mk_world());
consume_io_result(r2);
}

return new_env;
};

Expand Down
17 changes: 16 additions & 1 deletion src/shell/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,12 @@ add_custom_target(update-stage0

add_executable(lean lean.cpp)
target_link_libraries(lean leanstatic)
# create import library on Windows to link plugins against
set_target_properties(lean PROPERTIES ENABLE_EXPORTS ON)
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
# https://github.com/msys2/MINGW-packages/issues/5952
target_link_options(lean PRIVATE "-Wl,--out-implib,$<TARGET_LINKER_FILE:lean>")
endif()
install(TARGETS lean DESTINATION bin)

if(${EMSCRIPTEN})
Expand Down Expand Up @@ -76,7 +82,7 @@ else()
)
else()
ADD_CUSTOM_TARGET(bin_lean ALL
COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean>" "${LEAN_SOURCE_DIR}/../bin/"
COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean>" "$<TARGET_LINKER_FILE:lean>" "${LEAN_SOURCE_DIR}/../bin/"
DEPENDS bin_lean_stage0 lean
)
endif()
Expand Down Expand Up @@ -198,6 +204,15 @@ FOREACH(T_OUT ${LEANBENCHTESTS})
COMMAND bash "./test_single.sh" ${T_NAME})
ENDFOREACH(T_OUT)

# LEAN PLUGIN TESTS
file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/plugin/*.lean")
FOREACH(T ${LEANINTERPTESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leanplugintest_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/plugin"
COMMAND bash "./test_single.sh" ${T_NAME})
ENDFOREACH(T)

# LEANPKG TESTS
# file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/lean/leanpkg/*.sh")
# FOREACH(T ${LEANPKGTESTS})
Expand Down
44 changes: 43 additions & 1 deletion src/shell/lean.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,13 @@ Author: Leonardo de Moura
#endif
#include "githash.h" // NOLINT

#ifdef LEAN_WINDOWS
#include <windows.h>
#undef ERROR // thanks, wingdi.h
#else
#include <dlfcn.h>
#endif

#if defined(LEAN_LLVM)
#include <llvm/Support/TargetSelect.h>
#endif
Expand Down Expand Up @@ -201,6 +208,7 @@ static void display_help(std::ostream & out) {
std::cout << " --threads=num -j number of threads used to process lean files\n";
std::cout << " --tstack=num -s thread stack size in Kb\n";
#endif
std::cout << " --plugin=file load and initialize shared library for registering linters etc.";
std::cout << " --deps just print dependencies of a Lean input\n";
#if defined(LEAN_JSON)
std::cout << " --json print JSON-formatted structured error messages\n";
Expand Down Expand Up @@ -241,14 +249,15 @@ static struct option g_long_options[] = {
#if defined(LEAN_MULTI_THREAD)
{"tstack", required_argument, 0, 's'},
#endif
{"plugin", required_argument, 0, 'p'},
#ifdef LEAN_DEBUG
{"debug", required_argument, 0, 'B'},
#endif
{0, 0, 0, 0}
};

static char const * g_opt_str =
"PdD:c:C:qgvht:012j:012rM:012T:012a"
"PdD:c:C:qgvht:012j:012rM:012T:012ap:"
#if defined(LEAN_MULTI_THREAD)
"s:012"
#endif
Expand Down Expand Up @@ -289,6 +298,32 @@ options set_config_option(options const & opts, char const * in) {
}
}

void load_plugin(std::string path) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should move this function to a different folder since we need it to implement the import plugin <plugin-name> command

void * init;
// we never want to look up plugins using the system library search
path = lrealpath(path);
#ifdef LEAN_WINDOWS
HMODULE h = LoadLibrary(path.c_str());
if (!h) {
throw exception(sstream() << "error loading plugin " << path);
}
init = reinterpret_cast<void *>(GetProcAddress(h, "initialize_Default"));
#else
void *handle = dlopen(path.c_str(), RTLD_LAZY);
if (!handle) {
throw exception(sstream() << "error loading plugin, " << dlerror());
}
init = dlsym(handle, "initialize_Default");
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems every plugin must define initialize_Default. Is this a problem?
https://stackoverflow.com/questions/6538501/linking-two-shared-libraries-with-some-of-the-same-symbols
I am assuming it should work since you are using dlsym.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, objects loaded by dlsym are independent by default.

      RTLD_LOCAL
              This is the converse of RTLD_GLOBAL, and the default if neither flag is specified.  Symbols  defined  in  this
              shared object are not made available to resolve references in subsequently loaded shared objects.

As far as I could find out, this is actually the only behavior supported on Windows, so we should be fine.

Btw, note that if we ever do prefix import paths with the package name as we once discussed, this would be initialize_SnakeLinter_Default anyway (which --plugin should derive from the library filename).

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this try calling dlopen with RTLD_NOLOAD (if available) first, to check if the shared library is actually loaded already,
to avoid opening the same library twice?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the same shared object is opened again with dlopen(), the same object handle is returned. And Lean initializers are idempotent.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks I had missed the section describing that in the docs, needed to read further.

#endif
if (!init) {
throw exception(sstream() << "error, plugin " << path << " does not seem to contain a module 'Default'");
}
auto init_fn = reinterpret_cast<object *(*)(object *)>(init);
object *r = init_fn(io_mk_world());
consume_io_result(r);
// NOTE: we never unload plugins
}

class initializer {
private:
lean::initializer m_init;
Expand Down Expand Up @@ -344,6 +379,10 @@ int main(int argc, char ** argv) {
} catch (e) {
console.log(e);
});
#endif
#if LEAN_WINDOWS
// "best practice" according to https://docs.microsoft.com/en-us/windows/win32/api/errhandlingapi/nf-errhandlingapi-seterrormode
SetErrorMode(SEM_FAILCRITICALERRORS);
#endif
auto init_start = std::chrono::steady_clock::now();
::initializer init;
Expand Down Expand Up @@ -454,6 +493,9 @@ int main(int argc, char ** argv) {
case 'n':
new_frontend = true;
break;
case 'p':
load_plugin(optarg);
break;
default:
std::cerr << "Unknown command line option\n";
display_help(std::cerr);
Expand Down
Loading