calling a tactic without importing it

Stream: general

[Scott Morrison]

I am trying to write a tactic that will invoke norm_num, if it has otherwise been imported, and otherwise fail. I need this to work without actually importing norm_num.

[Scott Morrison]

Any suggestions?

[Mario Carneiro]

search for norm_num in the environment and call eval_expr on it

[Mario Carneiro]

import tactic.norm_num -- remove me

open tactic interactive
example : 2 + 2 = 4 :=
by try { do
  t ← mk_const `tactic.interactive.norm_num1,
  f ← eval_expr (loc → tactic unit) t,
  f (loc.ns [none]) }

[Scott Morrison]

Thanks.

[Scott Morrison]

It would be nice if norm_num didn't have to import tactic.interactive. :-)

[Scott Morrison]

I've just been looking; that seems rather unlikely.

[Keeley Hoek]

Stuff importing tactic.interactive has been a problem for me before too---is there scope for putting all of the real defs in tactic.interactive somewhere else (maybe tactic.interactive.basic?) and making tactic.interactive just a stub which conveniently includes most of mathlib's interactive stuff?

[Simon Hudon]

I suggested decoupling some of those dependencies in #878 but it did not seem like a popular suggestion

[Scott Morrison]

I think this is a great idea. tactic.basic and tactic.interactive should both be chopped up into tiny pieces. :-)

[Simon Hudon]

Sounds pretty gory :P

[Simon Hudon]

In general, I'd like a tool to analyze the dependencies of mathlib and detect the needless imports