by_contradiction not found?

Stream: general

[David Loeffler]

I hit the following when preparing examples for a lecture:

import Mathlib

example : False := by
  by_contra h
  sorry

If I hover the mouse over by_contra, a box comes up saying "Alias of by_contradiction". But if I change by_contra into by_contradiction, it gives an unknown tactic error! Presumably I've done something silly here, but can someone tell me exactly what?

[Adam Topaz]

No, I bet that the docstring for by_contra was just copied from mathlib3.

[Adam Topaz]

oh wait, I think this might be a bug.

[Adam Topaz]

we have a term docs#by_contra which is an alias of docs#by_contradiction (a term) which is an alias of docs#Decidable.byContradiction

[Adam Topaz]

we also have a tactic by_contra whose docstring is much longer. For some reason, it seems that the alias docstring is what shows up here.

[Adam Topaz]

Let me try to minimize.

[David Loeffler]

Aha, I hadn't spotted that by_contra is both a term and a tactic. (I was puzzled because I grepped for "by_contradiction" in the library and found lots of examples, but they were all terms.)

[Adam Topaz]

Here is a minimized example:

import Std.Tactic.Alias

def foo' : True := trivial
alias foo := foo'

elab "foo" : tactic => return

example : True := by
  foo
  sorry

[Adam Topaz]

I'm not sure whether this is a bug in the alias command, or somewhere else...

[Adam Topaz]

Pinging @Mario Carneiro since it looks like he wrote the alias command in Std.

[Alex J. Best]

I don't think this is really to do with alias, other than the fact that alias adds a docstring by default. In the following snippet the tactic foo gets the hover of the term foo

import Lean
/--blah-/
def foo : True := trivial

elab "foo" : tactic => return

example : True := by
  foo
  sorry

[Alex J. Best]

Though interestingly if the tactic foo is given a docstring of its own that does show up

[Alex J. Best]

And very interestingly the hover of by_contra h is different to by_contra

[Adam Topaz]

What’s strange is that the by_contra tactic does seem to have a docstring.

[Damiano Testa]

Maybe it is just an issue with Syntax: for hovering purposes, terms seem to have priority over Syntax. Here is a further example:

/--foo syntax-/
syntax "foo" : tactic

example : True := by
  try foo  -- hover shows `foo syntax`
  sorry

/--blah-/
def foo : True := sorry

example : True := by
  try foo  -- hover shows `blah`
  sorry

#check tacticFoo  -- hover shows `foo syntax`

[Mario Carneiro]

this is really weird, I tried to replicate the issue in the hover.lean test and it fails (which is to say it shows the tactic in both cases)

[Mario Carneiro]

and then if I copy the test verbatim to mathlib (even without importing anything from mathlib) the bug returns

[Mario Carneiro]

maybe the bug was recently fixed on accident?

[Damiano Testa]

Mario, where is the hover.lean test?

[Mario Carneiro]

https://github.com/leanprover/lean4/blob/master/tests/lean/interactive/hover.lean

[Damiano Testa]

Also, the hovers over the tactics by_contra h and by_contra do not match, within mathlib, with or without the term by_contra in the enviroment.

[Mario Carneiro]

that's because they are different tactics, IIRC

[Mario Carneiro]

hm, strangely go-to-def also fails on by_contra in example : True := by by_contra; sorry

[Mario Carneiro]

oh, the issue was that I put the test in a namespace

[Damiano Testa]

This is what I get:

import Std.Tactic.Basic

example : True := by
  by_contra h  -- hover: `by_contra` docs
  by_contra    -- hover: `A placeholder term, to be synthesized by unification.`
  sorry

I also think that by_contra is implemented at the same time as by_contra h, though.

[Mario Carneiro]

oh, that makes sense

[Mario Carneiro]

I think the generated _ takes its position from the by_contra token

[Damiano Testa]

Hmm:

example : True := by
  by_contra h  -- hover: `by_contra` docs
  by_contra _  -- hover: `by_contra` docs
  by_contra    -- hover: `A placeholder term, to be synthesized by unification.`
  sorry

[Mario Carneiro]

and the hover for that is blocking go-to-def and stuff for the by_contra tactic

[Damiano Testa]

Ah, the hover for the place-holder takes over when the place-holder is implicit! I get it now, I think.

[Mario Carneiro]

I'm replicating the term/tactic hover confusion in hover.lean now, I will try to track the issue down

[Damiano Testa]

Thanks, Mario! I am curious to know what causes it.

[Mario Carneiro]

oh, this already looks suspicious:

      -- try to find parser docstring from syntax tree
      let stack? := snap.stx.findStack? (·.getRange?.any (·.contains hoverPos))
      let stxDoc? ← match stack? with
        | some stack => stack.findSomeM? fun (stx, _) => do
          return (← findDocString? snap.env stx.getKind).map (·, stx.getRange?.get!)
        | none => pure none

[Damiano Testa]

Btw, the implementation of the by_contra tactic does contain

      | e => Unhygienic.run `(_%$e) -- HACK: hover fails without Unhygienic here

so something is at play here, besides the "precedence of doc-string".

[Mario Carneiro]

because stx.getKind returns the atom's string literal when called on an atom, so if that happens to be a declaration in the environment with a doc string...

[Mario Carneiro]

in fact the same thing seems like it would also happen for local variables, based on this code

[Mario Carneiro]

oh wait no, those use identKind

[Mario Carneiro]

although it does mean that if you define

/-- ident! -/ def ident := 1

then you get ident! as the doc string on every identifier

[Damiano Testa]

Mario Carneiro said:

although it does mean that if you define

/-- ident! -/ def ident := 1

then you get ident! as the doc string on every identifier

It may not be entirely undesirable to have a doc-string when hovering over an identifier (or any other piece of syntax) that informs you of what it is.

Is it possible to have "scoped hovers"?

[Mario Carneiro]

(fixed in lean4#2586)

[Mario Carneiro]

It may not be entirely undesirable to have a doc-string when hovering over an identifier (or any other piece of syntax) that informs you of what it is.

There is already a docstring when hovering over any piece of syntax, that is exactly what we have been seeing here

[Mario Carneiro]

identifiers are in a slightly different category though, the same mechanism doesn't work for them because they aren't considered .nodes

[Mario Carneiro]

besides this, I think a hover on all identifiers wouldn't be that great, it's about as useful as the underscore hover that shows up everywhere

[Mario Carneiro]

there is much more useful information we should be showing

[Kevin Buzzard]

Oh this is great that this issue has been isolated and is being worked on. I've known for a while that there's something weird going on here but always assumed it was my own lack of understanding.

[David Loeffler]

Splendid – thanks Mario and everyone else who contributed to fixing this so quickly!