Where are we, from literature mode?

[ice1000]

trafficstars

Let me start: a syntax design for a suitable markup language. Obviously we need our own markup language :thinking: and we need to compile it in our Doc backends.

[re-xyr]

What about just use LaTeX?

[ice1000]

We will have our own commands, can't reuse any existing ones

[re-xyr]

Like what commands?

[ice1000]

Like what commands?

aya-prover/aya-prover-proto#486

[re-xyr]

We can make it look like some LaTeX macro

[ice1000]

@re-xyr But it's no good, incompatible with other backends of Doc

[re-xyr]

I don't quite understand. Are we doing a literate -> Doc -> output translation?

[ice1000]

I don't quite understand. Are we doing a literate -> Doc -> output translation?

Yup

[re-xyr]

But if we use LaTeX syntax, what's incompatible with LaTeX-like -> Doc -> other format?

[re-xyr]

Agda supports lagda.tex and lagda.md and lagda.rst etc. I think we just have to translate the parts in the code blocks to properly rendered code?

[ice1000]

But if we use LaTeX syntax, what's incompatible with LaTeX-like -> Doc -> other format?

Then we need to parse latex!

[re-xyr]

I mean, how does Agda support .lagda.tex?

[ice1000]

@re-xyr I think their approach is bad. We need to make our own backend generating latex.

[ice1000]

@re-xyr Agda asks you to write latex

[re-xyr]

I mean, we'll want to insert our code into different kinds of documents (html, latex, etc). How do we do that? Or we don't?

[ice1000]

@re-xyr Imagine we use markdown, where aya code interpolated into some markup text. Then we codegen to latex by compiling aya to latex code blocks and markup text to latex typeset code, codegen to html by compiling aya to html and markup text to html. Users can put some latex in the markup text, they'll be preserved to the generated text, which will be recognized by latex compilers (and ofc won't work if generating html)

[re-xyr]

So basically we allow foreign (html, latex) syntax in our own markup syntax.

[ice1000]

@re-xyr It'll be treated as plain text

[ice1000]

Agda supports lagda.tex and lagda.md and lagda.rst etc. I think we just have to translate the parts in the code blocks to properly rendered code?

This is actually a nice idea, but I wanna add some 私货 to the markup language itself

[ice1000]

Fixed!