Deploying Tactician on JsCoq v8.17+lsp

[LasseBlaauwbroek]

I'm happy to report that I've successfully updated the online demo of Tactician to v8.17+lsp (to be deployed soon, not online yet).
This is actually the only version of JsCoq where I can get things to work. I cannot get older versions of JsCoq (that I used previously) to build, and the latest v0.17.1 throws STM related errors while Tactician is loaded.

Great success I'd say. Regardless, here are some questions about the rough edges:

• The message pane is overflowing with stderr: Queue length: 32 output, and some other stderr messages as well. Is this useful? Can we get rid of it?
• What is the intent of the new markdown editor? Is the idea that the markdown will be rendered eventually? (I see in the code that the markdown is being parsed by coq-lsp internally.) In its current state I'd say that the "literate programming" presentation is in a slightly worse state than that it used to be.

[ejgallego]

That's fanstastic, thanks for the feedback! We have indeed done a lot of not very rewarding work trying to make the setup easier. I can see the STM problems you had, unfortunately these are not possible to workaround, that's why we wrote Flèche / coq-lsp.

The message pane is overflowing with stderr: Queue length: 32 output, and some other stderr messages as well. Is this useful? Can we get rid of it?

Absolutely, this is debug code. Note that the official releases still use the old method, but the main dev branch is based on the new tech.

There is actually a couple of blocking issues to make a release of jsCoq with the LSP backend (related to interruptions and Javascript workers), also there is a few missing features in the LSP server such as the EnvUpdate call, but we are almost there.

What is the intent of the new markdown editor? Is the idea that the markdown will be rendered eventually? (I see in the code that the markdown is being parsed by coq-lsp internally.) In its current state I'd say that the "literate programming" presentation is in a slightly worse state than that it used to be.

Indeed, by default you can see this markdown editor, but we also support the older mode.

I was not expecting people to use this branch yet, so thanks for the report, I'll try to clean up the branch next week to resolve your issues.

[LasseBlaauwbroek]

Yeah, I wasn't really planning on using this branch. But the other branches were broken for me, so I was left with this.
Do you mind if I deploy it, even if it is not in a perfectly polished state?

but we also support the older mode.

How do I do that?

[ejgallego]

I don't mind at all, but keep in mind that if interrupts are broken in JS, checking large files will be annoying.

How do I do that?

With the current branch you need to pass the ?frontend=cm5&content_type=plain (or set them in the .html file), then you do as before, an example https://pastebin.com/Vf7ipApy

I see that showing the goals is broken for other snippets tho, that should be a very easy fix (we forgot to add the snippet-specific offset)

[LasseBlaauwbroek]

Thanks. (I noticed the interrupt issue, but it is just a small demo, so people will have to live with it.)

[ejgallego]

Thanks to you for the feedback, now that we have users of the new jsCoq 2.0 branch we'll try to fix these issues ASAP.

[LasseBlaauwbroek]

Note that the Tactician demo is online here: https://coq-tactician.github.io/demo.html

One additional issue I'm noticing is that the green navigation buttons don't do anything now that navigation is done by the cursor. This might be confusing to viewers.