Zulip Chat Archive

Stream: general

Topic: libiconfig


Scott Morrison (Jun 03 2019 at 11:47):

@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 (Jun 03 2019 at 11:47):

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

Keeley Hoek (Jun 03 2019 at 13:14):

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 (Jun 03 2019 at 13:19):

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 (Jun 03 2019 at 15:06):

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 (Jun 03 2019 at 15:06):

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 (Jun 03 2019 at 15:52):

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 (Jun 03 2019 at 15:56):

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 (Jun 04 2019 at 00:03):

Ok, I'll get rid of it!

Scott Morrison (Jun 04 2019 at 00:08):

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

Scott Morrison (Jun 04 2019 at 12:02):

@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 (Jun 04 2019 at 12:05):

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 (Jun 04 2019 at 12:07):

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

Keeley Hoek (Jun 04 2019 at 12:07):

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

Scott Morrison (Jun 04 2019 at 12:09):

Err... this is weird.

Scott Morrison (Jun 04 2019 at 12:09):

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

Scott Morrison (Jun 04 2019 at 12:10):

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 (Jun 04 2019 at 12:11):

:O

Keeley Hoek (Jun 04 2019 at 12:21):

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

Keeley Hoek (Jun 04 2019 at 12:22):

@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 (Jun 04 2019 at 12:23):

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 (Jun 04 2019 at 13:44):

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


Last updated: Dec 20 2023 at 11:08 UTC