catch leftover set_option commands

[rwbarton]

I think there's no good reason to have set_option pp.* or set_option trace.* lines under src/, but people sometimes leave these by mistake. It should be easy to catch these in Travis and fail quickly (doesn't even require building anything).

[rwbarton]

Are there other set_option categories that should have the same treatment?

Here is a list of all the distinct occurrences of set_option under src/ (I ran git grep -h '\bset_option\b' src/ | sort | uniq):

set_option class.instance_max_depth 100
set_option class.instance_max_depth 120
set_option class.instance_max_depth 180
set_option class.instance_max_depth 32
set_option class.instance_max_depth 36
set_option class.instance_max_depth 37
set_option class.instance_max_depth 39
set_option class.instance_max_depth 40
set_option class.instance_max_depth 41
set_option class.instance_max_depth 43
set_option class.instance_max_depth 45
set_option class.instance_max_depth 48
set_option class.instance_max_depth 49
set_option class.instance_max_depth 50
set_option class.instance_max_depth 55
set_option class.instance_max_depth 60
set_option class.instance_max_depth 70
set_option class.instance_max_depth 90
set_option class.instance_max_depth 95
set_option eqn_compiler.max_steps 50000
set_option eqn_compiler.zeta false
set_option eqn_compiler.zeta true
set_option old_structure_cmd true
set_option pp.universes false
set_option pp.universes true
-- set_option profiler true

Not quite sure what is going on with the last one (in src/tactic/lint.lean), but with the exception of set_option pp.universes, already mentioned above, the rest are fine.

[cipher1024]

profiler should be removed (even if it wasn't commented out)

[rwbarton]

Right, I agree set_option profiler is generally bad!

In the case of src/tactic/lint.lean in particular, there are a bunch of commented out options and commands at the end of the file. I don't understand their purpose. They should be either documented or deleted, but I don't know which.

[cipher1024]

If you do git blame, who put them there?

[robertylewis]

They're useful to quickly test new linters. (Floris had them there originally, I assume for this reason, and I didn't delete them.) Removing them is fine, they're not important.

[robertylewis]

Oops, didn't mean to close this...

[vihdzp]

Nowadays, isn't there a linter that can do this?

[fpvandoorn]

I think #5330 the style linter checks for these spurious set_option lines,