sanity check

Stream: general

[Patrick Massot]

I'm working a bit on the #sanity_check cleanup of topology. @Floris van Doorn Is there a reason why the command is not imported by default? Each file needs to add an import and then remember to remove it. It would also help tremendously if the command could print the type of the unused argument instead of only the number. But it's already very nice! What is weird is that removing useless type classes can have unexpected consequences on elaboration later one. I already had to add a couple of apply_instance.

[Patrick Massot]

Maybe we could have a hole command dumping the output of #sanity_check into the Lean file, that would save a copy-paste

[Patrick Massot]

Another potential improvement: when the command find an unused argument, check whether it's duplicated and report it.

[Floris van Doorn]

Thanks for actually cleaning up the library!

[Floris van Doorn]

I indeed forgot to add an import to tactic.basic. I will do that. The other improvements also seem doable.

[Patrick Massot]

It would be very nice to enter a self-sustaining cycle of cleanup/sanity_check improvements

[Floris van Doorn]

One disadvantage with a hole command is that you cannot write a hole when a command is expected, but only where an expression is expected. So you have to write something like run_cmd {!!} or example : {!!}. And then after the hole command replaces itself, you still have a broken run_cmd or example...

[Floris van Doorn]

Added all feature requests (except the self-sustaining cycle of cleanup/sanity_check improvements) in #1369.

[Floris van Doorn]

The unused argument command will now return something like

-- tactic\core.lean
#print tactic.symmetry_hyp /- argument 2: (md : opt_param transparency transparency.semireducible) -/

-- meta\rb_map.lean
#print native.rb_map.find_def /- argument 4: [_inst_2 : decidable_rel has_lt.lt] -/

-- logic\basic.lean
#print imp_intro /- argument 4: (h₂ : β) -/
#print not_iff /- argument 3: [_inst_1 : decidable a] -/
#print ball_of_forall /- argument 6: (_x : q x) -/

-- data\list\defs.lean
#print list.func.neg /- argument 2: [_inst_1 : inhabited α] -/

-- category\basic.lean
#print map_seq /- argument 6: [_inst_2 : is_lawful_applicative F] (duplicate) -/
#print seq_map_assoc /- argument 6: [_inst_2 : is_lawful_applicative F] (duplicate) -/

[Floris van Doorn]

I also added a new check: whether a namespace occurs twice in the name:

-- tactic\core.lean
#print tactic.tactic.has_to_tactic_format /- The namespace tactic is duplicated in the name -/
#print tactic.tactic.use /- The namespace tactic is duplicated in the name -/

[Floris van Doorn]

Fun fact: for this improvement I had to remove an unused argument from the instance list.decidable_chain' :grinning_face_with_smiling_eyes:

[Patrick Massot]

Amazing! I promise I'll the topology fix as soon as this gets merged.

[Johan Commelin]

I'm getting deterministic timeouts if I run #sanity_check at the bottom of https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/adic_space.lean

[Floris van Doorn]

That's not good. I'll take a look.
Which of the following get a timeout?

run_cmd print_decls_current_file prettify_unused_arguments >>= trace
run_cmd print_decls_current_file incorrect_def_lemma >>= trace
run_cmd print_decls_current_file dup_namespace >>= trace

[Johan Commelin]

@Floris van Doorn

type mismatch at application
  print_decls_current_file prettify_unused_arguments >>= trace
term
  trace
has type
  string → thunk ?m_1 → ?m_1 : Type ?
but is expected to have type
  format → tactic ?m_1 : Type

[Floris van Doorn]

oh yes, it should be tactic.trace.

[Johan Commelin]

1sec

[Floris van Doorn]

I'm also building the project myself rn.

[Johan Commelin]

None of them time out

[Floris van Doorn]

Ok, then for the moment you can use those, they give the same information. I'll make #sanity_check more efficient (currently I'm running through the whole environment 3 times)

[Johan Commelin]

They don't print anything at all... which might mean our code is sane...

[Floris van Doorn]

Yes, I just ran them myself, and that file in sane :)

[Johan Commelin]

Can you reproduce the timeout?

[Floris van Doorn]

yes

[Floris van Doorn]

I managed to speed up #sanity_check by about 2 orders of magnitude. (it now takes 100-200ms in adic_space)

One of the slowdowns was surprising me: if you run if p ∧ q then ... else ... and p is false, then q will also be checked. You have to use && instead:

open tactic
set_option profiler true
-- very fast
run_cmd do e ← get_env, e.mfold [] $ λ d ds, return $ if ff && d.is_auto_generated e then d::ds else ds
-- very slow (assuming you are importing enough files)
run_cmd do e ← get_env, e.mfold [] $ λ d ds, return $ if ff ∧ d.is_auto_generated e then d::ds else ds

[Scott Morrison]

I wonder why. Is and_decidable doing something dumb?

[Chris Hughes]

I checked, and it looks fine.

[Scott Morrison]

Yeah, I couldn't understand either.

[Reid Barton]

Are we talking about the kernel or the VM here?

[Scott Morrison]

Looks like the VM, I guess, since it's inside a run_cmd.

[Scott Morrison]

I admit I have no idea what the VM does when it sees if or ∧.

[Mario Carneiro]

It's actually surprising that either one is short circuiting. It's probably because of inlining

[Mario Carneiro]

The standard semantics of lean would require that both sides of the and be evaluated before the function is called (i.e. eager evaluation)

[Mario Carneiro]

One way to force delayed evaluation is to use a thunk

[Floris van Doorn]

Yeah, in the proof of and_decidable it probably evaluates the then clause before it evaluates the if-then-else. We should indeed rewrite it using a thunk.

[Chris Hughes]

Why is this super fast in that case?

def ack : nat → nat → nat
| 0     y     := y+1
| (x+1) 0     := ack x 1
| (x+1) (y+1) := ack x (ack (x+1) y)

def X : ℕ := if false then ack 100 100 else 0

#eval X

[Mario Carneiro]

if uses thunks

[Chris Hughes]

So why is the and.decidable instance slow?

[Mario Carneiro]

it uses thunks on the then and else branches, not on the condition (which must be evaluated first)

[Chris Hughes]

So that means it shouldn't be slow right?

[Mario Carneiro]

The difference is that band is @[inline] and and.decidable isn't

[Mario Carneiro]

I recommend looking at the generated bytecode

[Mario Carneiro]

def foo := ff
set_option trace.compiler.optimize_bytecode true
#eval if false && foo then 1 else 0
-- [compiler.optimize_bytecode]  _main 0
-- 0: scnstr #1
-- 1: ginvoke decidable.false
-- 2: scnstr #0
-- 3: ginvoke decidable.to_bool
-- 4: cases2 7
-- 5: scnstr #0
-- 6: goto 12
-- 7: ginvoke foo
-- 8: cases2 11
-- 9: scnstr #0
-- 10: goto 12
-- 11: scnstr #1
-- 12: ginvoke bool.decidable_eq._main
-- 13: cases2 16
-- 14: scnstr #0
-- 15: goto 17
-- 16: scnstr #1
-- 17: cfun nat.repr
-- 18: ret

#eval if false ∧ foo then 1 else 0
-- [compiler.optimize_bytecode]  _main 0
-- 0: scnstr #1
-- 1: ginvoke foo
-- 2: ginvoke bool.decidable_eq._main
-- 3: ginvoke decidable.false
-- 4: scnstr #0
-- 5: scnstr #0
-- 6: ginvoke and.decidable
-- 7: cases2 10
-- 8: scnstr #0
-- 9: goto 11
-- 10: scnstr #1
-- 11: cfun nat.repr
-- 12: ret

Notice in the second one that there is an explicit call to and.decidable at line 6, which needs foo to be called first (line 1). In the second one there is no call to band at all; instead it's all been inlined to an if-then (the cases2 at line 4) and the call to foo only happens in the second branch (line 7)

[Mario Carneiro]

If you use ff instead of false in these examples, the call to foo disappears entirely, because lean optimizes ff && foo to ff directly after unfolding the definition of &&

[Mario Carneiro]

If you use attribute [inline] decidable.false and.decidable then you get the expected code

[Mario Carneiro]

arguably that should have been set

[Scott Morrison]

We can provide a higher priority instance that inclines, can't we?

[Floris van Doorn]

I think we can just add the line attribute [inline] and.decidable or.decidable decidable.false to some file that everything imports. Shall I add it to logic/basic? Are there other declarations that need the [inline] attribute?

[Mario Carneiro]

logic.basic looks like a good place for it. The initial part contains a few other "omissions" from the core logic library

[Mario Carneiro]

Inline annotations are a bit of a black art. Probably implies.decidable is also good, definitely not.decidable, not so sure about iff and xor but I'm leaning toward inlining them

[Mario Carneiro]

also decidable.true of course

[Floris van Doorn]

Added them to #1393.

[Floris van Doorn]

Do you think decidable.to_boolshould be added?

[Mario Carneiro]

It should be the identity function, although I'm not sure if lean knows to render it as such

[Floris van Doorn]

I don't think so. I think it will then run both decidable.to_bool and bool.decidable_eq.

[Sebastien Gouezel]

I have started using sanity_check to clean up some files, and I found it super-useful. Just for the record, two small additions that I would find worthy:

• define an attribute sanity_check_skip for statements that should be skipped by sanity_check. For instance, theorem imp_intro {α β} (h : α) (h₂ : β) : α := h in logic/basic.lean has an unused argument by design. Or in fiber bundles the function topological_fiber_bundle.fiber has a lot of unused arguments, but this is to get a new name for a type, in order for typeclass inference to work correctly. If we don't add such an attribute, they will show up forever in the output of sanity_check.
• would it be possible to show as a mistake the use of > or >= in the assumptions or conclusions of theorems? Rewrites would be really easier if < and <= were used consistently all over mathlib, and I think this is a move we will have to do some day.

[Floris van Doorn]

• I was indeed thinking that some declarations would show up forever in the output of sanity_check, but it's actually a good idea to whitelist declarations that we know are fine.
• Yes, it is easy to check whether >/>= (i.e. ge/gt) are used in lemma statements. Are there other declarations we want to always avoid in lemma statements?

[Scott Morrison]

So is the attribute suppressing output of #sanity_check going to be @[sane] or @[insane]? :-)

[Mario Carneiro]

By analogy to Rust's unsafe block, which brackets code that is safe but for which the programmer, not the compiler, ensures safety, it seems that insane is the correct polarity

[Johan Commelin]

@Scott Morrison Thanks for the updated list at https://gist.github.com/semorrison/16d80d2cd154f6473af57b0c9e6912bb
I see quite a lot of unused decidable_eqs listed there (-; :tada: These reports are really useful.

[Johan Commelin]

I hope to find time to kill some of them

[Floris van Doorn]

I added @Sebastien Gouezel's suggestions to #sanity_check in #1487, and made some other improvements. I went for the attribute name [sanity_skip].