chore(*): fix compiler warnings (#148)

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));
         }
     }

src/frontends/lean/interactive.cpp

@@ -135,7 +135,7 @@ void report_info(environment const & env, options const & opts, io_state const &
                     record["source"]["file"] = f;
                     record["source"]["line"] = 1;
                     record["source"]["column"] = 0;
-                } catch (file_not_found_exception) {}
+                } catch (file_not_found_exception &) {}
                 break;
             }
             case break_at_pos_exception::token_context::option:

src/frontends/lean/local_decls.h

@@ -56,6 +56,13 @@ class local_decls {
         m_entries = new_entries;
     }
 
+    local_decls & operator=(local_decls const & d) {
+        m_map = d.m_map;
+        m_entries = d.m_entries;
+        m_counter = d.m_counter;
+        return *this;
+    }
+
     V const * find(name const & k) const { auto it = m_map.find(k); return it ? &(it->first) : nullptr; }
     unsigned find_idx(name const & k) const { auto it = m_map.find(k); return it ? it->second : 0; }
     bool contains(name const & k) const { return m_map.contains(k); }

src/frontends/lean/local_level_decls.h

@@ -15,7 +15,6 @@ class local_level_decls {
     unsigned           m_counter;
 public:
     local_level_decls():m_counter(1) {}
-    local_level_decls(local_level_decls const & d):m_decls(d.m_decls), m_idxs(d.m_idxs), m_counter(d.m_counter) {}
     void insert(name const & k, level const & v) {
         m_decls.insert(k, v);
         m_idxs.insert(k, m_counter);

src/frontends/lean/parser.cpp

@@ -2110,7 +2110,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;
     }
@@ -2484,7 +2484,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();
     }
 

src/frontends/lean/pp.cpp

@@ -1833,7 +1833,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;
@@ -1961,7 +1961,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;
         }
     }

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";

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();

src/library/inductive_compiler/util.cpp

@@ -86,7 +86,7 @@ void assert_def_eq(environment const & DEBUG_CODE(env), expr const & DEBUG_CODE(
     DEBUG_CODE(type_checker checker(env, true, false /* allow untrusted/meta */););
     try {
         lean_assert(checker.is_def_eq(e1, e2));
-    } catch (exception ex) {
+    } catch (exception & ex) {
         // TODO(dhs): this is only for debugging
         // We prefer to enter GDB than to throw an exception
         lean_assert(false);
@@ -98,7 +98,7 @@ void assert_type_correct(environment const & env, expr const & e) {
     type_checker checker(env, true, false /* allow untrusted/meta */);
     try {
         checker.check(e);
-    } catch (exception ex) {
+    } catch (exception & ex) {
         // TODO(dhs): this is only for debugging
         // We prefer to enter GDB than to throw an exception
         lean_assert(false);

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;
         }

src/library/module.cpp

@@ -432,7 +432,7 @@ struct mod_doc_modification : public modification {
     /** A module-level docstring. */
     mod_doc_modification(std::string const & doc, pos_info pos) : m_doc(doc), m_pos(pos) {}
 
-    void perform(environment & env) const override {
+    void perform(environment &) const override {
         // No-op. See `import_module` for actual action
     }
 
@@ -657,7 +657,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()});
     }
 }

src/library/module_mgr.cpp

@@ -87,7 +87,7 @@ module_loader mk_loader(module_id const & cur_mod, std::vector<module_info::depe
                     return get(d.m_mod_info->m_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.
         }
@@ -133,7 +133,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"));
     }
 }
@@ -457,7 +457,7 @@ std::shared_ptr<module_info> fs_module_vfs::load_module(module_id const & id, bo
             is_candidate_olean_file(olean_fname, src_hash)) {
             return std::make_shared<module_info>(id, read_file(olean_fname, std::ios_base::binary), src_hash, src_hash, module_src::OLEAN);
         }
-    } catch (exception) {}
+    } catch (exception &) {}
 
     return std::make_shared<module_info>(id, lean_src, src_hash, src_hash, module_src::LEAN);
 }

src/library/tactic/smt/theory_ac.h

@@ -46,7 +46,7 @@ class theory_ac {
     struct entry {
         /* m_expr is the term in the congruence closure
            module being represented by this entry */
-        unsigned    m_idx;
+        unsigned    m_idx = 0;
         occurrences m_R_occs[2];
         entry() {}
         entry(unsigned idx):m_idx(idx) {}

src/library/vm/vm.h

@@ -175,7 +175,7 @@ class ts_vm_obj {
 /** Builtin functions that take arguments from the system stack.
 
     \remark The C++ code generator produces this kind of function. */
-typedef vm_obj (*vm_cfunction)(vm_obj const &);
+using vm_cfunction = void *;
 typedef vm_obj (*vm_cfunction_0)();
 typedef vm_obj (*vm_cfunction_1)(vm_obj const &);
 typedef vm_obj (*vm_cfunction_2)(vm_obj const &, vm_obj const &);

src/library/vm/vm_io.cpp

@@ -216,7 +216,7 @@ static vm_obj fs_flush(vm_obj const & h, vm_obj const &) {
     try {
         href->flush();
         return mk_io_result(mk_vm_unit());
-    } catch (handle_exception e) {
+    } catch (handle_exception & e) {
         return mk_io_failure("flush failed");
     }
 }
@@ -238,7 +238,7 @@ static vm_obj fs_close(vm_obj const & h, vm_obj const &) {
     try {
         href->close();
         return mk_io_result(mk_vm_unit());
-    } catch (handle_exception e) {
+    } catch (handle_exception & e) {
         return mk_io_failure("close failed");
     }
 }
@@ -399,7 +399,7 @@ static vm_obj fs_write(vm_obj const & h, vm_obj const & b, vm_obj const &) {
     try {
         href->write(tmp);
         return mk_io_result(mk_vm_unit());
-    } catch (handle_exception e) {
+    } catch (handle_exception & e) {
         return mk_io_failure("write failed");
     }
 }
@@ -608,8 +608,8 @@ static vm_obj serial_deserialize(vm_obj const & h, vm_obj const &) {
     fseek(f, 0, SEEK_SET);
 
     char *data = reinterpret_cast<char *>(malloc(fsize));
-    fread(data, fsize, 1, f);
-    if (ferror(f)) {
+    size_t read = fread(data, fsize, 1, f);
+    if (read != 1 || ferror(f)) {
         clearerr(f);
         return mk_io_failure("deserialize failed");
     }

src/shell/server.cpp

@@ -423,7 +423,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")));
@@ -470,7 +470,7 @@ void server::handle_async_response(server::cmd_req const & req, task<cmd_res> 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")));

src/util/json.hpp

@@ -8600,7 +8600,7 @@ class basic_json
                 m_line_buffer.clear();
                 for (m_cursor = m_start; m_cursor != m_limit; ++m_cursor)
                 {
-                    m_line_buffer.append(1, static_cast<const char>(*m_cursor));
+                    m_line_buffer.append(1, static_cast<char>(*m_cursor));
                 }
 
                 // append 5 characters (size of longest keyword "false") to

src/util/sexpr/format.h

@@ -164,7 +164,6 @@ class format {
     }
     explicit format(name const & v):m_value(sexpr_text(sexpr(v))) {}
     format(format const & f1, format const & f2):m_value(sexpr_compose({f1.m_value, f2.m_value})) {}
-    format(format const & f):m_value(f.m_value) {}
     format_kind kind() const {
         return sexpr_kind(m_value);
     }

src/util/task_builder.h

@@ -128,7 +128,7 @@ class task_builder {
         auto ctok = mk_cancellation_token(m_cancel_tok);
         auto task = wrap(cancellation_support(ctok)).build_without_cancellation();
         ctok->add_child(task);
-        return std::move(task);
+        return task;
     }
 };
 
@@ -155,7 +155,7 @@ task<std::vector<Res>> traverse(std::vector<task<Res>> const & ts) {
     return task_builder<std::vector<Res>>([ts] {
         std::vector<Res> vs;
         for (auto & t : ts) vs.push_back(get(t));
-        return std::move(vs);
+        return vs;
     }).depends_on_fn([to_do] (buffer<gtask> & deps) {
         to_do->erase(std::remove_if(to_do->begin(), to_do->end(),
                 [] (gtask & t) { return t->peek_is_finished(); }),