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

Add support for restructured text (.rst) code blocks #1441

Closed
podhrmic opened this issue Sep 23, 2022 · 5 comments
Closed

Add support for restructured text (.rst) code blocks #1441

podhrmic opened this issue Sep 23, 2022 · 5 comments

Comments

@podhrmic
Copy link

An example below:

Lorem Ipsum
=========================

Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum

.. code-block:: cryptol

   R1 : {WIDTH} (fin WIDTH, WIDTH >= 2, WIDTH % 2 == 0) => [WIDTH/2-1] -> Integer
   R1 nhi = `(2^^WIDTH)

   R4 : {WIDTH} (fin WIDTH, WIDTH >= 2, WIDTH % 2 == 0) => [WIDTH/2-1] -> Integer
   R4 nhi = `(2^^(WIDTH+2))
@podhrmic
Copy link
Author

Use pandoc module.

@podhrmic
Copy link
Author

@yav closing as no longer relevant. .rst is a relatively complex format, so a simple parser similar to what we have for Markdown and Latex wouldn't cut it. A better way is probably to convert .rst code blocks to cryptol separately, and then directly load cryptol files.

@yav yav reopened this Sep 27, 2022
@yav
Copy link
Member

yav commented Sep 27, 2022

I think this would be a nice feature to have and extracting Cryptol code blocks from an RST really shouldn't be that hard. Can you say a bit more about what difficulties you envision?

@podhrmic
Copy link
Author

Of course. Here are the specs for the code-block directive in rst.

An example:

.. code-block:: cryptol
   :linenos:
   :dedent: 4

       some cryptol code
       
       some other cryptol code

Regular text here. Code block ended on the previous line.

The trick is you have to track the opening token .. code-block:: cryptol and correctly identify the ending newline. So probably some state tracking? Anyway, I agree that getting something that works shouldn't be that hard, but given my Haskell skills it is beyond the time I have available for this feature.

@yav
Copy link
Member

yav commented Sep 27, 2022

@podhrmic I implemented a simple RST pre-processor in PR #1443. Give it a go!

@yav yav closed this as completed Sep 28, 2022
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

No branches or pull requests

2 participants