max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: pass --trust to frontend

Browse source
This commit is contained in:
tydeu 2021-11-08 21:48:33 -05:00 • committed by Sebastian Ullrich
parent 6e4fcaaea9
commit f0fd17138c
2 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/Frontend.lean
View file

@ -94,10 +94,10 @@ def getPrintMessageEndPos (opts : Options) : Bool :=
opts.getBool `printMessageEndPos false
@[export lean_run_frontend]
def runFrontend (input : String) (opts : Options) (fileName : String) (mainModuleName : Name) : IO (Environment × Bool) := do
def runFrontend (input : String) (opts : Options) (fileName : String) (mainModuleName : Name) (trustLevel : UInt32 := 0) : IO (Environment × Bool) := do
let inputCtx := Parser.mkInputContext input fileName
let (header, parserState, messages) ← Parser.parseHeader inputCtx
let (env, messages) ← processHeader header opts messages inputCtx
let (env, messages) ← processHeader header opts messages inputCtx trustLevel
let env := env.setMainModule mainModuleName
let s ← IO.processCommands inputCtx parserState (Command.mkState env messages opts)
for msg in s.commandState.messages.toList do

8
src/util/shell.cpp
View file

@ -336,10 +336,10 @@ void load_library(std::string path) {
}
namespace lean {
extern "C" object * lean_run_frontend(object * input, object * opts, object * filename, object * main_module_name, object * w);
pair_ref<environment, object_ref> run_new_frontend(std::string const & input, options const & opts, std::string const & file_name, name const & main_module_name) {
extern "C" object * lean_run_frontend(object * input, object * opts, object * filename, object * main_module_name, uint32_t trust_level, object * w);
pair_ref<environment, object_ref> run_new_frontend(std::string const & input, options const & opts, std::string const & file_name, name const & main_module_name, uint32_t trust_level) {
return get_io_result<pair_ref<environment, object_ref>>(
lean_run_frontend(mk_string(input), opts.to_obj_arg(), mk_string(file_name), main_module_name.to_obj_arg(), io_mk_world()));
lean_run_frontend(mk_string(input), opts.to_obj_arg(), mk_string(file_name), main_module_name.to_obj_arg(), trust_level, io_mk_world()));
}
/* def workerMain : Options → IO UInt32 */
@ -647,7 +647,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
if (!main_module_name)
main_module_name = name("_stdin");
pair_ref<environment, object_ref> r = run_new_frontend(contents, opts, mod_fn, *main_module_name);
pair_ref<environment, object_ref> r = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl);
env = r.fst();
bool ok = unbox(r.snd().raw());