Stream: coqbot devs & users

Topic: coqbot minimize


view this post on Zulip Ralf Jung (Oct 26 2020 at 13:46):

I am trying the "coqbot minimize" feature in https://github.com/coq/coq/issues/13246... should I expect the bot to post some message like "I got your request, here's a link where you can follow its progress"? Or is the bot silent until it is done? How do I know if I used the command correctly?

view this post on Zulip Ralf Jung (Oct 26 2020 at 13:49):

hm, maybe the @coqbot needs to be the first thing in the comment?

view this post on Zulip Ralf Jung (Oct 26 2020 at 13:50):

no that does not seem to change anything

view this post on Zulip Ralf Jung (Oct 26 2020 at 13:50):

@Théo Zimmermann any advice? :D

view this post on Zulip Théo Zimmermann (Oct 26 2020 at 13:51):

Yes, I think that the bot should answer something. Let me see...

view this post on Zulip Ralf Jung (Oct 26 2020 at 13:52):

FWIW, it would be really useful if I could just put the coq sample code into ```coq right in the comment and have the bot put that into some well-known file instead of having to use that cat contortion

view this post on Zulip Théo Zimmermann (Oct 26 2020 at 14:01):

So, the bot did not match your message with the expected regexp and I do not understand why.

view this post on Zulip Ralf Jung (Oct 26 2020 at 14:02):

my message first has an extra line of text before the @coqbot, but then I edited and later re-posted without that extra line

view this post on Zulip Ralf Jung (Oct 26 2020 at 14:03):

what is that regexp?

view this post on Zulip Théo Zimmermann (Oct 26 2020 at 14:03):

https://github.com/coq/bot/blob/90f0b8f7b5ef984291b13a691b9351341c2fc0d8/src/bot.ml#L177

view this post on Zulip Ralf Jung (Oct 26 2020 at 14:06):

[^```] is weird

view this post on Zulip Ralf Jung (Oct 26 2020 at 14:06):

it is the same as [^`]

view this post on Zulip Ralf Jung (Oct 26 2020 at 14:06):

and means "no ` anywhere in that text". we probably have a backtic for `{...}

view this post on Zulip Théo Zimmermann (Oct 26 2020 at 14:07):

Hum, yes indeed!

view this post on Zulip Théo Zimmermann (Oct 26 2020 at 14:09):

Any suggestion of how to fix this? Maybe the solution is simply not to use regexp for that kind of parsing...

view this post on Zulip Ralf Jung (Oct 26 2020 at 14:09):

using .* should usually work I think

view this post on Zulip Ralf Jung (Oct 26 2020 at 14:10):

you might want to consult the docs of your regex library to see which match it will pick in case of an ambiguity

view this post on Zulip Ralf Jung (Oct 26 2020 at 14:10):

but without the backtics the bot still does not respond...

view this post on Zulip Théo Zimmermann (Oct 26 2020 at 15:08):

FWIW, this one was correctly parsed.

view this post on Zulip Théo Zimmermann (Oct 26 2020 at 15:10):

There was a bug later on when pushing the branch to the run-coq-minimizer repo.

view this post on Zulip Théo Zimmermann (Oct 26 2020 at 15:10):

Obviously, this feature is under tested. It was virtually not used since it was introduced (even though it was tested when it was introduced).

view this post on Zulip Théo Zimmermann (Oct 26 2020 at 15:11):

I'll look into it tomorrow morning.

view this post on Zulip Ralf Jung (Oct 26 2020 at 15:11):

sure :) this is not a high-priority bug, it was more like "I am too lazy to minimize this by hand (and it seems quite annoying to do so), let's see what the bot can do"

view this post on Zulip Ralf Jung (Oct 26 2020 at 15:12):

so I am happy to just use this to debug the bot

view this post on Zulip Théo Zimmermann (Oct 26 2020 at 15:16):

Great then :grinning:

view this post on Zulip Ralf Jung (Oct 26 2020 at 17:16):

(I might be logged out of Zulip but email notifications work well, so please ping me if you want me to try again or so)

view this post on Zulip Notification Bot (Oct 27 2020 at 15:28):

This topic was moved here from #Coq users > coqbot minimize by Théo Zimmermann

view this post on Zulip Théo Zimmermann (Oct 27 2020 at 15:28):

Unfortunately, I didn't find the time yet to investigate further, but this is definitely on my TODO for this week.

view this post on Zulip Ralf Jung (Oct 30 2020 at 09:02):

Okay. I was just logging in to see what the status is. :)

view this post on Zulip Théo Zimmermann (Oct 31 2020 at 11:33):

That TODO list was quite shaken by the new lockdown in France :S

view this post on Zulip Ralf Jung (Nov 07 2020 at 08:46):

@Théo Zimmermann how that, shouldn't you have more time for research now? :P

view this post on Zulip Jason Gross (Nov 14 2020 at 01:02):

Any suggestion of how to fix this? Maybe the solution is simply not to use regexp for that kind of parsing...

Very belatedly, depending on what regex library you use (see https://stackoverflow.com/a/49311828/377022), you can use negative lookahead ((?!```))

view this post on Zulip Jason Gross (Nov 14 2020 at 01:05):

It's possible that something that I broke something when I adapted the minimizer runner to work with the (hopefully coming soon?) feature of automatically running the minimizer on PRs with failing CI jobs. (Btw, what's the status of coqbot support for this? Can I help make it happen sooner?)

view this post on Zulip Théo Zimmermann (Nov 14 2020 at 11:25):

Hello @Jason Gross, thanks for your help! I've spent some time working on other coqbot issues during the last two weeks. In particular, on improving the GitLab reports in the GitHub Checks tab. This is related to the auto-minimizing feature because I wanted to see if I could gather all the info I needed to retrieve for this feature and store it on the GitHub side. I need to spend some time on other stuff, but I will hopefully come back to these two minimizer-related questions on Thursday.


Last updated: Jan 31 2023 at 11:01 UTC