Question about {! !}

Stream: general

[Stanislas Polu]

Hi! The following proof seems to type-check. Any idea what is going on?

import data.finset.basic
import data.nat.interval

example
  (vertices : finset ℕ)
  (diagonals : finset (finset ℕ))
  (h₀ : vertices = finset.Icc 1 5)
  (h₁ : ∀ (m n : ℕ), ({m,n} : finset ℕ) ∈ diagonals ↔
    {m,n} ⊂ vertices ∧ m ≠ n ∧ m ≠ n + 1 ∧ m ≠ n - 1 ∧ {m,n} ≠ ({1,5} : finset ℕ)) :
  diagonals.card = 5 :=
begin
  have h₂ : diagonals = {! {2,4}, {1,3}, {3,5} !}, {
    dec_trivial!,
  },
  rw h₂,
  dec_trivial!,
end

[Stanislas Polu]

Some weird interaction with the docstring parser?

[Jason Rute]

Do you know about hole commands using {! … !}? I’m struggling to find documentation to show you, but you can search for it hear on Zulip.

[Stanislas Polu]

It vaguely appears in comments in tactic/core.lean

[Stanislas Polu]

Clearly unused and undocumented

[Jason Rute]

In short, they are, or used to be, a way to highlight some code and prompt vs code to give you a lightbulb with possible actions (like expanding a template for a match).

[Stanislas Polu]

Models will find holes :) I guess I need to blacklist {!

[Jason Rute]

Yes, I don’t think you want your model producing them. :)

[Stanislas Polu]

Probably needs a fix in Lean as well I think would be sad to introduce false without lean make complaining about it

[Jason Rute]

I would make a GitHub issue for lean 3 community edition.

[Stanislas Polu]

Filed here: https://github.com/leanprover-community/lean/issues/725

[Alex J. Best]

What do you mean it seems to type-check, I get declaration [anonymous] uses sorry

[Sebastien Gouezel]

Can you get a proof of false from it?

[Sebastien Gouezel]

I also see the sorry.

[Mario Carneiro]

The source of the issue is that {! !} seems to produce a synthetic sorry (printed as ??), which suppresses most error reporting about it because this happens after an error was already reported so the knock on errors are unhelpful

[Stanislas Polu]

Ah you're right that we have a sorry :+1: So we're safe

[Mario Carneiro]

if you replace the hole command with (λ) or something then you will notice the tactics also seem to succeed

[Mario Carneiro]

I'm inclined to call this not-a-bug

[Stanislas Polu]

Yep closed the issue

[Stanislas Polu]

Source of the confusion on my end comes from the fact that we don't use the lean --make command output to "find out sorry" and instead inspect the code for sorry and admit.

[Stanislas Polu]

Is there a way to make lean --make error (instead of warning) in presence of any form of sorry ?

[Mario Carneiro]

just look for {!

[Alex J. Best]

Do you have any other warnings in the project?

[Alex J. Best]

Because the exit code of the process will be 1 in the case of warnings, and 0 otherwise, so maybe you can just use that?

[Mario Carneiro]

It looks like using trust level 0 will cause an error when you use sorry

[Mario Carneiro]

the exit code of lean is 0 in the case of sorry normally

[Mario Carneiro]

$ echo "def foo : nat := sorry" > test.lean
$ lean test.lean
/test.lean:1:0: warning: declaration 'foo' uses sorry
$ echo $?
0
$ lean test.lean -t0
/test.lean:1:17: error: failed to expand macro
$ echo $?
1

[Alex J. Best]

Hmm it seems there is a difference between lean and lean --make here, in my test the first also resulted in 1 with lean --make

[Mario Carneiro]

I'm not reproducing, both lean and lean --make have the same error code behavior

[Mario Carneiro]

although lean --make will not report an error if the sorry was in a file that has already been compiled (even if you use -t2 to compile it the first time and -t0 for the second)

[Mario Carneiro]

The sorry macro has trust level 2, so if you use -t1 or -t0 then sorry causes errors

[Mario Carneiro]

-t1 is probably the most appropriate setting here. -t0 will also expand other macros like strings and expr quote

[Mario Carneiro]

(the default setting is the amusingly named LEAN_BELIEVER_TRUST_LEVEL = 1024 but there aren't any other effects for values higher than 2)

[Alex J. Best]

My mistake! Sorry for the noise :smile:

[Stanislas Polu]

Thanks Mario! Will experiment with trust levels :+1:

[Mario Carneiro]

the only one of gabriel's examples from the issue that typechecks at -t0 is

example : false :=
begin
  tactic.add_decl (declaration.ax `very.clever [] `(false)),
  exact very.clever,
end

[Mario Carneiro]

however that example fails if it is made into a theorem. If it is a def then it's equivalent to actually adding an axiom very.clever; you have to #print axioms foo to detect this