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

Initial implementation of :check-docstrings #1682

Merged
merged 12 commits into from
Jul 18, 2024
Merged

Initial implementation of :check-docstrings #1682

merged 12 commits into from
Jul 18, 2024

Conversation

glguy
Copy link
Member

@glguy glguy commented Jun 6, 2024

No description provided.

@glguy glguy marked this pull request as ready for review June 28, 2024 18:10
@glguy glguy changed the title Update all commands to track their results Initial implementation of :check-docstrings Jun 28, 2024
@RyanGlScott
Copy link
Contributor

Could you write some documentation that describes how :check-docstrings works at a high level? The Cryptol reference manual might be one place to put this documentation, but if there isn't a good place in the manual to put it, even including the comments as just Haddocks would be nice. In particular, I think we should make note of things such as:

  • What syntax :check-docstrings is looking for?
  • Can docstrings live in any type of comment, or can they only belong to certain types of code blocks?
  • What are the conditions under which this command will succeed or fail?
  • Are the docstring blocks run in a particular order? If not, the documentation should say that this is unspecified so that we are free to change the order.

Some test cases that exercise the functionality of :check-docstrings would also be appreciated.

@sauclovian-g
Copy link
Contributor

If there isn't a place in the manual to put it, feel free to stick it in an appendix marked something like "Additional notes to be merged", create another issue for sorting it out properly, and assign that to me. There should be a place for everything in the manual.

glguy added 3 commits July 8, 2024 08:51
@glguy
Update all commands to track their results
ad5af8b
@glguy
Implement REPL :check-docstrings command
b2ce820 
This command checks that all of the unlabeled and "repl" labeled
codeblocks in docstrings can successfully evaluate as REPL commands.

Cryptol will now indicate exit failure if any of REPL commands fail,
making it possible to use in automated testing.

:check-docstrings internal implementation is set up to track results
of subcommands in support for integration into a remote server API
endpoint.
@glguy
Implement :focus
72902bd
This was referenced Jul 9, 2024
Open
Open
@weaversa weaversa mentioned this pull request Jul 11, 2024
Open
yav
yav approved these changes Jul 18, 2024
View reviewed changes
Copy link
Member

@yav yav left a comment

Choose a reason for hiding this comment

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

Looks good to me.

@glguy glguy merged commit 4ca0629 into master Jul 18, 2024
48 checks passed
@glguy glguy deleted the command-results branch July 18, 2024 22:44
RyanGlScott added a commit to GaloisInc/saw-script that referenced this pull request Jul 19, 2024
@RyanGlScott
Bump cryptol submodule to bring in changes from GaloisInc/cryptol#1682
f513938 
This bumps the `cryptol` submodule to bring in the changes from
GaloisInc/cryptol#1682, which does not require any other code changes on the
SAW side.
@RyanGlScott RyanGlScott mentioned this pull request Jul 19, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sauclovian-g sauclovian-g sauclovian-g left review comments

@yav yav yav approved these changes

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
@glguy @RyanGlScott @sauclovian-g @yav