Stream: coq-lsp

Topic: Log file problem?


view this post on Zulip Matthieu Sozeau (Nov 24 2022 at 15:34):

I'm getting this now:

coq-lsp: internal error, uncaught exception:
         Sys_error("log-lsp.txt: Read-only file system")
         Raised by primitive operation at Stdlib.open_out_gen in file "stdlib.ml", line 331, characters 29-55
         Called from Stdlib.open_out in file "stdlib.ml" (inlined), line 336, characters 2-74
         Called from Dune__exe__Coq_lsp.lsp_main in file "controller/coq_lsp.ml", line 404, characters 17-34
         Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
         Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 34, characters 37-44

After installing from source. It's unclear where it tries to write, probably at / or some other path that's non-writable for me

view this post on Zulip Ali Caglayan (Nov 24 2022 at 15:40):

Where is your .opam folder?

view this post on Zulip Ali Caglayan (Nov 24 2022 at 15:41):

It might be possible that opam marks the installed area as read only.

view this post on Zulip Ali Caglayan (Nov 24 2022 at 15:41):

coq-lsp really shouldn't be writing logs there anyway.

view this post on Zulip Ali Caglayan (Nov 24 2022 at 15:41):

I don't think anything would be read or written from /

view this post on Zulip Ali Caglayan (Nov 24 2022 at 15:42):

I'll try on my system too

view this post on Zulip Ali Caglayan (Nov 24 2022 at 15:51):

Ah wait is this during running?

view this post on Zulip Matthieu Sozeau (Nov 24 2022 at 15:51):

Actually, I didn't even install, I just ran dune exec in editor/code as advised

view this post on Zulip Ali Caglayan (Nov 24 2022 at 15:52):

are you in the coq-lsp repo?

view this post on Zulip Ali Caglayan (Nov 24 2022 at 15:54):

You don't need to do dune exec if you have isntalled it

view this post on Zulip Ali Caglayan (Nov 24 2022 at 15:54):

If you installed the extension for vscode correctly you should be able to run it

view this post on Zulip Ali Caglayan (Nov 24 2022 at 15:54):

The dune exec business is for getting the local dev build of coq-lsp into PATH for code

view this post on Zulip Ali Caglayan (Nov 24 2022 at 15:56):

You can get the extension from the extensions window of vscode

view this post on Zulip Ali Caglayan (Nov 24 2022 at 15:56):

Just search coq you will find it

view this post on Zulip Ali Caglayan (Nov 24 2022 at 15:57):

We should updating the install instructions in the main repo:

  1. opam install coq-lsp
  2. Instlal extension from VSCode store
  3. open a .v file in a project in VSCode

view this post on Zulip Paolo Giarrusso (Nov 24 2022 at 16:43):

Seems changes haven't propagated yet, opam info coq-lsp still fails after opam update unless I use a local git checkout (default-fork)

<><> Repository configuration for switch coq-8.16.01-ocaml-4.14.0+flambda <>  🐫
 1 default-fork git+file:///Users/pgiarrusso/git-bedrock/opam-repository
 2 iris-dev     git+https://gitlab.mpi-sws.org/iris/opam.git
 3 coq-released https://coq.inria.fr/opam/released
 4 default      https://opam.ocaml.org

view this post on Zulip Ali Caglayan (Nov 24 2022 at 17:56):

It takes a few hours

view this post on Zulip Ali Caglayan (Nov 24 2022 at 17:56):

opam remote set-url default git+https://github.com/ocaml/opam-repository

if you are impatient

view this post on Zulip Huỳnh Trần Khanh (Nov 24 2022 at 23:16):

Read-only file system

this answer might be unexpected. but this is an indication of hard disk failure. normally if you don't have the permissions to write, you get permission denied. linux remounts a file system as read only when it detects an inconsistency. it might be a good idea to back up your data

you have done all the other steps correctly, so I highly suspect this is the cause

view this post on Zulip Paolo Giarrusso (Nov 24 2022 at 23:30):

Possible, but one can also mount a file-system read-only intentionally via the ro option in /etc/fstab... IIRC such filesystem inconsistencies and remounting would be logged in dmesg, and at least cat /proc/mounts would tell which filesystems are read-only

view this post on Zulip Paolo Giarrusso (Nov 24 2022 at 23:31):

but good point that this isn't "permission denied" and can't be explained by missing permissions (technically, this is errno = EROFS, not errno = EPERM)

view this post on Zulip Enrico Tassi (Nov 25 2022 at 08:30):

I think we are on OSX here

view this post on Zulip Matthieu Sozeau (Nov 25 2022 at 09:07):

Yep, OS X here, I wouldn't trust it to be like Linux

view this post on Zulip Matthieu Sozeau (Nov 25 2022 at 09:09):

And still no coq-lsp after opam update, that seems long

view this post on Zulip Matthieu Sozeau (Nov 25 2022 at 09:22):

But it's in the git repo indeed

view this post on Zulip Matthieu Sozeau (Nov 25 2022 at 16:46):

It's working now with the opam package. I'm getting Missing serlib plugin: coq-equations.plugin messages, and similarly for Coq plugins, I guess that's not a problem?

view this post on Zulip Ali Caglayan (Nov 25 2022 at 22:34):

Those are not a problem, just artifacts of how serapi loads stuff.

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 02:43):

ah, my Mac indeed shows / is mounted read-only and reproduces the Read-only file system/Permission denied distinction

$ cat > /foo
-bash: /foo: Read-only file system
$ cat > /Users/foo
-bash: /Users/foo: Permission denied
$ mount
/dev/disk3s1s1 on / (apfs, sealed, local, read-only, journaled)
...

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

Indeed we were not careful enough, problem solved in main, will do a 0.1.1 release soon

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

Now if the log file can't be created we will notify to the user and don't crash


Last updated: Feb 06 2023 at 05:03 UTC