search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
137 stars 31 forks source link

[fleche] Support .tex literate documents #727

Closed ejgallego closed 2 months ago

ejgallego commented 2 months ago

Similarly to .mv files, we recognize .lv files to be LaTeX files with embedded Coq snippets, delimited by begin/end pairs.

To have some Coq code recognized inside a .lv or a .v.tex file do:

\begin{coq}
\end{coq}

Some tweaks to this scheme will be likely needed, for example I'm unsure the .lv extension will work in practice; suggestions welcome!

Alizter commented 2 months ago

Why not just recognize .tex files?

ejgallego commented 2 months ago

Why not just recognize .tex files?

Seems a bit heavy or intrusive to me to start the coq-lsp server for all .tex files, but indeed I'm open to do this based on user feedback.

Alizter commented 2 months ago

Right, I see why you wouldn't want that now. I'm thinking that latex tools won't work well with other file extensions. They generally all expect to see .tex. But as long as this is configurable this should be ok.

ejgallego commented 2 months ago

Right, I see why you wouldn't want that now. I'm thinking that latex tools won't work well with other file extensions. They generally all expect to see .tex. But as long as this is configurable this should be ok.

Yes, maybe we can change this to .v.tex for now?

ejgallego commented 2 months ago

Indeed I had already trouble using .lv but I like that idea, so I'll update the PR so both .lv and .v.tex work.