Proposal for updating the user interfaces page. #218
Conversation
There was a problem hiding this comment.
Thanks a lot for this update, I think it is a much-needed improvement.
FWIW, the current URL for ProofWeb is broken. Here is one that works: http://carol.dimap.ufrn.br/proofweb/
There also seems to be an issue with the ProofEditor website. Perhaps we could link to the paper instead? http://www-sop.inria.fr/everest/Julien.Charles/papers/08-08-08-uitp.pdf (or remove this item).
| <p> | ||
| Both provides the ability of continuous and asynchronous document | ||
| checking as well as position-based document navigation (an | ||
| interaction model introduced in Wenzel's Isabelle/JEdit which |
There was a problem hiding this comment.
It might be worth mentioning that VsCoq2 also supports switching to a legacy-style mode of interaction if it doesn't make the text too long.
There was a problem hiding this comment.
What about "Both provides the extra ability ..."? (In the case of coq-lsp, afaiu, the server supports evaluation to a chosen position but the client does not - yet? - give access to it.)
There was a problem hiding this comment.
IMO, what the users most care about is what is accessible for the client. But OK to me if you do not want to make a comparison here.
There was a problem hiding this comment.
IIUC, Emilio is not fully convincent that it is worth to support the PG mode and this is why the client is bridled. I temporarily wrote "Both servers provides the extra ability" until it is clear what is the intent of coq-lsp developers.
There was a problem hiding this comment.
OK for now, but if coq-lsp doesn't support the legacy mode on purpose, it will be important to make the distinction when we start to advertise these two options more.
There was a problem hiding this comment.
I still don't see it. But I'm fine with the current state FWIW.
There was a problem hiding this comment.
Ah OK, my mistake. I understand what you meant now.
There was a problem hiding this comment.
OK for now, but if coq-lsp doesn't support the legacy mode on purpose, it will be important to make the distinction when we start to advertise these two options more.
Technically coq-lsp does support checking to a point, and indeed it uses internally in an essential way (for example the way click to show goals works today is exactly like that)
The reason I didn't put an option for that is that 0 users do prefer the old mode, which has pretty bad latency properties. However there is a chicken and egg design problem here, in the sense that once you are used to the more eager mode, you never want to go back. Design in this sense should not work IMO by having the user do these choices. (Neither lean of isabelle allow that for example). If something, coq-lsp can read the power profile and be more eager / conservative, but always you want to do a bit of prefetching as Isabelle does, even in low power mode (which can the properly limited by the DM to have the right CPU / mem bounds)
Anyways we need a better setup for the start of the page than to expose all these very technical things IMHO.
There was a problem hiding this comment.
The reason I didn't put an option for that is that 0 users do prefer the old mode
You are always criticizing others when they make claims without evidence or false claims, but then you come and make such strong claims yourself. Do I need to remind you that Clément said explicitly that he didn't like the new mode from his experience with other proof assistants that use it?
There was a problem hiding this comment.
@Zimmi48 , I'm sorry to hear you think that me pointing out that a claim seems incorrect to me sounds like a critic; it is for sure not my intention to critizise (and not something I enjoy) but to point out that once I have reviewed what the code is doing I found different. I'd be happy to hear how could I do better in this sense.
In this case I have discussed with maybe a dozen users about their preferences, (and actually I'd love to run a true study on this), and none of the users did prefer the old mode, when we enabled it the bad latency alone makes a big impact on the usability (sample size here is N=3 tho, so again pretty low).
Note that I took Clément feedback into account, indeed you want to check less for example when you are in low power mode etc..., which IIUC that was a core problem he had with other systems. For example I understood that he'd be fine with the current hint Isabelle uses (and that is planned, but requires a bit more work on the core engine)
I was just trying to clarify, based on what Hugo had asked me in person, what was the status of such a feature in coq-lsp and why we didn't put an option to that. If there is interest in having such a mode I'm happy to add and option to enable it as it is only a one-line change in the engine (as I pointed out to Hugo in person)
Co-authored-by: Théo Zimmermann <[email protected]>
Co-authored-by: Théo Zimmermann <[email protected]>
Co-authored-by: Théo Zimmermann <[email protected]>
|
Links updated. I don't know much about ProofEditor. If it was mostly confidential, it could indeed be removed. Who could comment? Yves? |
Co-authored-by: Théo Zimmermann <[email protected]>
Co-authored-by: Théo Zimmermann <[email protected]>
Co-authored-by: Théo Zimmermann <[email protected]>
| <p> | ||
| Both provides the ability of continuous and asynchronous document | ||
| checking as well as position-based document navigation (an | ||
| interaction model introduced in Wenzel's Isabelle/JEdit which |
There was a problem hiding this comment.
I temporarily wrote "Both servers provides the extra ability" until it is clear what is the intent of coq-lsp developers.
You didn't push that change AFAICS.
Co-authored-by: Théo Zimmermann <[email protected]>
Co-authored-by: Théo Zimmermann <[email protected]>
| As a way to try Coq without installing anything, you can also | ||
| use <a href="https://jscoq.github.io/">JsCoq</a> which loads Coq | ||
| entirely in <strong>your browser</strong>. However, it is limited to conduct | ||
| actual projects: it lacks access to the VM and native computing |
There was a problem hiding this comment.
Not sure how "it is limited to conduct actual projects" sounds. Depending on your project it can work very well or very bad. I'd rephrase this entirely.
There was a problem hiding this comment.
OK, but then please suggest an alternative wording. Otherwise, you are just blocking the PR without helping make progress.
There was a problem hiding this comment.
I'm happy to provide the alternative wording, but IMHO we need to converge on the structure first.
There was a problem hiding this comment.
Note that indeed I'd like we don't block this PR for too long, however I think I see some critical issues with it so I'd be great if we could (as requested below) maybe have a quick visio chat and converge.
There was a problem hiding this comment.
I can make myself available tomorrow afternoon if needed. Ping me by Zulip or mail.
| See <tt>coq-lsp's</tt> <a | ||
| href="https://github.com/ejgallego/coq-lsp/blob/main/etc/FAQ.md">FAQ</a> | ||
| for more information. | ||
| <strong>Visual Studio Code</strong> and <strong>VSCodium</strong> users can use |
There was a problem hiding this comment.
Why is coq-lsp out of this list?
There was a problem hiding this comment.
Because this first part is about "Most popular user interfaces": it is set to change in the future when LSP-based extensions become more prevalent.
There was a problem hiding this comment.
Most popular seems like an strange notion, but if that's the criteria coq-lsp may have already more users than for example Coq + VIM already.
There was a problem hiding this comment.
The title may not be the most accurate. The goal was to separate the extensions that we know have been used for years already, from the ones that are still new and experimental, but probably represent the future.
It's hard to tell how many users Coqtail has, but for what this is worth (not a lot), it has twice as many stars on GitHub (compared to coq-lsp) and it had about as many users in the Coq Community Survey 2022 as jsCoq (although jsCoq has many more stars on GitHub).
| <div class="frameworkcontent"> | ||
|
|
||
| <p> | ||
| Coq projects can be developed with a variety of editors thanks to | ||
| Coq projects can be developed with a variety of <strong>editors</strong> thanks to |
There was a problem hiding this comment.
The whole wording of this paragraph sounds bizarre to me
| <div class="frameworkcontent"> | ||
|
|
||
| <p> | ||
| Coq projects can be developed with a variety of editors thanks to | ||
| Coq projects can be developed with a variety of <strong>editors</strong> thanks to | ||
| great support provided through user-contributed extensions. Here, we | ||
| list such support extensions that are actively used and maintained: |
There was a problem hiding this comment.
The below can be hardly called "extensions" IMHO.
There was a problem hiding this comment.
As I wrote below it does refer to the particular way Coq support is implemented, so that's an unecessary technical detail to the user here. We could use instead "editor support for Coq"
There was a problem hiding this comment.
Ah, I now understand what you mean! I think this is because we understand "user-contributed extensions" differently. You think of extensions to Coq while I think of extensions to editors (and I don't know what Hugo had in mind). We could change this to say "user-contributed editor support packages" to clarify.
There was a problem hiding this comment.
Yes I prefer that. For example in the emacs world people don't talk about extensions but about "modes", so I was trying to find out a more common terminology.
| for more information. | ||
| <strong>Visual Studio Code</strong> and <strong>VSCodium</strong> users can use | ||
| the <a href="https://github.com/coq-community/vscoq/tree/vscoq1">VsCoq 1 | ||
| extension</a>, which is maintained by several contributors as part |
There was a problem hiding this comment.
I am not sure who maintains what is relevant in this page.
| <strong>Vim/NeoVim</strong> users can use the actively | ||
| maintained <a href="https://github.com/whonore/Coqtail">Coqtail</a> | ||
| <strong>Vim/NeoVim</strong> users can use the | ||
| <a href="https://github.com/whonore/Coqtail">Coqtail</a> | ||
| extension. This extension is partly based upon a previous, and now | ||
| unmaintained, Vim extension | ||
| called <a href="https://github.com/the-lambda-church/coquille">Coquille</a>. |
There was a problem hiding this comment.
IMHO time to remove this info from here too.
| </ul> | ||
| </div> | ||
| </div> | ||
|
|
||
| <div class="framework"> | ||
| <div class="frameworklabel">Standalone interfaces</div> | ||
| <div class="frameworklabel">Towards an LSP-based modular design of Coq user interfaces</div> |
There was a problem hiding this comment.
What is the point of this section? IMHO it is very confusing, see my full review for more concrete thoughts.
| </ul> | ||
| </p> | ||
| <p> | ||
| Both servers provide the extra ability of continuous and asynchronous document |
There was a problem hiding this comment.
I think it is not the job of this page to compare the servers. Comparing options could be useful but that should be done in its own section and include other interfaces. Moreover keeping these comparisons accurate as the tools change is hard.
There was a problem hiding this comment.
I'm unsure the direction taken here is actually improving what the users need from the core user interface page IMO.
The way I see, when a user arrives to this page, they want to understand how to use Coq, so the first section is IMHO already terrible on that, moreover we create 4 categories of interfaces for the user to understand.
Also, there is no reason to have the LSP section in its current form.
Also, I think that coq-lsp is perfectly usable for a large majority of users and indeed provides a better experience than all the other released UIs so it is certainly for example the first choice for those wanting continous checking on 8.17 today.
|
Moreover interface and installation are the same for users, so certainly we should think (IMO of course) holistically about these two subjects. Compare what we have with Lean: https://leanprover.github.io/download/ It is much less verbose / cluttered. We could maybe do a quick call to prototype a page, but we could indeed try to go on the way of:
WDYT? |
|
Hi @ejgallego: this PR is an evolution of the previous page. This explains:
About lsp, I'd be ok to have less details and to clarify to which exact extent it is already usable now. (But this has to be done by an expert...). My understanding was that it was currently more for beta-testing than for production, but again, I'm not the expert so I can be entirely wrong! On my side, what I think is important (in addition to what was already mentioned as important) is:
If you have an alternative proposal, or if you'd like to modified my proposal, that'd be great. [PS: I'll be at the lab tomorrow 1pm-3:15pm if you want to discuss live] |
I agree that the previous page required change, however I am not sure the direction is the one we'd like.
We can maybe push it as in a more "use case" organization?
I think that assumption may be weak. Moreover a comparison should be avoided IMO, it is not easy.
That's an interesting topic. I can only speak for coq-lsp, but for a very significant number of users it is netly superior to all alternatives. I could put a 1.0 version if that would make people feel better, but I reserved that number for the day coq-lsp outperforms all other interfaces.
IMHO both cases here provide information that is not relevant for the users and thus confusing. This should be moved to the wiki / details page.
Extensions is an implementation term. IMHO no need to put that cognitive load on the reader. Maybe "editor support" or "Coq editor mode" would work?
I think the language "actual projects" is not accurate for the reasons above, yes, we should update that a bit more still IMVHO.
I am using it as the main tool in my Coq papers for example.
That is very important, but I would think that the user interfaces page is not the right place to do so? Users arrive there trying to figure out how to use Coq, we should try to answer directly IMO.
Maybe these two points do belong more on a "Contributing page"?
I think indeed it'd be great if we could discuss a bit about the PR, hopefully with Théo and others interested.
I'll be around but busy until the GT ACS finishes (should be 3 pm) |
Where does the number come from? The only figures that I had so far were from the Coq Community Survey, but these are from before coq-lsp was released. |
Marketplaces show 574 installs , of which around ~ 400 are for 0.1.6 , also I have talked to dozens of users and they implied they had more users in their entourage, so this is my very very inexact estimation, which could be very wrong indeed. |
|
As already said, I started this revision from the existing page. In particular, I tried to respect the intent of what was present before, including text written last January by Emilio about coq-lsp. So, I'm making the assumption that this text was agreed at some time by Emilio and that there is no reason it does not make sense any more. Let's give time to time (as we say in French). I propose (more or less like Théo was proposing I think) that we proceed in two steps.
If we (at least @Zimmi48 and @ejgallego) agree on working on the current structure as a first step, then, we can discuss about how to word things in the detail:
|
What? I formally oppose to stop mentioning it! |
|
Sorry, I meant Coquille, my confusion (fixed). |
While this started from the old page, I still think that the new section about "modular design" adds too much density to this page, thus in a sense going against the idea of making the page easier to parse by non-expert users. I'd suggest we find a slot to sync in person tho, for sure will be more effective!
Indeed, but I think we should not give too much information here, the more info we give, the higher the density, and worse, the harder it is to keep it correct in time as facts become not current anymore.
The focus on LSP in the page is likely the issue I have more problems with. First, because the two LSP servers have a very different set of features and support schedule, second because LSP is a low-level detail so that shouldn't be exposed to users in this stage at all. The question users want to answer is "what interface do I use" ? IMVHO
I'm happy to provide a wording but I suggest we first converge on the structure, if that's OK for you of course.
The problem was fixed in 8.17, and we added extra safeguards, so the experience is much better now. Moreover the solution can be deployed seamlessly on older Coq versions, but I just don't have the manpower to do so (happy to help if someone would volunteer)
It really depends, it is hard to compare. coq-lsp lacks features other systems have, and it has features other systems doesn't have. It is a very long list! For example, PG doesn't work with Elpi (and CoqIDE / VsCoq 1 have still bugs with it), coq-lsp works fine here. coq-lsp allows incremental (cached) and non-linear document edits, on the other hand search is has problems. etc... so it really depends a lot. For me and quite a few others has become our main interface, but YMMV.
As I wrote I see two potential issues with this:
I'd personally place all interfaces in the same footing, I also don't like where CoqIDE is placed now.
Yes, I think we all agree on this very minor tweak.
My fear here is that we would have to mention the maintainers for all interfaces, so that adds a lot of density. I think the wiki page you prepared is excellent so we could indeed leave these details to it, but maybe a workable compromise in terms of density is to write the maintainer(s) in short from, so we would have:
But at some point seems like redundant, I don't know. I'm unsure if we did agree to have a notion of "official" interface, that would certainly be relevant for users, but I guess we'd need to discuss what we consider "official" tho. |
|
Has this been superseded by #227 ? |
|
Not really supersed, but #227 is a good compromise. No short-term project to work on the PR, but maybe at some time. You can close it if it helps the management of PRs. |
|
Ok, closing for now |
This update of the user interface page has the following objectives: