libiconfig

Stream: general

[Scott Morrison]

@Keeley Hoek, could you remind me what your libiconfig repository is for? If we aspire to incorporating rewrite_search into mathlib, what are we going to do with this dependency? Remove it? Merge it first?

[Scott Morrison]

I just had to modify it a little bit to compile against current mathlib, so I made a PR on your repository.

[Keeley Hoek]

I suppose the dream was to PR it. It's short for LIBInteractiveCONFIG.

The point is to add a custom interactive monad which can parse config options. It makes mishmash syntax like rewrite_search { visualiser, depth := 50, strategy.bfs, metric.svm { mode := float } } and simultaneously also allow e.g. rewrite_search { no visualiser, strategy := bfs, metric := svm } and having sub-configs all work (without a host of opens to get the right name spaces of everything too), and having/resolving defaults, etc. (Okay, these are really long examples, but the point is the flexibility.) To be clear, we use a custom interaction monad to implement this, but this all works inside a normal tactic block.

It can automatically do some pretty cool stuff; e.g. if you have a normal lean structure, then there is e.g. a command which lets you do iconfig_add_struct[rewrite_search] tactic.rewrite_search.config which automatically creates setters for all of the fields of the structure tactic.rewrite_search.config inside the custom monad, and then there is an API to automatically have an instance of the structure synthesised from this data without having to manually build it from the value of each field yourself. (It's literally like mk_struct and then the type.) This supports the usual := blah default option syntax declared in normal structures, and gives a nice error if something can't be filled in, etc. You can also create arbitrary custom def do_stuff : iconfig unit := ... functions which can do arbitrary configuration logic when run as rewrite_search { do_stuff } for example.

It definitely seems like a thing people could want to use.

[Keeley Hoek]

I could get it into canonical-style state on Friday, if you're not so keen. Of course, it's not absolutely required.

[Scott Morrison]

It does seem a nice feature. On the other hand, it is an extra layer of complexity. (In the back of my mind, :four_leaf_clover: lurks...)

[Scott Morrison]

How much work is it going to be to remove this from rewrite_search for the PR, then possibly add it back later?

[Scott Morrison]

Also: I apparently can't write:

meta def rws : tactic string := `[rewrite_search { explain := tt }] >> pure ""

anymore. I get an error

type mismatch at application
  iconfig.rewrite_search.interactive.explain ⁇ tt
term
  tt
has type
  bool
but is expected to have type
  tactic_state

Do you know a work-around?

[Scott Morrison]

Ugh, okay, I think I want this libiconfig stuff gone, sorry. I can't work out how to call tactic.rewrite_search by hand and just pass it configuration options I want...

[Keeley Hoek]

Ok, I'll get rid of it!

[Scott Morrison]

Thank you. :-) Sorry, I know you were pleased to get all those config options working nicely!

[Scott Morrison]

@Keeley Hoek Any chance you can tell me how to construct a tactic unit that calls rewrite_search with explain := tt? I just can't do it. :-( I would like to have this for my talk in a day or two...

[Keeley Hoek]

Ahhh, @Scott Morrison, super rushing right now, but pasting:

meta def rws : tactic string := `[rewrite_search {explain := tt}] >> pure ""

directly into test/rewrite_search.lean works just fine for me. Can you reproduce?

[Scott Morrison]

Thank you. I'm absolutely sure I tried that earlier and got a mysterious error. :-) Sorry for the interruption!

[Keeley Hoek]

I copied it from what you wrote earlier! So yeah, no idea what's going on there

[Scott Morrison]

Err... this is weird.

[Scott Morrison]

That compiles, but all the trace messages are proofs for the wrong theorems...?

[Scott Morrison]

For every single rewrite problem it is printing one of

/- `rewrite_search` says -/
conv_lhs { congr, skip, erw [functor.image_preimage] },
conv_lhs { erw [functor.image_preimage] },
conv_lhs { congr, erw [functor.image_preimage] },
conv_lhs { erw [functor.image_preimage] }

or

/- `rewrite_search` says -/
conv_rhs { erw [functor.image_preimage] }

[Keeley Hoek]

:O

[Keeley Hoek]

Okay, what must have happened is that the congr-mode tracked rewrite reporting got broken when it was extracted for the mathlib

[Keeley Hoek]

@Scott Morrison
I have to sleep now (exam :O), but I think the fastest solution is to put the old rewrite_all folder verbatim back in the lean-rewrite-search repo and then deleting it from the mathlib version

[Keeley Hoek]

I don't know your mathlib version exactly but I think that's why garbage is coming out
I dont think what you are seeing are poofs at all

[Scott Morrison]

Got it. I think I've gone back to an old version successfully.