Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Allow customization of Coq version #252

Merged
merged 4 commits into from
Nov 21, 2022
Merged

Allow customization of Coq version #252

merged 4 commits into from
Nov 21, 2022

Conversation

JasonGross
Copy link
Member

Not entirely clear what the protocol should be, see also #183. We
currently allow things like coq-8.14 and coq.dev and coq: dev and
ocaml: 4.11, etc.

@JasonGross
Copy link
Member Author

JasonGross commented Nov 17, 2022 •
edited
Loading

This is deployed and worked correctly at coq/coq#16834 (comment)

Edit: The deployment had failed, and it was not working correctly

@Zimmi48 thoughts on merging?

@JasonGross
Copy link
Member Author

This apparently results in a 500 "Error: Internal Server Error" with no log info printed on comments like the one below. @Zimmi48 Can you help debug? (I've undeployed this for now)

@coqbot minimize coq.dev

true | coqtop
opam install -y coq-fiat-crypto.dev

@Zimmi48
Copy link
Member

Zimmi48 commented Nov 18, 2022

OK, I will have a look today.

@Zimmi48
Copy link
Member

Zimmi48 commented Nov 18, 2022

Something happened that made the bot crash. The log says: Process exited with status 143.
Have you observed this pattern of crashing repeatedly?
It's a very surprising behavior, maybe an OOM issue?

@JasonGross
Copy link
Member Author

I have not observed it (and did not see such messages in the log), but let me try splitting up the commit into the OCaml part and the bash part, maybe that will reveal what's going on more clearly. (Though if this only happened about 5 minutes ago, that might be a race condition from me merging #251 or #253 and a redeploy happening?)

@JasonGross
Copy link
Member Author

On the other hand I currently see
image
when I click on logentries

@JasonGross
Allow customization of Coq version in coq_bug_minimizer.sh
9ac8fcf 
Support is not yet hooked up in the OCaml code.
@JasonGross
Copy link
Member Author

I've split this PR into two commits, one for just the bash change and one for the OCaml change, I'm now trying the deploy of just the bash one

@JasonGross
Copy link
Member Author

Bash-only commit seems to be working at coq-community/run-coq-bug-minimizer#2 (comment)

@JasonGross
Copy link
Member Author

Is it possible that OCaml doesn't like multiple string_match on the same string? (Something with mutation?)

@JasonGross
Copy link
Member Author

I see the 143 error only on redeploy. I continue to see Error: Internal Server Error to the minimize comments while also seeing normal things like Unhandled comment: coqbot merge now

JasonGross
JasonGross commented Nov 18, 2022
View reviewed changes
src/bot.ml Outdated
Comment on lines 65 to 66
( Str.matched_group 1 body
, Str.matched_group 2 body |> extract_minimize_file )
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The issue seems to be this pair of lines. Maybe extract_minimize_file messes things up in a way that Str.matched_group 1 body fails? (Does OCaml evaluate tuples right-to-left?)

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

tuple evaulation order is undefined afaik

@Alizter
Copy link
Contributor

Alizter commented Nov 18, 2022 •
edited
Loading

Try writing an expect test to test out your regex.

Example in here: #240

You can do dune build @runtest --auto-promote -w to run Dune in the background and update the tests as you modify the code.

@JasonGross
Allow customization of Coq version
e9ccb72 
Not entirely clear what the protocol should be, see also coq#183.  We
currently allow things like `coq-8.14` and `coq.dev` and `coq: dev` and
`ocaml: 4.11`, etc.
@JasonGross
Avoid issue with string matching evaluation order
383c157
@Zimmi48
Copy link
Member

Zimmi48 commented Nov 18, 2022

On the other hand I currently see image when I click on logentries

I've seen this once but it worked when I immediately retried.

@JasonGross
Copy link
Member Author

Seems to be working now at https://github.com/coq-community/run-coq-bug-minimizer/actions/runs/3500541795/jobs/5863316068 / coq-community/run-coq-bug-minimizer#2 (comment)

@JasonGross
Copy link
Member Author

Seems to be working pretty well. Thoughts on merging @Zimmi48 ?

@Zimmi48
Copy link
Member

Zimmi48 commented Nov 21, 2022

I'm not in a state where I can properly review the PR but if you think this is sufficiently tested (including the case with no argument), then I'm fine with merging. I would just note that it looks like we are starting to grow a language of commands to coqbot and it would be preferable if we try to design this language consistently. It was decided in a Coq Call (then reported as an issue here #250, but not yet implemented) that @coqbot bench native should become @coqbot bench native=on. This suggests that this command could take options as @coqbot minimize coq=... ocaml=.... WDYT?

@JasonGross
Copy link
Member Author

It was decided in a Coq Call (then reported as an issue here #250, but not yet implemented) that @coqbot bench native should become @coqbot bench native=on. This suggests that this command could take options as @coqbot minimize coq=... ocaml=.... WDYT?

I've added support for coq=... and ocaml=..., and allowed users to specify versions as 8.16, also v8.16, also V8.16 (they are treated identically). I didn't feel like specifically forbidding vdev and Vdev, so these also work. I've left in other ways of specifying things, like coq:8.16 and coq: 8.16 and coq.8.16 and coq-8.16. I figure it's better to be generous in parsing the user's intent here, even if we only advertise one way of doing things.

@JasonGross
Copy link
Member Author

Seems to work both with and without versions at coq-community/run-coq-bug-minimizer#2 (comment), I'll merge

@JasonGross JasonGross merged commit adea26c into coq:master Nov 21, 2022
@JasonGross JasonGross deleted the minimize-coq-version branch November 21, 2022 18:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@SkySkimmer SkySkimmer SkySkimmer left review comments

@Zimmi48 Zimmi48 Awaiting requested review from Zimmi48

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@JasonGross @Zimmi48 @Alizter @SkySkimmer