search

coq / coq.github.io

Source files of the coq.inria.fr website
https://coq.inria.fr/
Other
15 stars 37 forks source link

Proposal for updating the user interfaces page. #218

Closed herbelin closed 4 months ago

herbelin commented 1 year ago

This update of the user interface page has the following objectives:

herbelin commented 1 year ago

Links updated. I don't know much about ProofEditor. If it was mostly confidential, it could indeed be removed. Who could comment? Yves?

ejgallego commented 1 year ago

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?

herbelin commented 1 year ago

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]

ejgallego commented 1 year ago

Hi @ejgallego: this PR is an evolution of the previous page. This explains:

I agree that the previous page required change, however I am not sure the direction is the one we'd like.

  • the place given to "Coq without install"

We can maybe push it as in a more "use case" organization?

  • the level of details and comparisons given on lsp-based UIs (which I agree is difficult to keep accurate along the time; but that idea is also that the page will be kept up-to-date in real time, at least as long as there is active work on interfaces)

I think that assumption may be weak. Moreover a comparison should be avoided IMO, it is not easy.

  • the "under development" status put on lsp-based UIs

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.

  • the place given to Coquille (which I agree could go the history)
  • the reference to maintainers (from my point of view, mentioning the maintainers or not could be up to what authors prefer)

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.

  • calling "extensions" the Coq support integrated to existing editors (but how would you call them?)

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?

  • the limitation mentioned for JsCoq (I'd be happy to remove the text if the expert says it is not outdated)

I think the language "actual projects" is not accurate for the reasons above, yes, we should update that a bit more still IMVHO.

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!

coq-lsp has over a hundreth users right now, and so far it works very very stably (it was desgined for that). There are some issues to solve, but the reason I released coq-lsp was due to the urgency expressed by the Coq direction on having something available for the users. As I wrote above it outperforms existing released interfaces in many cases already.

I am using it as the main tool in my Coq papers for example.

On my side, what I think is important (in addition to what was already mentioned as important) is:

  • to promote the work of the community and in particular to promote the UIs for Emacs, Vim, VsCode (accompanied with factual arguments, if needed).

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.

  • to advocate somewhere modularity and to encourage to develop other clients of lsp servers

Maybe these two points do belong more on a "Contributing page"?

If you have an alternative proposal, or if you'd like to modified my proposal, that'd be great.

I think indeed it'd be great if we could discuss a bit about the PR, hopefully with Théo and others interested.

[PS: I'll be at the lab tomorrow 1pm-3:15pm if you want to discuss live]

I'll be around but busy until the GT ACS finishes (should be 3 pm)

Zimmi48 commented 1 year ago

coq-lsp has over a hundreth users right now

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.

ejgallego commented 1 year ago

Where does the number come from?

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.

herbelin commented 1 year ago

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.

  1. We stabilize a version of the page that follows the current structure and which is worded in a way that everyone considers factually correct today.
  2. By September, when we have a bit more hindsight on LSP-based technology, we think at a possible different structure, which could actually be proposed as soon as now, but which I think should then be approved by everyone involved, and that may require some time.

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:

Zimmi48 commented 1 year ago

Coqtail -> I agree to stop mentioning it (I just added it to the wiki for the record)

What? I formally oppose to stop mentioning it!

herbelin commented 1 year ago

Sorry, I meant Coquille, my confusion (fixed).

ejgallego commented 1 year ago

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.

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!

  1. We stabilize a version of the page that follows the current structure and which is worded in a way that everyone considers factually correct today.

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.

  1. By September, when we have a bit more hindsight on LSP-based technology, we think at a possible different structure, which could actually be proposed as soon as now, but which I think should then be approved by everyone involved, and that may require some time.

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

  • jsCoq -> we could put a <strong> on "without installing anything" so that this can be seen directly when reading in diagonal; about the wording, Emilio, what would you suggest?

I'm happy to provide a wording but I suggest we first converge on the structure, if that's OK for you of course.

  • coq-lsp: the question seems to be to understand the status of it; my last experience with it (less than two months ago), was it was not supporting multiple files (with an old version of Coq); so, to be honest, I'm a bit afraid that coq-lsp is currently working only with the last version of any of its package requirements, and that gives the feeling that it is still under active development and thus worth to be advertized stepwise, at a regular pace, peacefully, taking the time to convince everyone, without being too much in the emotion of the instant.

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)

In particular, I'm not saying at all that it is not usable. I'm not opposing either to the claim that it would outperform any other existing interfaces, on the contrary. What I'm saying is that I feel that the typical current user is someone ok to live on the edge and willing to provide feedback (but maybe I'm wrong).

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.

According to this view, I think the "Towards an LSP-based modular design of Coq user interfaces" is good, because it stepwise prepares minds to the lsp-based client-server approach becoming the norm. (Again, I may be wrong and maybe only people with age > 45 have yet to be prepared to this evolution.)

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.

  • extension vs editor support vs editor mode: at the current stage of my understanding, I don't see what is wrong with "extension"; for instance, PG is much more than an emacs mode or an emacs support for Coq, it introduced proof-assistant features in a way which is more than just using Coq through emacs.

Yes, I think we all agree on this very minor tweak.

  • reference to maintainers of VsCoq: I have no opinion. I suspect that it was mentioned because it was an important concern for the VsCode community, but if this concern is obsolete we can remove it (at least, we should ask the vscode maintainers to know if it matters for them).

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.

mattam82 commented 4 months ago

Has this been superseded by #227 ?

herbelin commented 4 months ago

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.

mattam82 commented 4 months ago

Ok, closing for now