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.

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

[DOC-81] Update "Managing Timeouts" Section #159

Merged
merged 33 commits into from
Nov 21, 2023
Merged

Conversation

alexandernutz
Copy link
Contributor

@alexandernutz alexandernutz commented Oct 18, 2023

Towards a new and revised "Managing Timeouts" section.

Notes:

  • some sub-sections, or related sections are only stubs; to be done in future PRs (mostly the section on TAC reports)

Jira ticket: https://certora.atlassian.net/browse/DOC-345
Link to generated documentation: https://certora-certora-prover-documentation--159.com.readthedocs.build/en/159/docs/user-guide/timeouts/index.html

@alexandernutz alexandernutz added the existing feature new documentation for an existing feature label Oct 18, 2023
@alexandernutz alexandernutz changed the title Alex/timeouts update Update "Managing Timeouts" Section Oct 18, 2023
@alexandernutz alexandernutz requested a review from jar-ben October 19, 2023 10:04
@alexandernutz alexandernutz marked this pull request as ready for review October 19, 2023 10:04
@alexandernutz alexandernutz requested a review from a team as a code owner October 19, 2023 10:04
Copy link
Contributor

@jar-ben jar-ben left a comment

Choose a reason for hiding this comment

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

Some comments/suggestions :)

docs/user-guide/timeouts/index.md Outdated Show resolved Hide resolved
docs/user-guide/timeouts/timeouts-main.md Outdated Show resolved Hide resolved
docs/user-guide/timeouts/timeouts-main.md Outdated Show resolved Hide resolved
docs/user-guide/timeouts/timeouts-main.md Outdated Show resolved Hide resolved
docs/user-guide/timeouts/timeouts-main.md Outdated Show resolved Hide resolved
docs/user-guide/timeouts/timeouts-main.md Show resolved Hide resolved
docs/user-guide/timeouts/timeouts-main.md Outdated Show resolved Hide resolved
docs/user-guide/timeouts/timeouts-main.md Outdated Show resolved Hide resolved
docs/user-guide/timeouts/timeouts-theory.md Outdated Show resolved Hide resolved
docs/user-guide/timeouts/timeouts-theory.md Outdated Show resolved Hide resolved
Copy link
Contributor

@mdgeorge4153 mdgeorge4153 left a comment

Choose a reason for hiding this comment

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

This is excellent work, I'm very excited that we're adding it.

I think my main high-level comment is that the guide could be more directive. I expect that the primary use case for the guide is someone has a timeout and wants to know what to do next. So I think more information in the diagnosis sections about how to concretely tell which kind of timeout you have, with forward links to the sections that describe how to resolve them.

Similarly, there's several places where we say "you can summarize ..." but we haven't really explained what that is or how to do it. I think that information probably belongs on its own page somewhere in this section. Writing it is maybe beyond the scope of this PR, but maybe putting in a placeholder with a paragraph or two would be good.

I think this section would really benefit from examples, but I know constructing timeout examples is hard. Maybe you could work with Sitvanit, who is putting together examples for other CVL features.

docs/prover/diagnosis/index.md Outdated Show resolved Hide resolved
docs/prover/techniques/index.md Show resolved Hide resolved
docs/prover/diagnosis/index.md Outdated Show resolved Hide resolved
docs/prover/diagnosis/index.md Outdated Show resolved Hide resolved
docs/prover/diagnosis/index.md Show resolved Hide resolved
docs/user-guide/timeouts/timeouts-theory.md Outdated Show resolved Hide resolved
docs/user-guide/timeouts/timeouts-theory.md Show resolved Hide resolved
docs/user-guide/timeouts/timeouts-theory.md Show resolved Hide resolved
spelling_wordlist.txt Outdated Show resolved Hide resolved
spelling_wordlist.txt Outdated Show resolved Hide resolved
@mdgeorge4153 mdgeorge4153 changed the title Update "Managing Timeouts" Section [DOC-81] Update "Managing Timeouts" Section Oct 31, 2023
@alexandernutz
Copy link
Contributor Author

I think my main high-level comment is that the guide could be more directive. [...]

Points taken -- I think they all make sense, I plan to work on this page more in the future, and will try to drive things in that direction. (For this PR I hope that it can establish some basic concepts that the more practical instructions can build on .. and have some first shot at practical items ..)

docs/user-guide/glossary.md Show resolved Hide resolved
docs/user-guide/glossary.md Show resolved Hide resolved
docs/user-guide/glossary.md Outdated Show resolved Hide resolved
docs/user-guide/glossary.md Outdated Show resolved Hide resolved
docs/user-guide/glossary.md Outdated Show resolved Hide resolved
docs/user-guide/timeouts/timeouts-main.md Outdated Show resolved Hide resolved
docs/user-guide/timeouts/timeouts-main.md Show resolved Hide resolved
docs/user-guide/timeouts/timeouts-main.md Show resolved Hide resolved
@alexandernutz
Copy link
Contributor Author

Heads-up:
I'll land this one tomorrow if no one objects -- so if any of the reviewers (@mdgeorge4153 , @jar-ben , @shoham-certora ) thinks there is something still in here that absolutely should not enter our documentation, please let me know.

@alexandernutz alexandernutz dismissed mdgeorge4153’s stale review November 21, 2023 10:07

I think we discussed everything, to a sufficient extent -- and I'd like to land this :-) ... -- I can change always things in another PR of course

@alexandernutz alexandernutz merged commit 9a2ea86 into master Nov 21, 2023
@alexandernutz alexandernutz deleted the alex/timeouts-update branch November 21, 2023 13:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
existing feature new documentation for an existing feature
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants