local notation in doc-gen

Stream: general

[Rob Lewis]

Moving from https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20in.20the.20wild to a new thread:

Unfortunately there seem to be lots of uses of localized notation that only work with namespaces open. e.g. https://github.com/leanprover-community/mathlib/blob/5a2e7d7/src/number_theory/dioph.lean#L585 which actually refers to fin2.of_nat'.

[Rob Lewis]

If you open_locale dioph without fin2 open, you get an error.

[Mario Carneiro]

we should fix the local notation declarations to use full paths, I think

[Mario Carneiro]

or at least localized notations

[Rob Lewis]

I don't think it matters for regular local notation -- once you close the section that opened the namespace, you also close the notation forever. It does matter for localized notation.

[Mario Carneiro]

it's also partially the fault of our implementation of localized notations using strings that are injected into the code. If we used local notation then lean would do the name resolution only once (pretty sure) but since we're copying and pasting it gets resolved separately on every occurrence

[Floris van Doorn]

Yes, this is a known issue:

* Warning 2: You have to fully specify the names used in localized notation, so that the localized
  notation also works when the appropriate namespaces are not opened.

Normal notation does the name resolution at parsing time, but the current setup of localized notation does it at the time you open the locale.

[Floris van Doorn]

I'm not sure how to resolve this (without touching C++ or writing a parser that can at least recognize all occurrences of names in a notation declaration).

[Floris van Doorn]

We could probably write a linter for it

[Mario Carneiro]

How?

[Rob Lewis]

We haven't had a new linter in a while!

[Mario Carneiro]

require that the local notation contains := _root_ perhaps?

[Rob Lewis]

It can just do exactly what I'm trying to do now, open every locale in an envitonment with no namespaces open.

[Mario Carneiro]

oh I see, you don't even need to use the notation

[Floris van Doorn]

Every occurrence of localized notation generates a decl with an attribute. You can look at these decls and try to add the local notation to the environment the moment you call #lint (and then call #lint_mathlib without open namespaces)

[Mario Carneiro]

I know there are some aspects of local notation (like variable names) that are not checked until they are used

[Floris van Doorn]

That probably doesn't need a linter. We can assume that all localized notation is used at least once in mathlib.

[Mario Carneiro]

I would not be surprised if that assumption is false

[Floris van Doorn]

Or I guess you could write localized notation that refers to a local variable, and then that only works in that file? That is unlikely to happen accidentally.

[Mario Carneiro]

forgetting that the notation exists seems like a likely mistake

[Rob Lewis]

So, doc-gen is using src#tactic_state.pp_tagged to pretty print exprs, which, I don't know what that is and it doesn't seem to be using localized notation?

[Rob Lewis]

Not using local notation, that is.

[Mario Carneiro]

This seems to work:

def bar := 1
local notation `foo` := bar
theorem T : bar = 1 := rfl -- looks like foo = 1
run_cmd do
  ef ← tactic.pp_tagged `(bar = 1),
  tactic.trace $ ef.untag (λ _ f, f) -- foo = 1

[Rob Lewis]

doc-gen doesn't seem to ever pass it through untag.

[Rob Lewis]

It creates a json object with the eformat object in it and then it disappears into C++.

[Mario Carneiro]

I'm just doing the untag to print it, AFAICT it doesn't change the content of the format

[Rob Lewis]

I don't know what goes on after it turns into an eformat. But at https://github.com/leanprover-community/doc-gen/blob/master/src/export_json.lean#L390 if you change the notation to local notation, opt params are no longer printed with the nice formatting.

[Mario Carneiro]

run_cmd do
  tagged_format.of_format ef ← tactic.pp_tagged `(bar),
  tactic.trace $ format.to_string ef -- foo

[Mario Carneiro]

wait, it's at the end of the file?

[Mario Carneiro]

how does that even work

[Mario Carneiro]

My guess is that using lean --run makes it act like

import export_json
#eval main

which is to say, it's in another module scope and so you lose local notations

[Rob Lewis]

Hmm. eformat and efmt aren't the same, so I was misreading doc-gen... you might be right

[Rob Lewis]

image.png