Skip to content

Avoid discarding any docstring comments #1664

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

Merged
merged 3 commits into from
Jun 3, 2024
Merged

Avoid discarding any docstring comments #1664

merged 3 commits into from
Jun 3, 2024

Conversation

glguy
Copy link
Member

@glguy glguy commented May 17, 2024

  • include, import, and type constraint docstrings are now preserved
  • parameter and private block docstrings are not supported

@glguy glguy temporarily deployed to github-pages May 17, 2024 21:32 — with GitHub Actions Inactive
@glguy glguy marked this pull request as draft May 17, 2024 21:42
@RyanGlScott
Copy link
Contributor

Thanks for the PR, @glguy!

I realize that this is still a draft, but when you get a chance, could you open an issue describing what problem you are trying to solve? (If you can include one or two test cases showing what goes wrong with Cryptol's current behavior, all the better.) That way, this PR can reference the issue and provide better traceability into why we need to make the changes here.

@glguy glguy force-pushed the remember-docstrings branch from 7bb618d to 1718b10 Compare May 20, 2024 17:39
@glguy glguy temporarily deployed to github-pages May 20, 2024 17:39 — with GitHub Actions Inactive
@glguy glguy temporarily deployed to github-pages May 20, 2024 20:56 — with GitHub Actions Inactive
@glguy glguy marked this pull request as ready for review May 20, 2024 20:59
@glguy glguy requested a review from yav May 21, 2024 21:16
@yav
Copy link
Member

yav commented Jun 1, 2024

@glguy do you think there's any reason to allow doc comments on imports/includes? We can't really refer to them easily, and they don't really seem to be part of the API of a module... I haven't looked carefully, but my guess is that they were there in the first place to avoid ambiguities in the grammar---I am thinking it might be easier to just report an error instead of saving them.

@glguy
Copy link
Member Author

glguy commented Jun 1, 2024

I tracked them because they were there. I think it might make more sense not to allow them, however.

Int place I could imagine them making sense is if you wanted to assert something about the way you instantiated a parameterized module because you're relying on properties if it specific to your instantiation. Is that plausible?

@yav
Copy link
Member

yav commented Jun 2, 2024

I think we should make them an error, and keep the AST simpler. I think if you wanted to say something about instantiation you should probably do it where you define the instantiation. Which reminds me that we may want to allow doc comments at the top of a module, to say what the module is for (we don't have to do it in this PR though)

@glguy glguy temporarily deployed to github-pages June 3, 2024 15:46 — with GitHub Actions Inactive
glguy added 3 commits June 3, 2024 10:09
* include, import, and type constraint docstrings are now preserved
* parameter and private block docstrings are not supported
@glguy glguy force-pushed the remember-docstrings branch from 661bbc7 to 1009680 Compare June 3, 2024 17:09
@glguy glguy temporarily deployed to github-pages June 3, 2024 17:09 — with GitHub Actions Inactive
@glguy glguy merged commit 20d88b8 into master Jun 3, 2024
45 checks passed
@glguy glguy deleted the remember-docstrings branch June 3, 2024 20:53
RyanGlScott added a commit to GaloisInc/saw-script that referenced this pull request Jul 19, 2024
This bumps the `cryptol` submodule to bring in the changes from
GaloisInc/cryptol#1664. This requires some minor code changes in
`cryptol-saw-core` to adapt to the `Import` data constructor now having an
`iDoc :: Maybe (Located Text)` field to represent docstrings. None of the
`Import`s that `cryptol-saw-core` generates require any docstrings, so it
suffices to instantiate them with `Nothing`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants