Zulip Chat Archive

Stream: general

Topic: sanity check


Patrick Massot (Aug 28 2019 at 08:30):

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 (Aug 28 2019 at 08:34):

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 (Aug 28 2019 at 08:35):

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

Floris van Doorn (Aug 28 2019 at 14:26):

Thanks for actually cleaning up the library!

Floris van Doorn (Aug 28 2019 at 14:26):

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

Patrick Massot (Aug 28 2019 at 14:27):

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

Floris van Doorn (Aug 28 2019 at 18:03):

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 (Aug 28 2019 at 21:38):

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

Floris van Doorn (Aug 28 2019 at 22:07):

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 (Aug 28 2019 at 22:08):

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 (Aug 28 2019 at 22:10):

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 (Aug 29 2019 at 12:10):

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

Johan Commelin (Sep 02 2019 at 17:38):

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 (Sep 02 2019 at 18:17):

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 (Sep 02 2019 at 18:39):

@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 (Sep 02 2019 at 18:41):

oh yes, it should be tactic.trace.

Johan Commelin (Sep 02 2019 at 18:41):

1sec

Floris van Doorn (Sep 02 2019 at 18:42):

I'm also building the project myself rn.

Johan Commelin (Sep 02 2019 at 18:42):

None of them time out

Floris van Doorn (Sep 02 2019 at 18:43):

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 (Sep 02 2019 at 18:45):

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

Floris van Doorn (Sep 02 2019 at 18:49):

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

Johan Commelin (Sep 02 2019 at 18:50):

Can you reproduce the timeout?

Floris van Doorn (Sep 02 2019 at 18:59):

yes

Floris van Doorn (Sep 02 2019 at 20:13):

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 (Sep 02 2019 at 22:30):

I wonder why. Is and_decidable doing something dumb?

Chris Hughes (Sep 02 2019 at 22:33):

I checked, and it looks fine.

Scott Morrison (Sep 02 2019 at 22:42):

Yeah, I couldn't understand either.

Reid Barton (Sep 02 2019 at 23:11):

Are we talking about the kernel or the VM here?

Scott Morrison (Sep 02 2019 at 23:14):

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

Scott Morrison (Sep 02 2019 at 23:15):

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

Mario Carneiro (Sep 02 2019 at 23:24):

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

Mario Carneiro (Sep 02 2019 at 23:24):

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 (Sep 02 2019 at 23:25):

One way to force delayed evaluation is to use a thunk

Floris van Doorn (Sep 03 2019 at 00:47):

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 (Sep 03 2019 at 07:21):

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 (Sep 03 2019 at 07:26):

if uses thunks

Chris Hughes (Sep 03 2019 at 07:27):

So why is the and.decidable instance slow?

Mario Carneiro (Sep 03 2019 at 07:27):

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

Chris Hughes (Sep 03 2019 at 07:28):

So that means it shouldn't be slow right?

Mario Carneiro (Sep 03 2019 at 07:29):

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

Mario Carneiro (Sep 03 2019 at 07:29):

I recommend looking at the generated bytecode

Mario Carneiro (Sep 03 2019 at 07:35):

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 (Sep 03 2019 at 07:36):

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 (Sep 03 2019 at 07:38):

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

Mario Carneiro (Sep 03 2019 at 07:38):

arguably that should have been set

Scott Morrison (Sep 03 2019 at 07:59):

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

Floris van Doorn (Sep 03 2019 at 16:24):

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 (Sep 03 2019 at 17:45):

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

Mario Carneiro (Sep 03 2019 at 17:48):

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 (Sep 03 2019 at 17:50):

also decidable.true of course

Floris van Doorn (Sep 03 2019 at 18:22):

Added them to #1393.

Floris van Doorn (Sep 03 2019 at 18:43):

Do you think decidable.to_boolshould be added?

Mario Carneiro (Sep 03 2019 at 19:13):

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

Floris van Doorn (Sep 04 2019 at 15:28):

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

Sebastien Gouezel (Sep 09 2019 at 07:56):

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 (Sep 10 2019 at 05:20):

  • 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 (Sep 10 2019 at 05:24):

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

Mario Carneiro (Sep 10 2019 at 07:12):

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 (Sep 24 2019 at 05:37):

@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 (Sep 24 2019 at 05:37):

I hope to find time to kill some of them

Floris van Doorn (Sep 24 2019 at 22:25):

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


Last updated: Dec 20 2023 at 11:08 UTC