Shachar Itzhaky (Sep 26 2022 at 18:53): 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.
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?
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.
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.
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.
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
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_typewith valuesCoqandMarkdown. 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?
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.
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
Emilio Jesús Gallego Arias (Sep 27 2022 at 22:21):I'm interested in resurrecting Interrupt
Emilio Jesús Gallego Arias (Sep 27 2022 at 23:31):It seems to work well, nothing to do there.
Emilio Jesús Gallego Arias (Sep 27 2022 at 23:31):Next I will do queue optimization
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.
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
Shachar Itzhaky (Sep 29 2022 at 12:37):I am wondering if there is a concept of mini-modes in LSP?
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
Shachar Itzhaky (Sep 29 2022 at 12:39):ideally we will use Emacs' markdown mode with a coq-lsp nested mode
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
Shachar Itzhaky (Sep 29 2022 at 17:26):how can this be
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?
Emilio Jesús Gallego Arias (Sep 29 2022 at 19:45):Indeed there is a problem!
Emilio Jesús Gallego Arias (Sep 29 2022 at 19:45):Yeah I was playing with that and committed a wrong version
Emilio Jesús Gallego Arias (Sep 29 2022 at 19:46):Still not sure what the best way is
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?)
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
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
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
Emilio Jesús Gallego Arias (Sep 29 2022 at 19:50):But yeah, I don't have yet a very concrete design in mind
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.
Emilio Jesús Gallego Arias (Sep 29 2022 at 20:51):Yes, actually the code in coq-lsp does reset the flag
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
Emilio Jesús Gallego Arias (Sep 29 2022 at 20:52):so yeah that's something to design
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
Emilio Jesús Gallego Arias (Sep 29 2022 at 20:57):By the way I have a patch to that require will callback
Emilio Jesús Gallego Arias (Sep 29 2022 at 20:57):however, that callback is still in the worker context
Emilio Jesús Gallego Arias (Sep 29 2022 at 20:58):Type is { from : DirPath.t option; dirpath : DirPath.t } -> Path.t Promise.t
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
Emilio Jesús Gallego Arias (Sep 29 2022 at 21:02):There are still two options possible for it:
Config call with the new loadpath, and an Update to recheckI'm not sure what approach would be best.
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.
Shachar Itzhaky (Sep 30 2022 at 14:56):Ok I have pushed a version with ProviderContainer for documents with multiple snippets as before.
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.
Shachar Itzhaky (Sep 30 2022 at 14:57):In the meantime I'm attempting to reconstruct waCoq on top of the new coq_interp
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
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.
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!
Shachar Itzhaky (Sep 30 2022 at 18:42):oh yes :)
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.
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?
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
Shachar Itzhaky (Sep 30 2022 at 18:44):ok yeah
Shachar Itzhaky (Sep 30 2022 at 18:44):I think most of the code in wacoq-bin will not be needed
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.
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"
Emilio Jesús Gallego Arias (Sep 30 2022 at 18:44):as the ones emacs has for snippets
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
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!)
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
Emilio Jesús Gallego Arias (Sep 30 2022 at 18:47):As you prefer, I think it should commute
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
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
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
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
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?
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_ocamlout 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
Emilio Jesús Gallego Arias (Sep 30 2022 at 18:50):yes
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
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
Shachar Itzhaky (Sep 30 2022 at 18:53):ok good, I think Monday would be ok
Emilio Jesús Gallego Arias (Sep 30 2022 at 19:06):good, I've pushed a branch moving the proto and interp to common
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
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
Emilio Jesús Gallego Arias (Oct 01 2022 at 08:08):@Shachar Itzhaky what was the motivation for moving it to the client?
Emilio Jesús Gallego Arias (Oct 01 2022 at 08:08):It seems waCoq moved it back to the server/worker?
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?
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?
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)
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?
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
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
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?
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
Shachar Itzhaky (Oct 01 2022 at 18:26):how did it work with jsoo? did you add stubs?
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.
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!
Emilio Jesús Gallego Arias (Oct 01 2022 at 22:58):I've never heard of that stub
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
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?
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.
Emilio Jesús Gallego Arias (Oct 03 2022 at 12:39):That's a good point about jsoo! I have no idea
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.
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.
Shachar Itzhaky (Oct 03 2022 at 12:59):camlzip is written in C. I believe we looked into it at some point.
Emilio Jesús Gallego Arias (Oct 03 2022 at 14:58):Yes, the pure one is decompress
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
Emilio Jesús Gallego Arias (Oct 03 2022 at 15:47):it is only two callbacks so I'm happy to wrap that
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
Emilio Jesús Gallego Arias (Oct 06 2022 at 14:40):things are looking really good!
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
Emilio Jesús Gallego Arias (Oct 06 2022 at 14:40):and I will push the curvenote stuff
Emilio Jesús Gallego Arias (Oct 06 2022 at 14:41):and at some point some other nits
Shachar Itzhaky (Oct 06 2022 at 15:43):oh wow you rebased over the interp_unify? and it worked??
Emilio Jesús Gallego Arias (Oct 06 2022 at 15:48):didn't try wacoq as I ran out of time
Emilio Jesús Gallego Arias (Oct 06 2022 at 15:48):but builds
Emilio Jesús Gallego Arias (Oct 06 2022 at 15:49):It should work, provided the loader works
Shachar Itzhaky (Oct 06 2022 at 15:49):lol
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
Emilio Jesús Gallego Arias (Oct 06 2022 at 15:49):but it does!
Shachar Itzhaky (Oct 06 2022 at 15:49):ok I'll try it!
Shachar Itzhaky (Oct 06 2022 at 17:55):Hmm it is trying to load coq-serapi.serlib.ltac via findlib
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?
Shachar Itzhaky (Oct 06 2022 at 21:02):Also all error msgs in waCoq have a gazillion times this string: "Called from unknown location"
Emilio Jesús Gallego Arias (Oct 07 2022 at 12:38):That's lack of backtraces? Strange
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
Emilio Jesús Gallego Arias (Oct 07 2022 at 12:38):It is a mystery I need to research
Emilio Jesús Gallego Arias (Oct 07 2022 at 12:39):the code in question is here
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
Emilio Jesús Gallego Arias (Oct 07 2022 at 12:45):maybe try the same?
Emilio Jesús Gallego Arias (Oct 07 2022 at 12:45):haha
Emilio Jesús Gallego Arias (Oct 07 2022 at 12:45):I just refuse to load anything not from the legacy method
Emilio Jesús Gallego Arias (Oct 07 2022 at 12:45):but it is really a mystery why that is working
Emilio Jesús Gallego Arias (Oct 07 2022 at 12:46):it should not unless we linked the serlib thing statically somewhere
Emilio Jesús Gallego Arias (Oct 07 2022 at 12:46):before we did
Emilio Jesús Gallego Arias (Oct 07 2022 at 12:46):but after I removed the serapi dep we should not
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"
Emilio Jesús Gallego Arias (Oct 07 2022 at 13:02):as the libraries implement the cache-optimized ops
Emilio Jesús Gallego Arias (Oct 07 2022 at 13:02):but we don't
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
Emilio Jesús Gallego Arias (Oct 07 2022 at 14:31):I've pushed a better plugin loding setup to the branch
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
Emilio Jesús Gallego Arias (Oct 07 2022 at 15:31):Indeed, the mystery is solved: we used to link serlib.ltac statically.
Emilio Jesús Gallego Arias (Oct 07 2022 at 15:31):Now we don't
Emilio Jesús Gallego Arias (Oct 07 2022 at 15:31):I'll push a patch to hopefully fix wacoq for now tho.
Shachar Itzhaky (Oct 07 2022 at 18:24):Oh actually now it fails with (Sys_error "/home/ltac_plugin: No such file or directory")
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!
Shachar Itzhaky (Oct 07 2022 at 18:25):then all you need to do is set backend: 'wa' in the options
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:31):Great!!
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
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:32):Mmmm
Shachar Itzhaky (Oct 08 2022 at 13:32):ok but ltac_plugin is using legacy mode and is in path
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
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:32):that didn't work in jsoo
Shachar Itzhaky (Oct 08 2022 at 13:32):actually I did not get this message before your last patch
Shachar Itzhaky (Oct 08 2022 at 13:33):in wasm it can scan the path and find the right one usually
Shachar Itzhaky (Oct 08 2022 at 13:33):no idea why it is trying /home
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:33):Oh
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:34):Indeed my patch is buggy in this sense
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:34):That's what Coq does if not mltop is set
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
Ok so replace the code in load_module for something like
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
Where !coq_mlpath_copy should be the search path
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
Shachar Itzhaky (Oct 08 2022 at 13:36):ok, it looks weird that we cannot call the "normal" top's load_module
Shachar Itzhaky (Oct 08 2022 at 13:36):so you need to duplicate it
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:36):Yes that's a problem in the API
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:36):You have to set both
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
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:37):but the path resolution procedure
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:37):the pity is that indeed we cannot just disable the findlib loader
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:38):Or just patch Coq to explose Mltop.PluginSpec.load
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:38):and use it
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:38):Yeah easier is just to do load_module = Mltop.PluginSpec.load
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:38):and export that in mltop.mli
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:38): val load : t -> unit
Shachar Itzhaky (Oct 08 2022 at 13:39):ok that sounds like a valid patch
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
load_module should be for loading a .cma directly, no?
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:50):Oh yes, damn
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:50):indeed it registers the loaded module with findlib
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
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.
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:51):Was an attempt to allow more flexibility to the caller
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:51):We can for now just indeed use the longer version :S
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
Shachar Itzhaky (Oct 08 2022 at 14:16):I have a conf already
Shachar Itzhaky (Oct 08 2022 at 14:16):it has this: path="/lib/ocaml"
Shachar Itzhaky (Oct 08 2022 at 14:16):findlib in wasm seems to find it
Shachar Itzhaky (Oct 08 2022 at 15:02):are you no longer using the Loader module from coq-lsp?
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?
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
Emilio Jesús Gallego Arias (Oct 08 2022 at 23:41):likely we want to tweak the API a bit
Emilio Jesús Gallego Arias (Oct 08 2022 at 23:42):all the loader module does is to load instrumentation plugins
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 inis 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
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
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
Shachar Itzhaky (Oct 09 2022 at 05:47):oh I thought this was the same code that is used for vscode
Emilio Jesús Gallego Arias (Oct 09 2022 at 16:28):coq-lsp just always uses findlib
Emilio Jesús Gallego Arias (Oct 09 2022 at 16:29):Actually load_module is irrelevant for us, I remeber why it is there
Emilio Jesús Gallego Arias (Oct 09 2022 at 16:30):The native compiler needs it to load the JITed modules
Emilio Jesús Gallego Arias (Oct 09 2022 at 16:30):so it is always load_plugin
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?
Emilio Jesús Gallego Arias (Oct 09 2022 at 19:13):coq-lsp is using this change
Emilio Jesús Gallego Arias (Oct 09 2022 at 19:14):but it sets up the loader differently
Emilio Jesús Gallego Arias (Oct 09 2022 at 19:14):As it assumes a working findlib
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
Emilio Jesús Gallego Arias (Oct 09 2022 at 19:51):Pushed a patch that should fix wacoq
Shachar Itzhaky (Oct 09 2022 at 20:35):ok cool!
Shachar Itzhaky (Oct 09 2022 at 20:37):oh you've put it in load_plugin
Shachar Itzhaky (Oct 09 2022 at 20:37):alright that might be better in fact
Emilio Jesús Gallego Arias (Oct 09 2022 at 20:45):Yes, load_module is unused actually
Emilio Jesús Gallego Arias (Oct 09 2022 at 20:45):it is only there for the native compiler which we don't use
Emilio Jesús Gallego Arias (Oct 09 2022 at 20:45):and still needs to call Dynload directly
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
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
Emilio Jesús Gallego Arias (Oct 09 2022 at 20:46):but I bet getting findlib to work in wacoq is easy
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
Emilio Jesús Gallego Arias (Oct 09 2022 at 20:47):like elpi
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
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
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
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
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
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
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
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
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 -> ())
}
tho that's set in icoq.ml, so it should be common for both?
Emilio Jesús Gallego Arias (Oct 09 2022 at 20:58):You are missing the "cache hit messages" etc... right?
Shachar Itzhaky (Oct 09 2022 at 20:58):yeah
Emilio Jesús Gallego Arias (Oct 09 2022 at 20:58):They are sent to this callback
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
Shachar Itzhaky (Oct 09 2022 at 20:58):I have seen eprintfs before
Shachar Itzhaky (Oct 09 2022 at 20:59):alright I'll check it tomorrow
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 :)
Emilio Jesús Gallego Arias (Oct 09 2022 at 21:00):Oh that's cool!
Emilio Jesús Gallego Arias (Oct 09 2022 at 21:01):yeah in jsoo we post a Log even for each stdout / stderr
Emilio Jesús Gallego Arias (Oct 09 2022 at 21:01):So to find the deps of a plugin
Emilio Jesús Gallego Arias (Oct 09 2022 at 21:01):provided the plugin did install its META correctly
Emilio Jesús Gallego Arias (Oct 09 2022 at 21:02):you do this
Emilio Jesús Gallego Arias (Oct 09 2022 at 21:03):ocamlfind query $pkg -r
Emilio Jesús Gallego Arias (Oct 09 2022 at 21:03):for elpi it gives
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
oh cool that's precisely what I need
Emilio Jesús Gallego Arias (Oct 09 2022 at 21:04):yes
Shachar Itzhaky (Oct 09 2022 at 21:04):that is in fact the list that I constructed manually before ;))
Shachar Itzhaky (Oct 09 2022 at 21:04):ok perfect
Shachar Itzhaky (Oct 09 2022 at 21:05):gnight then :)
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
Emilio Jesús Gallego Arias (Oct 09 2022 at 21:07):good night!
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
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?
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.
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
Emilio Jesús Gallego Arias (Oct 17 2022 at 10:49):In the current model there is little the client can do about this
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]
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?
Shachar Itzhaky (Oct 17 2022 at 10:56):and another issue that we had is how to update the loadpath in the starting state
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
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
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
Emilio Jesús Gallego Arias (Oct 17 2022 at 11:01):so then we have something like:
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
Emilio Jesús Gallego Arias (Oct 17 2022 at 11:02):the update of the initial state should have fleche recheck everything
Shachar Itzhaky (Oct 17 2022 at 11:02):ok but this state is now inside coq-lsp so it's hard to access
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
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
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
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
Shachar Itzhaky (Oct 17 2022 at 11:04):ok let me start by taking a look at the require ast
Emilio Jesús Gallego Arias (Oct 17 2022 at 11:04):great
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
Emilio Jesús Gallego Arias (Oct 17 2022 at 11:05):with a modular build_error_diagnostic function
Shachar Itzhaky (Oct 17 2022 at 11:05):ok cool
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
Emilio Jesús Gallego Arias (Oct 17 2022 at 11:05):at some point we will add error codes, etc...
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
Shachar Itzhaky (Oct 17 2022 at 11:06):what does --std mean?
Shachar Itzhaky (Oct 17 2022 at 11:06):avoid non-standard attributes?
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
Shachar Itzhaky said:
what does
--stdmean?
Yup, that meant don't put extra custom fields in the json
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
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
Emilio Jesús Gallego Arias (Oct 17 2022 at 11:08):I'll take care of the update of the root state then
Shachar Itzhaky (Oct 17 2022 at 11:08):cool
Shachar Itzhaky (Oct 17 2022 at 11:34):btw pls merge the cleanup branch whenever you want
Emilio Jesús Gallego Arias (Oct 17 2022 at 16:53):Done, lsp branch updated too
Emilio Jesús Gallego Arias (Oct 17 2022 at 16:53):now it includes https://github.com/ejgallego/coq-lsp/pull/65
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
Emilio Jesús Gallego Arias (Oct 17 2022 at 16:54):c.f. https://github.com/leanprover/lean4/issues/503
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
Shachar Itzhaky (Oct 17 2022 at 17:07):if you don't send the OK, then how are the goals going to show?
Emilio Jesús Gallego Arias (Oct 17 2022 at 17:19):Goals are shown on a request, aren't they?
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
Emilio Jesús Gallego Arias (Oct 17 2022 at 17:21):it is ok if we want to do like that tho
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
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
Emilio Jesús Gallego Arias (Oct 17 2022 at 17:24):Sounds reasonable, for now then just flip the flag on config
Emilio Jesús Gallego Arias (Oct 17 2022 at 17:24):we can avoid these problems as we will pass the viewport to update
Emilio Jesús Gallego Arias (Oct 17 2022 at 17:25):for now we can survive sending all the diags
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
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?
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.
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.
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?
Emilio Jesús Gallego Arias (Oct 18 2022 at 16:08):If we are gonna hook into loadpath I guess so
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
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.
Emilio Jesús Gallego Arias (Oct 18 2022 at 19:42):Great
Emilio Jesús Gallego Arias (Oct 18 2022 at 19:42):I will have a look
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
Emilio Jesús Gallego Arias (Oct 18 2022 at 19:43):the way Coq code is structured, loadpath is set by command line args
Emilio Jesús Gallego Arias (Oct 18 2022 at 19:43):option B is to indeed get rid of loadpath at all
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
Emilio Jesús Gallego Arias (Oct 18 2022 at 19:44):let me see something tho
Emilio Jesús Gallego Arias (Oct 18 2022 at 19:46):Indeed, as I suspected
Emilio Jesús Gallego Arias (Oct 18 2022 at 19:47):note the discrepancy here
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
newdoc should take the loadpath, the underlying fleche engine already takes it
Emilio Jesús Gallego Arias (Oct 18 2022 at 19:47):it is just laziness on my part not to update this
Emilio Jesús Gallego Arias (Oct 18 2022 at 19:48):[didn't see the push btw]
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:01):I fixed the init code, let me know if I can push
Shachar Itzhaky (Oct 18 2022 at 20:01):I pushed the commit that was missing
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:01):ok I will rebase
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:01):one sec
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:02):thanks
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:04):huhu it works tho the anomaly is still there
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:05):ha
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:05):I understand
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:06):don't re-issue coq.init on package loading
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:06):that's the anomaly
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:06):so we just need to split coqInit in two
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:06):coqInit and docInit
Shachar Itzhaky (Oct 18 2022 at 20:06):yes I already did that
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:06):then just call docInit when the packages have been re-loaded
Shachar Itzhaky (Oct 18 2022 at 20:06):but then I saw that the lib_path is actually in the init_opts
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:06):yes
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:06):I've fixed that
Shachar Itzhaky (Oct 18 2022 at 20:07):ok so now we can call this.coq.newDoc
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:07):yup, in handleMissing
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:08):You wanna fix it? I can do it too
Shachar Itzhaky (Oct 18 2022 at 20:10):ok yeah I can fix it
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:10):thanks; maybe indeed docInit can be called from the Ready handler
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
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:11):whether to do the roundtrip is not a big deal
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
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:12):Yup
Emilio Jesús Gallego Arias (Oct 18 2022 at 20:12):the roundtrip is pretty harmless in this case IMO
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.
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.
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
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 ?
Emilio Jesús Gallego Arias (Oct 19 2022 at 14:51):so there are many intermediate state
Shachar Itzhaky (Oct 19 2022 at 16:20):yes that was my original idea. but yeah nvm using the diag extras works
Shachar Itzhaky (Oct 19 2022 at 16:20):I even show a yellow block where the pending Require is. I will push that.
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
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)
Emilio Jesús Gallego Arias (Oct 19 2022 at 17:26):what's next on the TODO @Shachar Itzhaky ?
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
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
Shachar Itzhaky (Oct 19 2022 at 18:11):definitely showing the errors
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
Shachar Itzhaky (Oct 19 2022 at 20:18):my chrome errors out on that.. I'm putting the .js back
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:15):Ahhh, I only checked that the frontend webpack was OK
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?
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
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
Shachar Itzhaky (Oct 19 2022 at 21:18):hmm I assume we can provide typings even when the module is imported as backend.js
Shachar Itzhaky (Oct 19 2022 at 21:18):need to try
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 ?
Shachar Itzhaky (Oct 19 2022 at 21:42):yeah maybe
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
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:44):assuming that solves the issue
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?
Shachar Itzhaky (Nov 10 2022 at 17:19):hmm it should be in the js console I think?
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
Emilio Jesús Gallego Arias (Nov 10 2022 at 17:33):so how are we doing in this front?
Emilio Jesús Gallego Arias (Nov 10 2022 at 17:33):we need to attach the diags to snippets, but that is?
Emilio Jesús Gallego Arias (Nov 10 2022 at 17:34):I think for goals would make sense to be a bit more discoverable?
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.
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.
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.
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:
dist target: builds wacoq_worker.html and frontend.html , that builds very very fast in the last dist-cli: builds cli.ts , which as of today requires the .bc.js binary which is very slow to build due to jsoo 4.0 (jsoo 5.0 may be much faster)dist-webpack: for the vue stuff, which is still using webpack.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.
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.
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?
Emilio Jesús Gallego Arias (Jan 30 2023 at 21:00):Ok @Ramkumar Ramachandra , releasing the lock for today.
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.
Last updated: May 31 2023 at 10:01 UTC