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?
hm, maybe the @coqbot
needs to be the first thing in the comment?
no that does not seem to change anything
@Théo Zimmermann any advice? :D
Yes, I think that the bot should answer something. Let me see...
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
So, the bot did not match your message with the expected regexp and I do not understand why.
my message first has an extra line of text before the @coqbot
, but then I edited and later re-posted without that extra line
what is that regexp?
https://github.com/coq/bot/blob/90f0b8f7b5ef984291b13a691b9351341c2fc0d8/src/bot.ml#L177
[^```]
is weird
it is the same as [^`]
and means "no `
anywhere in that text". we probably have a backtic for `{...}
Hum, yes indeed!
Any suggestion of how to fix this? Maybe the solution is simply not to use regexp for that kind of parsing...
using .*
should usually work I think
you might want to consult the docs of your regex library to see which match it will pick in case of an ambiguity
but without the backtics the bot still does not respond...
FWIW, this one was correctly parsed.
There was a bug later on when pushing the branch to the run-coq-minimizer repo.
Obviously, this feature is under tested. It was virtually not used since it was introduced (even though it was tested when it was introduced).
I'll look into it tomorrow morning.
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"
so I am happy to just use this to debug the bot
Great then :grinning:
(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)
This topic was moved here from #Coq users > coqbot minimize by Théo Zimmermann
Unfortunately, I didn't find the time yet to investigate further, but this is definitely on my TODO for this week.
Okay. I was just logging in to see what the status is. :)
That TODO list was quite shaken by the new lockdown in France :S
@Théo Zimmermann how that, shouldn't you have more time for research now? :P
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 ((?!```)
)
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?)
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: Oct 13 2024 at 01:02 UTC