Markdown code fence delimiting

[auricratio]

In 2.8 and 2.9 (at least), triple-backtick followed by cryptolcheese and presumably any line starting with triple-backtick cryptol acts as a fence and code within gets consumed by Cryptol's parser.

[weaversa]

For the class, we’d like to be able to differentiate between cryptol and cryptol-repl (or cryptol-interpreter).

[yav]

I am not sure if that's a bug or a feature, as the code is purposefully written to work that way, and either I didn't write the original or have forgotten the reasoning behind it :) It's easy enough to change, we should just decide how we'd like it to work.

I think it is useful to have something more than just cryptol though. For example, you may want to have some "boring" bits of code be hidden in the document, but cryptol still needs them to load the file. So you could use cryptol-boring as the fence, and then filter that before generating the final document. Another variation is exercises of the form "write a function that does X", you may want to have the answer in the document, but hide it before generating the questions for the students.

So maybe allowing any string starting with cryptol to be a Cryptol fence is actually useful?

@weaversa are you suggesting that it'd be nice to have a different code block that would contain Cryptol REPL commands, and would be interpreted differently while loading? If so, I think that's a very interesting idea, but maybe we should make a separate ticket to workout exactly how it should work (e.g., when should the commands be loaded, do we want to capture their output in some way, etc.). I've been thinking along the same lines for the Cryptol book, which always gets out of date, so it'd be nice to have some tooling help with that issue.

[auricratio]

While we're discussing it, I also noticed that Markdown and Cryptol both being layout sensitive leads to some interesting interaction.

My first thought is that fenced code that is indented/quoted in Markdown should be unindented by the Markdown's indentation level when consumed by Cryptol.

So in the Markdown a list item containing some code (using periods for spaces)

*.```cryptol
..private
......benke.x.=.x
..``` 

should parse as:

private
....benke.x.=.x

Trickier if it's a quoted item with code:

>.```cryptol
>.private
>.....benke.x.=.x
>.``` 

but I'd expect the same parse.

Truthfully, I'm not certain whether there's a good answer since Markdowns are mostly ill-defined, but I suppose we have some hope since GitHub Flavored Markdown has a somewhat rigorous definition.

[auricratio]

Looking at the GFM spec, it says

An info string can be provided after the opening code fence. Although this spec doesn’t mandate any particular treatment of the info string, the first word is typically used to specify the language of the code block.

which means we could have:

```cryptol code
```shell cryptol commands
```shell cryptol session 

etc., the first word directing the formatting in markdown and the others being hints to the reader and/or test runner.

[WeeknightMVP]

Given that shell is currently registered for shell scripts in Linguist (GitHub's GFM syntax highlighter) and renders Cryptol REPL goofily, perhaps leading with cryptol and defining different space-delimited modes would make sense. For Python, for example, languages.yml defines modes for (EDIT: Python console) and Python traceback in addition to the language Python.

[auricratio]

I was thinking that Cryptol would parse exactly those fences that started with ```cryptol followed by a space or newline and would begin parsing on the next line. Obviously there are several uses cases to reconcile...

[auricratio]

So we want the fence info string to do several things:

1. Delimit code to be formatted prettily in Markdown.
2. Delimit code to be parsed by Cryptol.
3. Help the reader understand the category of the fenced code.
4. Delimit code to be processed by automated tools, perhaps subdivided into:
   • rapid tests that we want run as part of CI
   • slower tests that we would run on some schedule (nightly, weekly)

Are there others?

[WeeknightMVP]

One minor distinction is REPL vs. batch output, e.g. batch mode adds Testing... and Satisfiable for :sat responses. (Is this intended?)

[auricratio]

One minor distinction is REPL vs. batch output, e.g. batch mode adds "Testing..." and "Satisfiable" for :sat responses. (Is this intended?)

@WeeknightMVP could you elaborate on this, I'm not following you.

[WeeknightMVP]

@auricratio So of course I don't get the same results running another version of Cryptol...

When I run cryptol -b <script>.icry with a newer Cryptol version from docker image cryptolcourse/cryptol, the batch output adds Testing... and Satisfiable to whatever the interpreter would have displayed in response to a successful :sat <property> command running in the REPL. But Cryptol 2.8.1 from about a year ago does not.

[WeeknightMVP]

...and in the Cryptol version I just built from source today, both the interpreter and batch mode output Satisfiable, but not Testing..., so it looks like the behavior is based on Cryptol versions and not REPL vs. batch mode. I retract my earlier comment.

[yav]

Could someone summarize what we may want to add/change to satisfy this ticket?

[weaversa]

Well, how about we follow Frank’s suggestion:

I was thinking that Cryptol would parse exactly those fences that started with ```cryptol followed by [whitespace] and would begin parsing on the next line.

Then we leave REPL parsing for CI, etc. to be worked out by other tools. This would allow Markdown fences to start with ‘cryptol’ and then include modifiers that other tools could key on.

[yav]

@weaversa That's less flexible that what we currently have, and will disallow the use cases I mentioned in https://github.com/GaloisInc/cryptol/issues/857#issuecomment-668690850 How would you write a literate Cryptol document where you'd like to hide some of the definitions?

Isn't a rather simple solution to the original issue to simply use cryptol and repl-cryptol?

[weaversa]

🤷

Many of the Cryptol course students were new to Markdown and didn't understand that their were different types of code fences. We had lots of questions about why typing import labs::Language::Basics into the interpreter threw an error. We were hoping to add a little more semantic meaning to the code fences by having cryptol interpreter (or something similar) rather than shell to help the students see that some code fences were for typing and and some were for commands that go into the interpreter.

We ended up adding a rather large paragraph at the top of every lab which seems to have fixed the issue the students were having.

I'm not opposed to just leaving things as they are.

I do think it's worthwhile to explore how to integrate tooling to help catch inconsistent interpreter output (like you said, for the Cryptol book).

[brianhuffman]

Just now I was trying to put a pre-formatted ascii-art diagram into a literate cryptol markdown file. I had been marking all my cryptol code sections with ```cryptol, under the assumption that the cryptol bit was required. But then cryptol gave a parse error because it was trying to parse my diagram (which was marked with plain ```) as cryptol source code. Is this intentional?

Fortunately I discovered a workaround, which is to add a meaningless info string to the triple-backtick for the non-cryptol preformatted text.

[yav]

@brianhuffman At present we consider a markdown code segment to be Cryptol code if:

• it does not have a specified language (wihch is what you encountered), or
• the language is some string starting with cryptol

The code as written is clearly on purpose (i.e., not an unintentional bug), but I don't have a strong opinion on how it should work as this is not a feature I use a lot: https://github.com/GaloisInc/cryptol/blob/07c689a699a7e2508da51bb22f63b0d3667ac15d/src/Cryptol/Parser/Unlit.hs#L103

I do kind if like that unspecified code is treated as cryptol though, as having to write cryptol all the time in a cryptol file seems a bit odd.

[brianhuffman]

Well, the important thing to me is that I'm able to have a markdown file with some cryptol code blocks and some other preformatted text blocks that are not cryptol. And I can do that, although it wasn't obvious to me at first how to do it.

The main action item, I think, is to document the .md literate cryptol feature. Currently the Programming Cryptol book only has a few sentences in an appendix about literate cryptol, and it only mentions .tex files; markdown is not mentioned at all. We need to describe how to put a cryptol code block in a markdown file, and we should also mention the possibility of non-cryptol code blocks.

[weaversa]

Well, the important thing to me is that I'm able to have a markdown file with some cryptol code blocks and some other preformatted text blocks that are not cryptol.

@brianhuffman I want this too, for Cryptol and SAW -- https://github.com/GaloisInc/saw-script/issues/1408