Skip to content

Commit

Permalink
fix(frontends/lean/parser_config): serialize notation names (#759)
Browse files Browse the repository at this point in the history
Addendum to #754. The underlying issue in #754 (comment) was that the `.olean` files did not serialize the notation names, so although everything works in a single-session `lean --make` call, if you try to do it in multiple passes the read-in `.olean` files will not have the notation names and will cause a conflict.

This changes the olean format, but AFAIR there is no olean version or anything to bump.
  • Loading branch information
digama0 committed Aug 25, 2022
1 parent f2b2bee commit ab42dba
Showing 1 changed file with 6 additions and 6 deletions.
12 changes: 6 additions & 6 deletions src/frontends/lean/parser_config.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -350,8 +350,8 @@ struct notation_config {
}
static char const * get_serialization_key() { return "NOTA"; }

static void write_entry(serializer & s, entry const & e) {
s << static_cast<char>(e.kind()) << e.overload() << e.parse_only() << e.get_expr();
static void write_entry(serializer & s, entry const & e) {
s << static_cast<char>(e.kind()) << e.get_name() << e.overload() << e.parse_only() << e.get_expr();
if (e.is_numeral()) {
s << e.get_num();
} else {
Expand Down Expand Up @@ -408,12 +408,12 @@ struct notation_config {

static entry read_entry(deserializer & d) {
notation_entry_kind k = static_cast<notation_entry_kind>(d.read_char());
bool overload, parse_only; expr e;
d >> overload >> parse_only >> e;
name n; bool overload, parse_only; expr e;
d >> n >> overload >> parse_only >> e;
if (k == notation_entry_kind::Numeral) {
mpz val;
d >> val;
return entry(val, e, overload, parse_only);
return entry(val, e, overload, parse_only, n);
} else {
bool is_nud = k == notation_entry_kind::NuD;
unsigned sz; char _g;
Expand All @@ -424,7 +424,7 @@ struct notation_config {
ts.push_back(read_transition(d));
unsigned priority;
d >> priority;
return entry(is_nud, to_list(ts.begin(), ts.end()), e, overload, priority, g, parse_only);
return entry(is_nud, to_list(ts.begin(), ts.end()), e, overload, priority, g, parse_only, n);
}
}
static optional<unsigned> get_fingerprint(entry const &) {
Expand Down

0 comments on commit ab42dba

Please sign in to comment.