Literate cryptol parser not permissive enough

[benjaminselfridge]

I have a literate Cryptol markdown document that uses the following syntax:

```{.cryptol}
<code here>

However, Cryptol only accepts

```cryptol

I suggest we add a case to cover the former syntax, since it's standard and is produced by pandoc in most cases.

[RyanGlScott]

I wasn't aware of this before looking it up: this is an extension to Pandoc's particular flavor of markdown called fenced_code_attributes. This is a pretty powerful feature in general, as it lets you write things like this:

``` {#mycode .haskell .numberLines startFrom="100"}
qsort []     = []
qsort (x:xs) = qsort (filter (< x) xs) ++ [x] ++
               qsort (filter (>= x) xs)
```

I suppose that if we wanted to support this feature in its full generality, we would need to scan for any occurrence of .cryptol within a set of open-close curly braces that appear after the opening ```. Then again, simply recognizing ```{.cryptol} might also suffice.

[benjaminselfridge]

I also think there may be a way to just tell pandoc to generate

```cryptol

instead. If that is possible, it might be a better solution for what I need.

[benjaminselfridge]

Fun -- with -t commonmark-fenced_code_attributes, I can get it to output

``` cryptol

with a space before cryptol. So I am submitting a small patch to Cryptol to strip the whitespace there before checking if the string is equal to cryptol.

[RyanGlScott]

Resolved in #1502.

[benjaminselfridge]

I have hit enough new issues with pandoc that I now believe the correct approach is to simply see if "cryptol" appears anywhere on the line. I'm getting all sorts of crazy stuff from different versions of pandoc with different command line args.

[yav]

Can you say a bit more about what your use case it? I am asking because it sounds like you are using pandoc to generate markdown, which is backward from the usual use cases. Treating every line that contains cryptol somewhere in it as code that Cryptol should interpret seems too permissive.

[benjaminselfridge]

Sure -- depending on the version of pandoc I'm using, I sometimes get

``` {.sourceCode .cryptol}

or sometimes

``` sourceCode cryptol

Or some other variation. Is it too permissive to have the criteria be "starts with three backticks and contains the substring 'cryptol'"?

[yav]

I understand that pandoc is generating markdown in some way, but I was wondering why the markdown is being generated in the first place, rather than being written by hand, which is the usual purpose of markdown.

What you want is too permissive, because it prevents us from supporting Cryptol related environments that should be rendered but not interpreted by Cryptol.

I don't mind changing what we do to support your use case, I just think we need to come up with something a bit more structured than just having "cryptol" somewhere in there.

[benjaminselfridge]

Makes sense. The original documents are in restructured text format, and we're using pandoc to translate to markdown. I can't remember why, but I'm pretty sure that Cryptol doesn't unlit the rst the way we want. Now that I think of it, I probably should double check that before complaining more here. Let me close this issue again and I'll reopen if needed.