Emilio Jesús Gallego Arias (Jan 22 2023 at 17:51): Emilio Jesús Gallego Arias (Jan 22 2023 at 17:51):Hi folks, I'm thinking of going ahead with 0.1.4 soon, Unicode support is quite important feature.
The rendering PR is still not working, I think I understand why but I also think that to fix that, the whole goal render setup has to be rewritten, this time properly. I'm gonna give it a go.
What do you think?
Ali Caglayan (Jan 22 2023 at 18:40):Do we have a meeting tomorrow?
Emilio Jesús Gallego Arias (Jan 22 2023 at 20:10):Why not?
Ali Caglayan (Jan 22 2023 at 20:12):Then lets discuss during the meeting.
Emilio Jesús Gallego Arias (Jan 22 2023 at 20:39):Ok sounds good, can you update the wiki then?
Emilio Jesús Gallego Arias (Jan 23 2023 at 15:57):Let's use zoom, I'll put a link in 2 mins
Emilio Jesús Gallego Arias (Jan 23 2023 at 15:59):Renater works today, let's use that
Emilio Jesús Gallego Arias (Jan 27 2023 at 17:03):@Ali Caglayan , I think the 0.1.4 milestone is in final form for a release very soon.
Ali Caglayan (Jan 27 2023 at 17:04):Yes, there is nothing else I wish to cram into it
Ali Caglayan (Jan 27 2023 at 17:04):Were you going to do the react stuff?
Emilio Jesús Gallego Arias (Jan 27 2023 at 17:13):yes it is done, merging now
Emilio Jesús Gallego Arias (Jan 27 2023 at 17:13):tweaking the css stuff as we speak
Emilio Jesús Gallego Arias (Jan 27 2023 at 17:13):as we talk
Emilio Jesús Gallego Arias (Jan 29 2023 at 13:06):@Ali Caglayan if you still get a backtrace we can't release like that, you should not get a backtrace because the server does validate the input
Emilio Jesús Gallego Arias (Jan 29 2023 at 13:06):So some stuff is wrong in the server. Can you post the backtrace?
Ali Caglayan (Jan 29 2023 at 13:47):IIRC it was coming from the same place
Ali Caglayan (Jan 29 2023 at 13:47):We should write an expect test for that
Ali Caglayan (Jan 29 2023 at 13:48):First do one with a correct document and location
Ali Caglayan (Jan 29 2023 at 13:48):Then do one with a stake doc and see the error
Emilio Jesús Gallego Arias (Jan 29 2023 at 13:51):That's the thing, I can't understand how the error could possibly happen
Emilio Jesús Gallego Arias (Jan 29 2023 at 13:52):What's the backtrace with master?
Emilio Jesús Gallego Arias (Jan 29 2023 at 13:52):and the request parameters / document
Emilio Jesús Gallego Arias (Jan 29 2023 at 13:56):I just did a bunch of unit tests and indeed I can't see a backtrace happening, so I'm very confused
Emilio Jesús Gallego Arias (Jan 29 2023 at 14:19):Never mind I understand now, of course we return the length of the string, that is silly.
Matthieu Sozeau (Feb 06 2023 at 15:40):No 0.1.4 for Coq 8.16? I would have liked to have a look at it :)
Matthieu Sozeau (Feb 06 2023 at 15:40):Right now if I have 0.1.2 and the 0.1.4 vscode extension goal printing doesn't work
Matthieu Sozeau (Feb 06 2023 at 15:41):Also, it would be great to have the option to set OCAMLPATH for the execution of coq-lsp, in MetaCoq we have a META file that's not yet installed when building later folders
Ali Caglayan (Feb 06 2023 at 15:56):We have 0.1.4 for 8.16: https://github.com/ejgallego/coq-lsp/releases/tag/0.1.4%2Bv8.16
Ali Caglayan (Feb 06 2023 at 15:57):@Emilio Jesús Gallego Arias did you do an opam release for it?
Emilio Jesús Gallego Arias (Feb 06 2023 at 16:12):Yes it is in opam
Emilio Jesús Gallego Arias (Feb 06 2023 at 16:12):https://opam.ocaml.org/packages/coq-lsp/
Emilio Jesús Gallego Arias (Feb 06 2023 at 16:13):Matthieu Sozeau said:
Also, it would be great to have the option to set OCAMLPATH for the execution of coq-lsp, in MetaCoq we have a META file that's not yet installed when building later folders
I'll look into that, thanks for the heads up
Emilio Jesús Gallego Arias (Feb 06 2023 at 16:13):By the way we have improved the goal printing compat story, now it should work better across versions
Notification Bot (Feb 22 2023 at 22:52):Emilio Jesús Gallego Arias has marked this topic as resolved.
Last updated: Apr 20 2024 at 07:01 UTC