feat(frontends/lean): allow transient coercions, i.e., coercions that

are not saved in .olean files

library/data/int/basic.lean

@@ -203,13 +203,11 @@ exists_intro (pr1 (rep a))
       a = psub (rep a) : (psub_rep a)⁻¹
     ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod_ext (rep a))⁻¹}))
 
-definition of_nat (n : ℕ) : ℤ := psub (pair n 0)
-
 theorem has_decidable_eq [instance] [protected] : decidable_eq ℤ :=
 take a b : ℤ, _
 
 opaque int
-coercion of_nat
+definition of_nat [coercion] (n : ℕ) : ℤ := psub (pair n 0)
 
 theorem eq_zero_intro (n : ℕ) : psub (pair n n) = 0 :=
 have H : rel (pair n n) (pair 0 0), by simp,

library/data/int/order.lean

@@ -614,8 +614,6 @@ or.elim (em (a = 0))
         have H3 : (to_nat (a * b)) ≠ of_nat 0, from mt of_nat_inj H2,
         mul_cancel_right H3 H))
 
---set_option pp::coercion true
-
 theorem sign_idempotent (a : ℤ) : sign (sign a) = sign a :=
 have temp : of_nat 1 > 0, from iff.elim_left (iff.symm (lt_of_nat 0 1)) succ_pos,
     --this should be done with simp

src/emacs/lean-syntax.el

@@ -70,7 +70,8 @@
      ;; place holder
      (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
      ;; modifiers
-     (,(rx (or "\[notation\]" "\[visible\]" "\[protected\]" "\[private\]" "\[instance\]" "\[class\]" "\[coercion\]" "\[inline\]")) . 'font-lock-doc-face)
+     (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[protected\]" "\[private\]"
+               "\[instance\]" "\[class\]" "\[coercion\]" "\[inline\]")) . 'font-lock-doc-face)
      ;; tactics
      (,(rx symbol-start
            (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "back" "beta" "done" "exact" "repeat")

src/frontends/lean/builtin_cmds.cpp

@@ -46,6 +46,8 @@ static name g_renaming("renaming");
 static name g_as("as");
 static name g_colon(":");
 
+static name g_persistent("[persistent]");
+
 environment print_cmd(parser & p) {
     if (p.curr() == scanner::token_kind::String) {
         p.regular_stream() << p.get_str_val() << endl;
@@ -129,7 +131,8 @@ environment set_option_cmd(parser & p) {
         name lean_id = name("lean") + id;
         decl_it = get_option_declarations().find(lean_id);
         if (decl_it == get_option_declarations().end()) {
-            throw parser_error(sstream() << "unknown option '" << id << "', type 'help options.' for list of available options", id_pos);
+            throw parser_error(sstream() << "unknown option '" << id
+                               << "', type 'help options.' for list of available options", id_pos);
         } else {
             id = lean_id;
         }
@@ -293,14 +296,26 @@ environment open_export_cmd(parser & p, bool open) {
 environment open_cmd(parser & p) { return open_export_cmd(p, true); }
 environment export_cmd(parser & p) { return open_export_cmd(p, false); }
 
+bool parse_persistent(parser & p, bool & persistent) {
+    if (p.curr_is_token_or_id(g_persistent)) {
+        p.next();
+        persistent = true;
+        return true;
+    } else {
+        return false;
+    }
+}
+
 environment coercion_cmd(parser & p) {
+    bool persistent = false;
+    parse_persistent(p, persistent);
     name f   = p.check_constant_next("invalid 'coercion' command, constant expected");
     if (p.curr_is_token(g_colon)) {
         p.next();
         name C = p.check_constant_next("invalid 'coercion' command, constant expected");
-        return add_coercion(p.env(), f, C, p.ios());
+        return add_coercion(p.env(), f, C, p.ios(), persistent);
     } else {
-        return add_coercion(p.env(), f, p.ios());
+        return add_coercion(p.env(), f, p.ios(), persistent);
     }
 }
 

src/frontends/lean/token_table.cpp

@@ -78,7 +78,7 @@ token_table init_token_table() {
          {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
 
     char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion",
-                               "variables", "[private]", "[protected]", "[inline]", "[visible]", "[instance]",
+                               "variables", "[persistent]", "[private]", "[protected]", "[inline]", "[visible]", "[instance]",
                                "[class]", "[coercion]", "abbreviation", "opaque", "transparent",
                                "evaluate", "check", "print", "end", "namespace", "section", "import",
                                "abbreviation", "inductive", "record", "renaming", "extends", "structure", "module", "universe",

src/library/coercion.cpp

@@ -361,11 +361,11 @@ struct coercion_config {
 template class scoped_ext<coercion_config>;
 typedef scoped_ext<coercion_config> coercion_ext;
 
-environment add_coercion(environment const & env, name const & f, name const & C, io_state const & ios) {
-    return coercion_ext::add_entry(env, ios, coercion_entry(f, C));
+environment add_coercion(environment const & env, name const & f, name const & C, io_state const & ios, bool persistent) {
+    return coercion_ext::add_entry(env, ios, coercion_entry(f, C), persistent);
 }
 
-environment add_coercion(environment const & env, name const & f, io_state const & ios) {
+environment add_coercion(environment const & env, name const & f, io_state const & ios, bool persistent) {
     declaration d = env.get(f);
     expr t = d.get_type();
     check_pi(f, t);
@@ -383,10 +383,10 @@ environment add_coercion(environment const & env, name const & f, io_state const
         --i;
         if (i == 0) {
             // last alternative
-            return add_coercion(env, f, Cs[i], ios);
+            return add_coercion(env, f, Cs[i], ios, persistent);
         } else {
             try {
-                return add_coercion(env, f, Cs[i], ios);
+                return add_coercion(env, f, Cs[i], ios, persistent);
             } catch (exception &) {
                 // failed, keep trying...
             }

src/library/coercion.h

@@ -35,9 +35,12 @@ namespace lean {
    \pre \c f is a constant defined in \c env.
 
    \remark \c ios is used to report warning messages.
+
+   \remark if persistent == true, then coercion is saved in .olean files
 */
-environment add_coercion(environment const & env, name const & f, io_state const & ios);
-environment add_coercion(environment const & env, name const & f, name const & C, io_state const & ios);
+environment add_coercion(environment const & env, name const & f, io_state const & ios, bool persistent = true);
+environment add_coercion(environment const & env, name const & f, name const & C, io_state const & ios,
+                         bool persistent = true);
 /** \brief If \c f is a coercion, then return the name of the 'from-class' and the number of
     class parameters.
 */