Matthieu Sozeau (Nov 24 2022 at 15:34): 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
Ali Caglayan (Nov 24 2022 at 15:40):Where is your .opam folder?
Ali Caglayan (Nov 24 2022 at 15:41):It might be possible that opam marks the installed area as read only.
Ali Caglayan (Nov 24 2022 at 15:41):coq-lsp really shouldn't be writing logs there anyway.
Ali Caglayan (Nov 24 2022 at 15:41):I don't think anything would be read or written from /
Ali Caglayan (Nov 24 2022 at 15:42):I'll try on my system too
Ali Caglayan (Nov 24 2022 at 15:51):Ah wait is this during running?
Matthieu Sozeau (Nov 24 2022 at 15:51):Actually, I didn't even install, I just ran dune exec in editor/code as advised
Ali Caglayan (Nov 24 2022 at 15:52):are you in the coq-lsp repo?
Ali Caglayan (Nov 24 2022 at 15:54):You don't need to do dune exec if you have isntalled it
Ali Caglayan (Nov 24 2022 at 15:54):If you installed the extension for vscode correctly you should be able to run it
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
Ali Caglayan (Nov 24 2022 at 15:56):You can get the extension from the extensions window of vscode
Ali Caglayan (Nov 24 2022 at 15:56):Just search coq you will find it
Ali Caglayan (Nov 24 2022 at 15:57):We should updating the install instructions in the main repo:
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
It takes a few hours
Ali Caglayan (Nov 24 2022 at 17:56):opam remote set-url default git+https://github.com/ocaml/opam-repository
if you are impatient
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
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
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)
Enrico Tassi (Nov 25 2022 at 08:30):I think we are on OSX here
Matthieu Sozeau (Nov 25 2022 at 09:07):Yep, OS X here, I wouldn't trust it to be like Linux
Matthieu Sozeau (Nov 25 2022 at 09:09):And still no coq-lsp after opam update, that seems long
Matthieu Sozeau (Nov 25 2022 at 09:22):But it's in the git repo indeed
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?
Ali Caglayan (Nov 25 2022 at 22:34):Those are not a problem, just artifacts of how serapi loads stuff.
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)
...
Indeed we were not careful enough, problem solved in main, will do a 0.1.1 release soon
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