Stream: VsCoq devs & users

Topic: TeX in VScoq

view this post on Zulip Brandon Sisler (Dec 22 2022 at 00:24):

Hey all, I was wondering if there was any way to use symbols as I would in TeX in a Coq file (note, I am not trying to just have my finished file have the symbols I want, I want specifically to type them, and see them in the file as I create it). Lean 3 comes to mind in terms of what I want to be able to do. In that I can type something like \Pi, and have it be replaced by that symbol.

view this post on Zulip Huỳnh Trần Khanh (Dec 22 2022 at 02:54):

You would need to patch VsCoq for that. If there are many folks who want this feature, we could implement it.

I'm an ex-Lean user. So far I haven't needed to type Unicode symbols in Coq because the ecosystem sticks to plain ASCII symbols. But if the community wants this feature, I'm willing to implement it.

view this post on Zulip Paolo Giarrusso (Dec 22 2022 at 05:38):

There are already multiple Unicode Input extensions in the marketplace.. https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/editor.md#unicode-input-setup links to a configurable one with an example of configuration

view this post on Zulip Bas Spitters (Dec 22 2022 at 07:37):

jscoq does some beautiful things, @Emilio Jesús Gallego Arias probably has good insights on how to do literate proving across vscoq and jscoq. Or knows what the problems are...
I'm not sure whether markdown could be a complete replacement for tex/html which is currently used in coqdoc.
https://coq.zulipchat.com/#narrow/stream/256336-jsCoq/topic/Coqdoc.20as.20Html.20in.20ScratchPad.3F/near/309012814

view this post on Zulip Théo Winterhalter (Dec 22 2022 at 09:55):

We had discussions like this in the past, the last being https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs-.26-users/topic/inputting.20UTF8.20symbols also you can use unicode notations in Coq by importing the UTF8 package.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 22 2022 at 11:51):

@Bas Spitters , indeed we are close to release new jsCoq version that will be "pure" literate, you can already input coq Markdown files in vscode using coq-lsp, but the schema is very basic.

Internally, we use a "schema", that is close to MyST Markdown , there is indeed the possibility to use TeX documents directly but I haven't looked into what TeX parser woud allow that. I would expect that format to replace coqdoc, but OMMV

Last updated: Jun 04 2023 at 22:30 UTC