Stream: jsCoq

Topic: Flèche Upgrade Process Thread


view this post on Zulip Shachar Itzhaky (Sep 26 2022 at 18:53):

This topic is to coordinate as @Emilio Jesús Gallego Arias and myself are working towards a functional (in the sense of "working") coq-lsp-based version for both literate programming documents and the scratchpad.

Feel free to mute the topic as it may get some heavy traffic at bursts.

view this post on Zulip Shachar Itzhaky (Sep 27 2022 at 08:57):

I motion that we move the source directories frontend, backend, and coq-jslib into a subdir src/. This is conventional in js projects, don't know if there is a similar convention in ocaml but I've noticed some coq plugins have their ocaml sources in src/. wdyt?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2022 at 10:53):

I think that the coq-jslib should go away entirely, as for moving backend / frontend into src I'm not sure it is an improvement. I view src as a kind of anacronic pattern, when I check the repository I know I'm already in the source code. So this just adds a longer path to every source file to save one entry in the root dir. Not worth it IMHO.

Some developments have server / client directories at the toplevel (see for example https://github.com/microsoft/vscode-languageserver-node ) which makes sense to me as these are separate components / packages. And indeed, it seems to me that here it is the case that the backend / frontend are really separate components.

view this post on Zulip Shachar Itzhaky (Sep 27 2022 at 11:18):

yeah ok. I have adopted src for my projects out of the feeling that there is a lot of "stuff" that tend to be in the main directory, which ofc can also be viewed as source code (build, package configuration, documentation, tests) but not "the source". But sure if all of it goes into backend / frontend then that's indicative enough.

view this post on Zulip Shachar Itzhaky (Sep 27 2022 at 11:21):

Right now I'm working on this: converting the "markdown" boolean flag into a config option content_type with values Coq and Markdown. We can even have other values later on.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2022 at 12:34):

Yes, it is very important to keep the main directory organized, another important point is the vendoring we are doing which is a bit of a PITA. I'm convinced a monorepos would be more effective, but that has other bad properties :S

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2022 at 12:35):

Shachar Itzhaky said:

Right now I'm working on this: converting the "markdown" boolean flag into a config option content_type with values Coq and Markdown. We can even have other values later on.

Do we need the flag at all tho? We could just do the processing client-side as we do for ProseMirror?

view this post on Zulip Shachar Itzhaky (Sep 27 2022 at 12:58):

Do we need the flag at all tho? We could just do the processing client-side as we do for ProseMirror?

Ok yeah we could, that's probably another way to do it. And for ocaml clients you can provide a convenience method to do the same preprocessing.

view this post on Zulip Shachar Itzhaky (Sep 27 2022 at 19:16):

I find this xkcd strip about SE quite appropriate.
https://imgs.xkcd.com/comics/two_key_system.png

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2022 at 22:21):

I'm interested in resurrecting Interrupt

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2022 at 23:31):

It seems to work well, nothing to do there.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2022 at 23:31):

Next I will do queue optimization

view this post on Zulip Emilio Jesús Gallego Arias (Sep 28 2022 at 19:42):

Note that LSP / Flèche will have to keep supporting markdown in the OCaml so for example emacs users can open foo.mv files without going too far from standard lsp support, but jscoq doesn't need to use that.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 28 2022 at 19:42):

I'm still wondering about multiple formats in the same document, today Makarius did talk a bit about what he does in Isabelle but I don't understand the technical details

view this post on Zulip Shachar Itzhaky (Sep 29 2022 at 12:37):

I am wondering if there is a concept of mini-modes in LSP?

view this post on Zulip Shachar Itzhaky (Sep 29 2022 at 12:38):

e.g. in VSCode you can have JS nestled within HTML and it's handled just like a JS document

view this post on Zulip Shachar Itzhaky (Sep 29 2022 at 12:39):

ideally we will use Emacs' markdown mode with a coq-lsp nested mode

view this post on Zulip Shachar Itzhaky (Sep 29 2022 at 17:26):

umm I think I broke something
I am getting all the diags for the original document, but for updates I am getting Diags received: 0

view this post on Zulip Shachar Itzhaky (Sep 29 2022 at 17:26):

how can this be

view this post on Zulip Shachar Itzhaky (Sep 29 2022 at 18:54):

It seems to be caused by this

    update(text, version) {
        this.sendCommand(["Update", text, version]);
        this.interrupt();   <----
    }

I remember you explaining to me why this makes sense. But it looks like there can be a race in case the queue is empty? As in, it will interrupt the update that was just requested?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 19:45):

Indeed there is a problem!

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 19:45):

Yeah I was playing with that and committed a wrong version

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 19:46):

Still not sure what the best way is

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 19:46):

Shachar Itzhaky said:

ideally we will use Emacs' markdown mode with a coq-lsp nested mode

This has been so far quite tricky, as far as I know, the mythical MMM mode in Emacs. I don't know how vscode does, but likely it just sends the full document to the server (and it ignores the html?)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 19:47):

Emilio Jesús Gallego Arias said:

Yeah I was playing with that and committed a wrong version

That doesn't make sense in general, tho with some queues approach I took it could

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 19:48):

in the OCaml server we can do better as we can use OS-level threads

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 19:49):

An interesting possibility is to use two workers, one that is a queue manager, and one that does the work

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 19:50):

But yeah, I don't have yet a very concrete design in mind

view this post on Zulip Shachar Itzhaky (Sep 29 2022 at 20:47):

Seems like you were facing the problem of the message event handler not being called while the dequeue loop is running. I think even a lean yield (e.g. await Promise.resolve()) would take care of that, and will push all pending updates to the queue, allowing for compaction.

I assume you want to cause an interrupt in case the worker is actually busy and waiting for the current document check to complete will take too long. I think that this is doable, but perhaps the worker needs to artificially clear the interrupt flag when it starts an operation. Because an interrupt that was set before the operation started, should not interrupt it; that's just leftovers from a previous operation that terminated before getting the chance to read the interrupts.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 20:51):

Yes, actually the code in coq-lsp does reset the flag

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 20:52):

But the semantics of the queue, that myself I havent' figured out yet, it seems to me that we should also interrupt on Requests

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 20:52):

so yeah that's something to design

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 20:52):

so if a goal request comes, we preempt the checking, solve it, and resume

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 20:57):

By the way I have a patch to that require will callback

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 20:57):

however, that callback is still in the worker context

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 20:58):

Type is { from : DirPath.t option; dirpath : DirPath.t } -> Path.t Promise.t

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 20:59):

Given that interrupt works OK I think [modulo the queue problems] I will work next days on fixing the auto-include stuff

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2022 at 21:02):

There are still two options possible for it:

I'm not sure what approach would be best.

view this post on Zulip Shachar Itzhaky (Sep 30 2022 at 14:10):

I think it would be ok to send a message from the worker to the main thread for every Require that is being evaluated. Then the main thread can either say "ok go ahead" or block the worker until libraries have been downloaded (or even interrupt the worker and then re-check the document). At any rate, cached states will not trigger the round-trip, so the impact will not be huge.

view this post on Zulip Shachar Itzhaky (Sep 30 2022 at 14:56):

Ok I have pushed a version with ProviderContainer for documents with multiple snippets as before.

view this post on Zulip Shachar Itzhaky (Sep 30 2022 at 14:57):

I suggest we take the landing page and turn it into a ProseMirror document? That could be neat.

view this post on Zulip Shachar Itzhaky (Sep 30 2022 at 14:57):

In the meantime I'm attempting to reconstruct waCoq on top of the new coq_interp

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:37):

So that would be a request from the worker (server in LSP terminology) to the client

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:42):

Yup, we can try to go that way then, but in a sense that message will be "out of band", and not part of the protocol as such. Actually the best implementation is when the worker can indeed handle the download, IMO. This seems something that belongs in the server.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:42):

Shachar Itzhaky said:

Ok I have pushed a version with ProviderContainer for documents with multiple snippets as before.

Great! Now we need to attach a tooltip with the error message on the mark and we should be very close to have something working!

view this post on Zulip Shachar Itzhaky (Sep 30 2022 at 18:42):

oh yes :)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:43):

Looking forward to see coq-next + SF with the new system, so we can fine tune it.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:43):

For waCoq, maybe we could do a bit of hacking session over zoom? I wanted to do that in Paris, but we ran out of time. IMO it makes sense first to merge the OCaml code in backend, we can do that for the original protocol first. WDYT?

view this post on Zulip Shachar Itzhaky (Sep 30 2022 at 18:43):

yeah I need to get the wa support as SF in general does not eval with js but perhaps some of it would

view this post on Zulip Shachar Itzhaky (Sep 30 2022 at 18:44):

ok yeah

view this post on Zulip Shachar Itzhaky (Sep 30 2022 at 18:44):

I think most of the code in wacoq-bin will not be needed

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:44):

By the way, I was thinking today about completion, something that is very needed by people is completion of notations.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:44):

We can actually do that very easily, provided we have a reasonable JS library for "templates"

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:44):

as the ones emacs has for snippets

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:45):

Shachar Itzhaky said:

I think most of the code in wacoq-bin will not be needed

Yes it should not take us long, I suggest we indeed do that in the non LSP branch first

view this post on Zulip Shachar Itzhaky (Sep 30 2022 at 18:45):

yes and also something that Clement once suggested to me, showing in the completion identifiers from the docs that are not currently loaded (and even if the user selects them, add the corresponding Require!)

view this post on Zulip Shachar Itzhaky (Sep 30 2022 at 18:47):

I'm usually in favor of small steps but in this case perhaps merging waCoq in the Flèche branch is the path of least resistence

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:47):

As you prefer, I think it should commute

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:48):

I thought a PR from 8.16 could mean that we can push the merge to the main branch quicker, but I don't mind doing the other way either

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:48):

depends how we organize, if we work async on this def a smaller PR is easier to review

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:48):

ideally the protocol file will be shared so not a huge deal to rebase

view this post on Zulip Shachar Itzhaky (Sep 30 2022 at 18:49):

ok maybe you're right. anyway the main obstacle is to get open Js_of_ocaml out of coq_interp so that we can use it in wasm as well, or put in place some conditional compilation

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:49):

showing completion of things that are not loaded is interesting, actually the way I proposed to go upstream is to cache this info in the vo files, so you can query it without loading the full .vo, but we can maybe extract a cache for the package?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:50):

Shachar Itzhaky said:

ok maybe you're right. anyway the main obstacle is to get open Js_of_ocaml out of coq_interp so that we can use it in wasm as well, or put in place some conditional compilation

let's get it out of place

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:50):

yes

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:50):

so if you wanna work syncronoulsy on that let's fix a time next week

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 18:51):

need to go now, but will try to push js_of_ocaml out of interp in the main branch

view this post on Zulip Shachar Itzhaky (Sep 30 2022 at 18:53):

ok good, I think Monday would be ok

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2022 at 19:06):

good, I've pushed a branch moving the proto and interp to common

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 08:08):

Shachar Itzhaky said:

ok good, I think Monday would be ok

All days except Tue will work for me

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 08:08):

Emilio Jesús Gallego Arias said:

good, I've pushed a branch moving the proto and interp to common

Something I'm wondering is if we should put the package logic back in the worker, as it was

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 08:08):

@Shachar Itzhaky what was the motivation for moving it to the client?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 08:08):

It seems waCoq moved it back to the server/worker?

view this post on Zulip Shachar Itzhaky (Oct 01 2022 at 10:06):

Yeah it was convenient in waCoq to put this logic in the worker since I already had some JS running in the worker. Do we want to do it in jsCoq as well?

view this post on Zulip Shachar Itzhaky (Oct 01 2022 at 13:55):

Looks like I'm in need of a native library that I wasn't before: dllbase_internalhash_types_stubs.
Where does it come from?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 18:13):

Shachar Itzhaky said:

Yeah it was convenient in waCoq to put this logic in the worker since I already had some JS running in the worker. Do we want to do it in jsCoq as well?

Need to think a bit about it, but I think we should do what we think is best in terms of "ownership" of resources. Who owns the FS or the packages for example is IMO more important than the language that have been implemented. Both in wacoq and jsoo we can use js just fine (and in fact there is this automatic js -> ocaml generator for jsoo)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 18:14):

But indeed I think it makes sense the server owns the packages, as it is the main consumer, what is the point of doing the roundtrip to the client just to resolve a missing lib?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 18:14):

Seems like overkill to me, and a nice opportunity to have protocol "fun" XD

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 18:15):

Shachar Itzhaky said:

Looks like I'm in need of a native library that I wasn't before: dllbase_internalhash_types_stubs.
Where does it come from?

That's coming from ppx_hash which uses Jane Street hash library (from base I think).

That's needed to implement the caching tables, moreover we tweak the hash to ignore some stuff (that is reconstructed later by the cache) as we discussed

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 18:15):

Is that a tricky one? I guess JS implemeted it in C to make it faster?

view this post on Zulip Shachar Itzhaky (Oct 01 2022 at 18:26):

yes it's implemented in C which in principle should be ok but I'm having some trouble loading it for some reason

view this post on Zulip Shachar Itzhaky (Oct 01 2022 at 18:26):

how did it work with jsoo? did you add stubs?

view this post on Zulip Shachar Itzhaky (Oct 01 2022 at 18:29):

Emilio Jesús Gallego Arias said:

Seems like overkill to me, and a nice opportunity to have protocol "fun" XD

I am not sure it's an overkill but at any rate it seems that it's not the interpreter that should load the packages, but some hook like you mentioned. We can implement it in OCaml... just that downloading & unzipping in OCaml seemed like a headache.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 22:56):

Shachar Itzhaky said:

how did it work with jsoo? did you add stubs?

I did nothing!

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 22:58):

I've never heard of that stub

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 23:05):

Shachar Itzhaky said:

We can implement it in OCaml... just that downloading & unzipping in OCaml seemed like a headache.

js is fine too, for the Require to filename resolution OCaml is tempting because I can just reuse the lookup library in Coq, so I don't have to reimplement the semantics.

Why is downloading and unzipping in OCaml a headache? Jslibmngr still has the download code, it is just a Lwt.t promise, pretty straightforward:

let* frame = Js_of_ocaml_lwt.XmlHttpRequest.perform_raw ~response_type:ArrayBuffer request_url in
if frame.code = 200 then
  let cache_entry = Typed_array.String.of_arrayBuffer frame.content in
  let () = Hashtbl.add file_cache full_url cache_entry in
  Lwt.return_unit
else
  Lwt.return_unit

anyways it is fine to call a Js lib from jsoo too

view this post on Zulip Shachar Itzhaky (Oct 02 2022 at 04:04):

what about progress? what about unzipping? also, in wasm, will we still use jsoo for the package management part?

view this post on Zulip Shachar Itzhaky (Oct 02 2022 at 04:37):

Emilio Jesús Gallego Arias said:

Shachar Itzhaky said:

how did it work with jsoo? did you add stubs?

I did nothing!

Oh I wonder if jsoo automatically includes Jane Street's JS runtime of base!! That would be funny.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 03 2022 at 12:39):

That's a good point about jsoo! I have no idea

view this post on Zulip Emilio Jesús Gallego Arias (Oct 03 2022 at 12:41):

Shachar Itzhaky said:

what about progress? what about unzipping? also, in wasm, will we still use jsoo for the package management part?

Unzipping can be done with camlzip just fine I think? (And I'd bet it outperforms node XD, at least in the native case) Progress is actually done OK too? Anyways I'm very happy for the worker to be a hybrid TS/OCaml setup, including the package manager.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 03 2022 at 12:42):

OCaml / Reason is great for web dev actually, but with TypeScript these days there is less need for a strongly typed system, but still in some cases I find the workflow more streamlined.

view this post on Zulip Shachar Itzhaky (Oct 03 2022 at 12:59):

camlzip is written in C. I believe we looked into it at some point.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 03 2022 at 14:58):

Yes, the pure one is decompress

view this post on Zulip Emilio Jesús Gallego Arias (Oct 03 2022 at 15:47):

If I can reuse the package manager from wacoq in the jsoo server I'll do so tho

view this post on Zulip Emilio Jesús Gallego Arias (Oct 03 2022 at 15:47):

it is only two callbacks so I'm happy to wrap that

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 14:40):

I did a pass yesterday and rebased the lsp branch on top of wacoq

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 14:40):

things are looking really good!

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 14:40):

The LSP stuff needs some tweaks, mainly to jump faster to position on edits

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 14:40):

and I will push the curvenote stuff

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 14:41):

and at some point some other nits

view this post on Zulip Shachar Itzhaky (Oct 06 2022 at 15:43):

oh wow you rebased over the interp_unify? and it worked??

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 15:48):

didn't try wacoq as I ran out of time

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 15:48):

but builds

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 15:49):

It should work, provided the loader works

view this post on Zulip Shachar Itzhaky (Oct 06 2022 at 15:49):

lol

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 15:49):

that's actually tricky I'm not sure how it is working now in jsoo

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 15:49):

but it does!

view this post on Zulip Shachar Itzhaky (Oct 06 2022 at 15:49):

ok I'll try it!

view this post on Zulip Shachar Itzhaky (Oct 06 2022 at 17:55):

Hmm it is trying to load coq-serapi.serlib.ltac via findlib

view this post on Zulip Shachar Itzhaky (Oct 06 2022 at 17:55):

it is really fascinating how this "just works" in jsoo! what did they do to support findlib?

view this post on Zulip Shachar Itzhaky (Oct 06 2022 at 21:02):

Also all error msgs in waCoq have a gazillion times this string: "Called from unknown location"

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 12:38):

That's lack of backtraces? Strange

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 12:38):

For the loading of serlib.ltac I did nothing, in fact I can't figure out how it is working now

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 12:38):

It is a mystery I need to research

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 12:39):

the code in question is here

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 12:45):

https://github.com/jscoq/jscoq/blob/v8.16%2Blsp/backend/jsoo/jscoq_worker.ml#L126

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 12:45):

maybe try the same?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 12:45):

haha

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 12:45):

I just refuse to load anything not from the legacy method

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 12:45):

but it is really a mystery why that is working

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 12:46):

it should not unless we linked the serlib thing statically somewhere

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 12:46):

before we did

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 12:46):

but after I removed the serapi dep we should not

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 13:02):

if we don't link that libraries, the thing is that we should get way more cache misses, so it is nothing "fatal"

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 13:02):

as the libraries implement the cache-optimized ops

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 13:02):

but we don't

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 14:30):

Indeed, we are not loading the serlib plugins so caching works worse now, but it does work

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 14:31):

I've pushed a better plugin loding setup to the branch

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 14:31):

so I suggest for wacoq you just ignore the finlib libs for now, see the new commit

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 15:31):

Indeed, the mystery is solved: we used to link serlib.ltac statically.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 15:31):

Now we don't

view this post on Zulip Emilio Jesús Gallego Arias (Oct 07 2022 at 15:31):

I'll push a patch to hopefully fix wacoq for now tho.

view this post on Zulip Shachar Itzhaky (Oct 07 2022 at 18:24):

Oh actually now it fails with (Sys_error "/home/ltac_plugin: No such file or directory")

view this post on Zulip Shachar Itzhaky (Oct 07 2022 at 18:25):

btw all the deps should be in place now. If you install wasi-sdk (which eventually will be installed by toolchain_setup I guess) you should be able to run make wacoq!

view this post on Zulip Shachar Itzhaky (Oct 07 2022 at 18:25):

then all you need to do is set backend: 'wa' in the options

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:31):

Great!!

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:31):

Shachar Itzhaky said:

Oh actually now it fails with (Sys_error "/home/ltac_plugin: No such file or directory")

Oh, that problem is solved in the jsoo using the special Jslibmng.coq_cma_link

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:32):

Mmmm

view this post on Zulip Shachar Itzhaky (Oct 08 2022 at 13:32):

ok but ltac_plugin is using legacy mode and is in path

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:32):

What Coq does to locate a plugin in legacy mode is to scan the directories

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:32):

that didn't work in jsoo

view this post on Zulip Shachar Itzhaky (Oct 08 2022 at 13:32):

actually I did not get this message before your last patch

view this post on Zulip Shachar Itzhaky (Oct 08 2022 at 13:33):

in wasm it can scan the path and find the right one usually

view this post on Zulip Shachar Itzhaky (Oct 08 2022 at 13:33):

no idea why it is trying /home

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:33):

Oh

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:34):

Indeed my patch is buggy in this sense

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:34):

That's what Coq does if not mltop is set

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:34):

    | { file = Some file; lib } ->
      let file = select_plugin_version file in
      let _, gname = System.find_file_in_path ~warn:false !coq_mlpath_copy file in
      Dynlink.loadfile gname;
      Findlib.(record_package Record_load) lib

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:35):

Ok so replace the code in load_module for something like

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:35):

let load_module file =
  let file = file ^ ".cma" in
  let _, gname = System.find_file_in_path ~warn:false !coq_mlpath_copy file in
  Dynlink.loadfile gname

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:36):

Where !coq_mlpath_copy should be the search path

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:36):

Yeah that was an oversight in the compat layer code I did for 8.16

view this post on Zulip Shachar Itzhaky (Oct 08 2022 at 13:36):

ok, it looks weird that we cannot call the "normal" top's load_module

view this post on Zulip Shachar Itzhaky (Oct 08 2022 at 13:36):

so you need to duplicate it

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:36):

Yes that's a problem in the API

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:36):

You have to set both

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:37):

Maybe I was thinking of jsoo as to allow the clients to overload not only the function loading the mdoule

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:37):

but the path resolution procedure

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:37):

the pity is that indeed we cannot just disable the findlib loader

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:38):

Or just patch Coq to explose Mltop.PluginSpec.load

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:38):

and use it

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:38):

Yeah easier is just to do load_module = Mltop.PluginSpec.load

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:38):

and export that in mltop.mli

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:38):

val load : t -> unit

view this post on Zulip Shachar Itzhaky (Oct 08 2022 at 13:39):

ok that sounds like a valid patch

view this post on Zulip Shachar Itzhaky (Oct 08 2022 at 13:43):

wait, PluginSpec.load docs say that it also invokes findlib so I'm a bit confused:

  (* Load a plugin, low-level, that is to say, will directly call the
     loading mechanism in OCaml/findlib *)
  val load : t -> unit

view this post on Zulip Shachar Itzhaky (Oct 08 2022 at 13:43):

load_module should be for loading a .cma directly, no?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:50):

Oh yes, damn

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:50):

indeed it registers the loaded module with findlib

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:50):

yeah load_module should be that way, but the organization of the code is very subtle

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:51):

so for now load_module has two tasks: to locate the module, then to load it.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:51):

Was an attempt to allow more flexibility to the caller

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:51):

We can for now just indeed use the longer version :S

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:51):

Or we can have findlib not to fail, we just need some dummy conf in path

view this post on Zulip Shachar Itzhaky (Oct 08 2022 at 14:16):

I have a conf already

view this post on Zulip Shachar Itzhaky (Oct 08 2022 at 14:16):

it has this: path="/lib/ocaml"

view this post on Zulip Shachar Itzhaky (Oct 08 2022 at 14:16):

findlib in wasm seems to find it

view this post on Zulip Shachar Itzhaky (Oct 08 2022 at 15:02):

are you no longer using the Loader module from coq-lsp?

view this post on Zulip Shachar Itzhaky (Oct 08 2022 at 15:37):

I captured the ml path like this:

  let mlpath = Loadpath.get_load_paths ()
               |> List.map Loadpath.physical in

is this ok? Or is there a better way w/o going through Coq?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 23:41):

Shachar Itzhaky said:

are you no longer using the Loader module from coq-lsp?

It is not useful until findlib support is working

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 23:41):

likely we want to tweak the API a bit

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 23:42):

all the loader module does is to load instrumentation plugins

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 23:42):

Shachar Itzhaky said:

I captured the ml path like this:

  let mlpath = Loadpath.get_load_paths ()
               |> List.map Loadpath.physical in

is this ok? Or is there a better way w/o going through Coq?

I'm afraid the ML path is totally separated and kept in Mltop

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 23:43):

But if you have a config that doesn't make wacoq crash you can just use Mltop.PluginSpec.load

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 23:44):

The only API to get the (legacy) ML path is Mltop.print_ml_path lol

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 05:47):

oh I thought this was the same code that is used for vscode

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 16:28):

coq-lsp just always uses findlib

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 16:29):

Actually load_module is irrelevant for us, I remeber why it is there

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 16:30):

The native compiler needs it to load the JITed modules

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 16:30):

so it is always load_plugin

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 17:01):

wait didn't you make this change in coq-lsp? Or is it a separate branch of coq-lsp for jsCoq?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 19:13):

coq-lsp is using this change

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 19:14):

but it sets up the loader differently

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 19:14):

As it assumes a working findlib

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 19:14):

The loading method is paramter to the library, it is setup differently in the coq-lsp driver and jscoq jsoo driver

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 19:51):

Pushed a patch that should fix wacoq

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 20:35):

ok cool!

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 20:37):

oh you've put it in load_plugin

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 20:37):

alright that might be better in fact

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:45):

Yes, load_module is unused actually

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:45):

it is only there for the native compiler which we don't use

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:45):

and still needs to call Dynload directly

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:46):

I had to patch Coq as I didn't anticipate our use case here, but in the end we should use findlib, or whathever we want

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:46):

as load_plugin gets the findlib name (and maybe a legacy name if present in Declare ML Module) and let us do what we want

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:46):

but I bet getting findlib to work in wacoq is easy

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:47):

I think we can get it to work first without dependencies, then later on we can start packaging some libs

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:47):

like elpi

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:47):

that should be easy elpi.ocaml-pkg should contain the META and the cma

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 20:49):

yes, in fact I have already been able to call findlib in wacoq in the past, I just needed to put all the META files in the right places

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 20:50):

so if we can have Dune assist us in locating all the deps then packaging them would be easy

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:55):

Dune knows about the deps but in general we can't rely on it due to some packages not being compiled with Dune

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:55):

Tho Dune reads the META files too, not sure Dune allow us to dump the databse

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 20:55):

ok waCoq works :thumbs_up: although I don't quite understand why in jsCoq there are tons of debug output messages and in waCoq there's silence

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:55):

Shachar Itzhaky said:

ok waCoq works :thumbs_up: although I don't quite understand why in jsCoq there are tons of debug output messages and in waCoq there's silence

I know that one, let me fix it

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:55):

Well I'm not sure I know how to fix it, but I bet it is related to this call

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:57):

let lsp_cb =
  Fleche.Io.CallBack.
    { log_error = (fun cat msg -> Format.eprintf "[%s] %s@\n%!" cat msg)
    ; send_diagnostics = (fun ~uri:_ ~version:_ _diags -> ())
    }

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:57):

tho that's set in icoq.ml, so it should be common for both?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:58):

You are missing the "cache hit messages" etc... right?

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 20:58):

yeah

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 20:58):

They are sent to this callback

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 20:58):

so eprintf messages are not directed to the log window but still I should have seen them in the console

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 20:58):

I have seen eprintfs before

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 20:59):

alright I'll check it tomorrow

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 20:59):

one good thing about wasm is that it is not slowed down by the developer tools being open :)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 21:00):

Oh that's cool!

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 21:01):

yeah in jsoo we post a Log even for each stdout / stderr

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 21:01):

So to find the deps of a plugin

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 21:01):

provided the plugin did install its META correctly

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 21:02):

you do this

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 21:03):

ocamlfind query $pkg -r

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 21:03):

for elpi it gives

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 21:03):

/home/egallego/.opam/coq-v8.15/lib/seq
/home/egallego/.opam/coq-v8.15/lib/re
/home/egallego/.opam/coq-v8.15/lib/re/str
/home/egallego/.opam/coq-v8.15/lib/elpi/util
/home/egallego/.opam/coq-v8.15/lib/elpi/lexer_config
/home/egallego/.opam/coq-v8.15/lib/menhirLib
/home/egallego/.opam/coq-v8.15/lib/result
/home/egallego/.opam/coq-v8.15/lib/ppx_deriving/runtime
/home/egallego/.opam/coq-v8.15/lib/stdlib-shims
/home/egallego/.opam/coq-v8.15/lib/ocaml
/home/egallego/.opam/coq-v8.15/lib/elpi/parser
/home/egallego/.opam/coq-v8.15/lib/elpi/trace/runtime
/home/egallego/.opam/coq-v8.15/lib/elpi

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 21:04):

oh cool that's precisely what I need

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 21:04):

yes

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 21:04):

that is in fact the list that I constructed manually before ;))

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 21:04):

ok perfect

view this post on Zulip Shachar Itzhaky (Oct 09 2022 at 21:05):

gnight then :)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 21:07):

You can refine that, likely ocamlfind query elpi -r -format '%+a' -predicates byte and ocamlfind query elpi -r -format '%m is what you need

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 21:07):

good night!

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2022 at 21:07):

Shachar Itzhaky said:

that is in fact the list that I constructed manually before ;))

Yes, we don't need to gather the info manually, fortunately for us ocamlfind API is very stable

view this post on Zulip Shachar Itzhaky (Oct 17 2022 at 09:39):

I want to get a working version that can load Required packages. I know you mentioned doing the hook to the module resolution mechanism, but I thought maybe a simpler solution would be to use some logic from coqdep. I only need to detect whether the user has edited a sentence that has a Require so that I don't run coqdep on every edit. Is this something that's easy to get?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 10:48):

Using coqdep may be a bit annoying in the sense that it will choke big time on edits as most of the time such edits may not be parseable.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 10:49):

We have already a branch in coq-lsp that can hook the loadpath thing, but if you want something more immediate you can just inspect the error diagnostic

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 10:49):

In the current model there is little the client can do about this

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 10:50):

[and that kind of model is something that seems hard set in the LSP approach, IIU LSP devs correctly]

view this post on Zulip Shachar Itzhaky (Oct 17 2022 at 10:51):

ok yeah I can look at errors as a starting point. Can I get the ast of the Require that failed?

view this post on Zulip Shachar Itzhaky (Oct 17 2022 at 10:56):

and another issue that we had is how to update the loadpath in the starting state

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:00):

The advantange of the loadpath hook is that we don't need to update any loadpath

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:00):

The resolution function owns the loadpath so Coq can just be happy and don't care about it

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:01):

Yes it should be easy to send to require ast in the error state

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:01):

so then we have something like:

view this post on Zulip Shachar Itzhaky (Oct 17 2022 at 11:02):

yeah well if you think that would be too much of a hack to change the loadpath I can wait for the hook

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:02):

the update of the initial state should have fleche recheck everything

view this post on Zulip Shachar Itzhaky (Oct 17 2022 at 11:02):

ok but this state is now inside coq-lsp so it's hard to access

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:02):

up to you, I think it is not too much work, the loadpath stuff is actually trickier than it looks, as I've discovered in the branch

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:02):

due to the loadpath code needing the .vo files in place before they can be built XD

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:03):

Shachar Itzhaky said:

ok but this state is now inside coq-lsp so it's hard to access

Yup we need to patch Flèche, but that's not a hard patch, I can take care of that one

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:03):

it is just updating the state as we do in the non-lsp version of jscoq

view this post on Zulip Shachar Itzhaky (Oct 17 2022 at 11:04):

ok let me start by taking a look at the require ast

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:04):

great

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:04):

I'd suggest you basically replace this line https://github.com/ejgallego/coq-lsp/blob/main/fleche/doc.ml#L203

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:05):

with a modular build_error_diagnostic function

view this post on Zulip Shachar Itzhaky (Oct 17 2022 at 11:05):

ok cool

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:05):

which takes the context, and in the same way we do error recovery, can attach custom info to the diagnostic

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:05):

at some point we will add error codes, etc...

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:06):

LSP finally supports custom diagnostics attributes, I had to introduce this --std argument to coq-lsp as in the past emacs and other clients choked if the diagnostics contained extra fields

view this post on Zulip Shachar Itzhaky (Oct 17 2022 at 11:06):

what does --std mean?

view this post on Zulip Shachar Itzhaky (Oct 17 2022 at 11:06):

avoid non-standard attributes?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:07):

so it should be

let diags = mk_diag loc 1 msg :: diags in

to

let diags = build_error_diagnotic ~ast ~msg ... :: diags in

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:07):

Shachar Itzhaky said:

what does --std mean?

Yup, that meant don't put extra custom fields in the json

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:07):

we don't need that now thanks to LSP supporting this in most requests

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:08):

Also the devs will add a range parameter to the diagnostics requests in 3.18, so we can implement the viewport view with standard calls

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:08):

I'll take care of the update of the root state then

view this post on Zulip Shachar Itzhaky (Oct 17 2022 at 11:08):

cool

view this post on Zulip Shachar Itzhaky (Oct 17 2022 at 11:34):

btw pls merge the cleanup branch whenever you want

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 16:53):

Done, lsp branch updated too

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 16:53):

now it includes https://github.com/ejgallego/coq-lsp/pull/65

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 16:54):

note that vendor/coq-lsp/fleche/config.ml:ok_diag is now set to false, that means we don't send an OK diagnostic, instead for vscode we are thinking of using the same mechanism than lean

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 16:54):

c.f. https://github.com/leanprover/lean4/issues/503

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 16:55):

we don't emit that yet but will soon, we can do as we prefer tho

view this post on Zulip Shachar Itzhaky (Oct 17 2022 at 17:07):

if you don't send the OK, then how are the goals going to show?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 17:19):

Goals are shown on a request, aren't they?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 17:20):

Thing is that using diagnostics to highlight the background / show progress was a bit sketchy, and for example vscode caps the number of diags to 1000

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 17:21):

it is ok if we want to do like that tho

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 17:21):

but the lean method is a bit more compact and I guess we could derive the highlighing from the range report

view this post on Zulip Shachar Itzhaky (Oct 17 2022 at 17:22):

I felt like I wanted to also show some visual cue that there are goals to be had, like the yellow highlighting

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 17:24):

Sounds reasonable, for now then just flip the flag on config

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 17:24):

we can avoid these problems as we will pass the viewport to update

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 17:25):

for now we can survive sending all the diags

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 17:25):

there are two models for diags, pull and push, for systems like coq seems like pull is the best, but that's not a problem for us IMO

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 11:09):

Shachar is it correct that for the auto require code we could remove the roundtrip to the client in the wacoq backend?

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 13:48):

Assuming that we make the worker aware of packages, then yes. Currently the client holds the list of packages, so only the client can know which coq-pkg's to load.

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 13:48):

but this we can change, and then the only thing we need is to report to the UI the loading progress.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 16:07):

Shachar Itzhaky said:

but this we can change, and then the only thing we need is to report to the UI the loading progress.

Is that something we want?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 16:08):

If we are gonna hook into loadpath I guess so

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 18:19):

ok the thing is now loading the packages, the part that I'm missing is setting the loadpath

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 19:17):

I pushed it. Right now it re-inits which is ugly and causes an anomaly but at least shows that the libraries were loaded.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 19:42):

Great

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 19:42):

I will have a look

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 19:42):

I think reinit is the right approach here, what would you like to happen

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 19:43):

the way Coq code is structured, loadpath is set by command line args

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 19:43):

option B is to indeed get rid of loadpath at all

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 19:44):

and option C is to inject it somehow, but reinit is the same than to update the initial state

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 19:44):

let me see something tho

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 19:46):

Indeed, as I suspected

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 19:47):

note the discrepancy here

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 19:47):

let create_doc (doc_opts : doc_options) =
  let opts =
    { Icoq.uri = "file:///browser.v"
    ; opt_values = []
    ; vo_path = mk_vo_path !opts.lib_path
    ; require_libs  = Jslib.require_libs doc_opts.lib_init;
    }
  in
  Icoq.new_doc opts

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 19:47):

newdoc should take the loadpath, the underlying fleche engine already takes it

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 19:47):

it is just laziness on my part not to update this

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 19:48):

[didn't see the push btw]

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:01):

I fixed the init code, let me know if I can push

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 20:01):

I pushed the commit that was missing

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:01):

ok I will rebase

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:01):

one sec

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:02):

thanks

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:04):

huhu it works tho the anomaly is still there

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:05):

ha

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:05):

I understand

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:06):

don't re-issue coq.init on package loading

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:06):

that's the anomaly

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:06):

so we just need to split coqInit in two

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:06):

coqInit and docInit

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 20:06):

yes I already did that

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:06):

then just call docInit when the packages have been re-loaded

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 20:06):

but then I saw that the lib_path is actually in the init_opts

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:06):

yes

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:06):

I've fixed that

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 20:07):

ok so now we can call this.coq.newDoc

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:07):

yup, in handleMissing

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:08):

You wanna fix it? I can do it too

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 20:10):

ok yeah I can fix it

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:10):

thanks; maybe indeed docInit can be called from the Ready handler

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:10):

but it seems to me we got this working, and not in the worst way

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:11):

whether to do the roundtrip is not a big deal

view this post on Zulip Shachar Itzhaky (Oct 18 2022 at 20:12):

it would be pretty easy to move the logic if we manage to put the package handler in the worker

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:12):

Yup

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2022 at 20:12):

the roundtrip is pretty harmless in this case IMO

view this post on Zulip Shachar Itzhaky (Oct 19 2022 at 12:00):

In a sense we can save up on the loading of the prelude by saving that state after the prelude load and setting the loadpath there instead of creating a new doc. Don't know if we want to get into that; but if init_libs is large this could be a bit slow.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 13:20):

The thing is that as of today, loading of the prelude depends on the loadpath state. So we can optimize some, but in the general case you'd be unsound. But yes, it can be slow.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 13:21):

On the other hand if make loadpath something the document manager controls, then all of the loading is caching and the perf impact of the feature is 0

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 14:50):

You could always run coqdep before loading for example, and then automatically set the lib_path ?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 14:51):

so there are many intermediate state

view this post on Zulip Shachar Itzhaky (Oct 19 2022 at 16:20):

yes that was my original idea. but yeah nvm using the diag extras works

view this post on Zulip Shachar Itzhaky (Oct 19 2022 at 16:20):

I even show a yellow block where the pending Require is. I will push that.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 16:48):

Shachar Itzhaky said:

yes that was my original idea. but yeah nvm using the diag extras works

Yup, tho the coqdep stuff can be a nice optimization; still the current setup is a bit ineffcieint in that fleche will try to process the whole document, but once we add the range parameter to update only what's in view (and before) should be checked, so that should work much better

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 16:48):

Making require independent of loadpath is still on the roadmap as it is IMO very useful (and even superseedes coqdep)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 17:26):

what's next on the TODO @Shachar Itzhaky ?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 17:27):

I have quite a few cleanups on the line, but I think none of them essential

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 17:59):

I've enabled type-checking for backend on the js frontend, maybe you wanna have a look, I'm unsure if what I did makes sense

view this post on Zulip Shachar Itzhaky (Oct 19 2022 at 18:11):

definitely showing the errors

view this post on Zulip Shachar Itzhaky (Oct 19 2022 at 18:13):

w8 is it ok to remove the .js in imports? I thought the browser doesn't like it. Or do you mean that you have changed it to load the webpacked frontend as well

view this post on Zulip Shachar Itzhaky (Oct 19 2022 at 20:18):

my chrome errors out on that.. I'm putting the .js back

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:15):

Ahhh, I only checked that the frontend webpack was OK

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:15):

So there is now way to get vscode check the frontend .js files with the TS types of the backend?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:16):

A (not pretty at all) solution we can do for the browser to like this setup (apart of course of loading the packed frontend) is to provide the module map

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:16):

dunno if that would work, but I def want type-checking on the js files

view this post on Zulip Shachar Itzhaky (Oct 19 2022 at 21:18):

hmm I assume we can provide typings even when the module is imported as backend.js

view this post on Zulip Shachar Itzhaky (Oct 19 2022 at 21:18):

need to try

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:29):

I didn't manage unfortunately :S but yeah likely there is a way; would be cool indeed to see the types.

Maybe it is just time we move the frontend to .ts too ?

view this post on Zulip Shachar Itzhaky (Oct 19 2022 at 21:42):

yeah maybe

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:44):

I liked how we had the js files, maybe we can just add the module map for backend

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:44):

assuming that solves the issue

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 17:12):

Do we know how to make the stderr printing to show in the wacoq backend?

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 17:19):

hmm it should be in the js console I think?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 17:33):

oh yes, thanks! I will add an option to display it in the main log

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 17:33):

so how are we doing in this front?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 17:33):

we need to attach the diags to snippets, but that is?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 17:34):

I think for goals would make sense to be a bit more discoverable?

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 17:49):

yes all of the above. we need to fix the quick help because now it says use up/down which is not what it does. also we need a goal cursor (plus an option to always move with cursor if ppl are used to that from lean)
and I think we can show the error & info diagnostics in the goal area when the cursor is on the mark. I don't really like error on hover like in vscode.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 24 2023 at 23:37):

Ok folks, I did quite a bit of work these last days in coq-lsp and Flèche, the result is a new up to date tree, and build system replacing dog-slow webpack. Still the coq-pkg build is painfully slow, but at least dune is caching and promoting most things now.

The way I see the roadmap now is:

then there is some more janitorial stuff to do w.r.t. workspace / package handling consolidation among the 3 (yes jsCoq waCoq coq-lsp) systems, but coq-lsp 0.2 should have the right workspace tools as to allow a backing filesystem than jsCoq can use.

Still waiting to make some progress on the ProseMirror + Curvenote schema, but that's kind of orthogonal.

view this post on Zulip Shachar Itzhaky (Jan 25 2023 at 09:21):

oh nice! we can probably set up an artificial cache for coq-pkgs; or, we can have targets that only rebuild the worker+frontend.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2023 at 13:15):

Caching sounds nice yes! Actually dune should cache it but I guess our dep chain is too strict. In fact, as the build targets are directories I did split them in 3:

Then we have coq-pkgs which depends on the cli.
Note that all the main targets now seem to be promoted to the source tree so that makes it easier to do some JS stuff directly.

I didn't do any perf metric but packing seems to make things faster client side also.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2023 at 13:18):

The TL;DR is that now make wacoq while developing should be very very fast, and usable as watch mode for the frontend, so developing with the bundler is IMHO finally feasible.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 30 2023 at 18:41):

@Ramkumar Ramachandra , I think I've found the solution, pass both an event handler and a synthetic Event to forward the worker results. Can I push that change?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 30 2023 at 21:00):

Ok @Ramkumar Ramachandra , releasing the lock for today.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 30 2023 at 21:00):

The event structure is in place, so indeed now all we lack is a way to connect to the editor.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 28 2023 at 15:43):

@Shachar Itzhaky I'm gonna push some more changes

view this post on Zulip Shachar Itzhaky (Jul 28 2023 at 15:44):

ok I am trying to restore the CLI because the examples page of the website does not build right now

view this post on Zulip Emilio Jesús Gallego Arias (Jul 28 2023 at 15:45):

What is the problem? I can load examples/inf_primes.html right but I need mathcomp.js and the node_modules/@jscoq/mathcomp files to be there.

view this post on Zulip Shachar Itzhaky (Jul 28 2023 at 15:47):

it is needed for building examples.coq-pkg

view this post on Zulip Shachar Itzhaky (Jul 28 2023 at 15:48):

I think that one is needed by sqrt2?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 28 2023 at 22:17):

Ok let me have a look, thanks. I did some more work on the branch and IMHO it is ready to be merged in 8.17 so and ready to start work on the rest of the TODOs

I did separate the .coq-pkg builder from the CLI for now, to sped up the build, and maybe rework the CLI a little bit.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 29 2023 at 15:06):

examples.coq-pkg build fixed in the last commit of the lsp branch

view this post on Zulip Emilio Jesús Gallego Arias (Jul 29 2023 at 15:07):

symb files do remain broken

view this post on Zulip Emilio Jesús Gallego Arias (Jul 29 2023 at 15:07):

that should be not too hard to fix, tho I wonder if we should not just make jscoq.cli a LSP client

view this post on Zulip Emilio Jesús Gallego Arias (Jul 29 2023 at 15:09):

So the v8.16+branch looks pretty good IMO, I added a show goals on click setting and it works like a charm across all the 3 editors.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 29 2023 at 15:10):

I think I'm gonna go to coq-lsp and implement the workspace setting and some other improvements needed in jscoq

view this post on Zulip Emilio Jesús Gallego Arias (Aug 09 2023 at 13:00):

Ok, the default branch is now 8.17+lsp , I'm gonna merge the branch

view this post on Zulip Emilio Jesús Gallego Arias (Aug 09 2023 at 13:03):

@Shachar Itzhaky I'm gonna rebase https://github.com/jscoq/jscoq/pull/336 , can I take the lock for a couple of minutes?

view this post on Zulip Shachar Itzhaky (Aug 09 2023 at 13:04):

sure

view this post on Zulip Shachar Itzhaky (Aug 09 2023 at 13:04):

so I will have to do a soft reset afterwards?

view this post on Zulip Emilio Jesús Gallego Arias (Aug 09 2023 at 13:08):

git fetch --all -p && git reset --hard $remote/v8.17+lsp+goalview should do the trick, provided you have no local changes, otherwise do a rebase instead of the reset

view this post on Zulip Emilio Jesús Gallego Arias (Aug 09 2023 at 13:16):

@Shachar Itzhaky so we now have the goal view PR and the editor swap PR, let me know if you wanna do a quick call to discuss about the plans.

My plan for now is:

view this post on Zulip Emilio Jesús Gallego Arias (Aug 09 2023 at 13:18):

I have the old CM5 mode almost working, all I do is on top of #338 , find the generated textareas, and launch the code mirror manager

view this post on Zulip Emilio Jesús Gallego Arias (Aug 09 2023 at 13:18):

only thing missing is that I don't synchronize changes made in the CM5 multi-snippet view back to the markdown view

view this post on Zulip Emilio Jesús Gallego Arias (Aug 09 2023 at 13:22):

that will require some changes to the document model, that is a big headache due to the way we do ProseMirror. Due to this the new CoqDocument class needs to represent the document both in Coq view and document view, and editors like Prosemirror find the view to be different. I guess at some point having Flèche to understand ProseMirror offset system could be easier, but Flèche would need to parse the Markdown to the model the editor is using, that seems fragile. Maybe the most maintenable solution would be to make Prosemirror talk in line/columns instead of offsets, but that's also tricky.

Let's think about it.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 09 2023 at 13:23):

I suggest for now we try to merge the new goal view, or if we are not happy about it, let's discuss what kind of view we'd like to have.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 09 2023 at 13:25):

Note that the shared goal view between jsCoq and the coq-lsp vsCode extension needs support for extension as we did for the contextual info, for example Bhakti's amazing QWire visualizer uses it, so we can have people develop extensions that work fine in both setting. That's IMHO a nice thing.


Last updated: Mar 28 2024 at 22:01 UTC