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
Where is your .opam folder?
It might be possible that opam marks the installed area as read only.
coq-lsp really shouldn't be writing logs there anyway.
I don't think anything would be read or written from /
I'll try on my system too
Ah wait is this during running?
Actually, I didn't even install, I just ran
dune exec in
editor/code as advised
are you in the coq-lsp repo?
You don't need to do
dune exec if you have isntalled it
If you installed the extension for vscode correctly you should be able to run it
The dune exec business is for getting the local dev build of coq-lsp into PATH for code
You can get the extension from the extensions window of vscode
Just search coq you will find it
We should updating the install instructions in the main repo:
Seems changes haven't propagated yet,
opam info coq-lsp still fails after
opam update unless I use a local git checkout (
<><> 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
opam remote set-url default git+https://github.com/ocaml/opam-repository
if you are impatient
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
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
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)
I think we are on OSX here
Yep, OS X here, I wouldn't trust it to be like Linux
And still no coq-lsp after
opam update, that seems long
But it's in the git repo indeed
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?
Those are not a problem, just artifacts of how serapi loads stuff.
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
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