PG
PG copied to clipboard
ProofGeneral
Library compilation failed
OS: Ubuntu Linux 20.04 The Coq Proof Assistant, version 8.18.0 compiled with OCaml 4.14.1
coq is installed via snap into directory /snap/bin
coqc -where gives /snap/coq-prover/34/coq-platform/lib/coq
I set the following variables into Emacs config:
(setq exec-path (append exec-path '("/snap/bin")))
(setq coq-prog-name "/snap/bin/coqtop")
(setq coq-load-path '("/snap/coq-prover/34/coq-platform/lib/coq"))
But unfortunately, when I open a .v file and try to execute coq over it it fails on line:
Require Import List.
With errors:
Library compilation failed
-*- mode: compilation; -*-
coqdep /tmp/ProofGeneral-coqp2nTIp.v
*** Error: /tmp/ProofGeneral-coqp2nTIp.v: No such file or directory
Seems, that it is unable to find the directory with coq libraries. What should I do?
AFAIU the error means that the file ProofGeneral-coqp2nTIp.v that PG just wrote to find the dependencies of Require Import List. did not exist just after PG wrote that file.
The documentation of coq-load-path says "Under normal circumstances this list does not need to contain the coq standard library", so please delete your setting of coq-load-path.
I can no reproduce your problem yet, I therefore cannot give precise advise.
From the error message I deduce that you enabled Auto Compilation - please describe how.
Please check that the directory /tmp does exist and that you have write and search permissions there.
If the error persists, please include (setq coq--debug-auto-compilation t) in your Emacs config. This causes a lot of diagnostic messages in *Message*, please report them here.
I would be interested which piece in the documentation lead you to set coq-load-path with the standard library directory, so that we can improve this point.
When I try to start Coq 8.18 or 8.19 with coq-load-path set to its standard library, then coqtop aborts with an error and PG does not even start to process the current buffer.
With that wrong coq-load-path setting, can you process something very trivial, such as Definition a := 1.?
I would be interested which piece in the documentation lead you to set coq-load-path
It was chatGPT(!)
Can you confirm that you use Emacs 26.3?
My Emacs version: 28.1
Please check that the directory /tmp does exist and that you have write and search permissions there.
/$ ls -la / | grep tmp
drwxrwxrwt 42 root root 4096 ноя 21 18:42 tmp
When I try to start Coq 8.18 or 8.19 with coq-load-path set to its standard library, then coqtop aborts with an error and PG does > not even start to process the current buffer. With that wrong coq-load-path setting, can you process something very trivial, such as Definition a := 1.?
Yes, it works. Definition a := 1. gives the correct output: a is defined.
It was chatGPT(!)
I am sorry, but if you use a more or less random source to misconfigure your Emacs and Proof General, then you are on your own. I gave some hints earlier to which you haven't replied yet and which might help you. Otherwise, please provide a detailed description on how to reproduce the problem in the docker container proofgeneral/coq-emacs:coq-8.18.0-emacs-28.1.
I gave some hints earlier to which you haven't replied yet and which might help you. Otherwise, please provide a detailed description on how to reproduce the problem in the docker container proofgeneral/coq-emacs:coq-8.18.0-emacs-28.1.
This happens at work computer. As soon as I get there on Monday 25.11.2024 I will give the detailed description using you guidance.
You can run the container with docker run -it proofgeneral/coq-emacs:coq-8.18.0-emacs-28.1. To get Proof General, you may do git clone https://github.com/ProofGeneral/PG.git inside the container. To run Proof General, then do emacs -l /home/coq/PG/generic/proof-site.el.
Here are the logs:
1 items were added to the queue, scan for require attach first 0 items directly to queue handle require command "Require Import List." job-3: create require job for Require Import List. job-3: this job is the last compilation job now job-3: TTT start coqdep for require job for file /tmp/ProofGeneral-coqofYWUP.v job-3 pro-4: start coqdep /tmp/ProofGeneral-coqofYWUP.v in /home/usr345/mnt/vault/logics/ compilation queue empty return control, waiting for background jobs job-3 pro-4: TTT process status changed to exited abnormally with code 1 command: coqdep /tmp/ProofGeneral-coqofYWUP.v default-dir: /home/usr345/mnt/vault/logics/ curr buf deduct3.v job-3 coqdep error coqdep exit status 1 job-3: mark as failed job-3: coqc dependencies finished job-3: has itself no queue dependency job-3: ready job-3: locked ancestors: clear last compilation job Library compilation failed job-3: no queue dependant, queue kickoff finished compilation queue empty Beginning of buffer [2 times] Auto-saving...done End of buffer
I manually ran the command
$ strace coqdep /tmp/ProofGeneral-coqofYWUP.v
trying to imitate what proof general does and got the following:
--- SIGURG {si_signo=SIGURG, si_code=SI_TKILL, si_pid=123729, si_uid=1000} ---
rt_sigreturn({mask=[]}) = 22
getpid() = 123729
tgkill(123729, 123751, SIGURG) = 0
getpid() = 123729
tgkill(123729, 123750, SIGURG) = 0
futex(0x55610de9d158, FUTEX_WAKE_PRIVATE, 1) = 1
futex(0x55610de9d250, FUTEX_WAIT_PRIVATE, 0, {tv_sec=0, tv_nsec=100000}) = 0
getpid() = 123729
tgkill(123729, 123751, SIGURG) = 0
getpid() = 123729
tgkill(123729, 123750, SIGURG) = 0
futex(0x55610de9d158, FUTEX_WAKE_PRIVATE, 1) = 1
getpid() = 123729
tgkill(123729, 123751, SIGURG) = 0
futex(0x55610de9d158, FUTEX_WAKE_PRIVATE, 1) = 1
epoll_pwait(4, [], 128, 0, NULL, 0) = 0
futex(0xc000100948, FUTEX_WAKE_PRIVATE, 1) = 1
futex(0x55610de9d250, FUTEX_WAIT_PRIVATE, 0, {tv_sec=0, tv_nsec=100000}) = 0
close(3) = 0
futex(0x55610de9bc28, FUTEX_WAIT_PRIVATE, 0, NULL) = 0
epoll_pwait(4, [{EPOLLOUT, {u32=1967093352, u64=140516117149288}}], 128, 0, NULL, 0) = 1
epoll_pwait(4, [{EPOLLOUT, {u32=1967093352, u64=140516117149288}}], 128, -1, NULL, 0) = 1
epoll_pwait(4, [], 128, 0, NULL, 191668) = 0
futex(0x55610de9bc28, FUTEX_WAIT_PRIVATE, 0, NULL) = 0
epoll_pwait(4, [{EPOLLIN|EPOLLOUT, {u32=1967093592, u64=140516117149528}}], 128, 0, NULL, 0) = 1
epoll_pwait(4, [{EPOLLOUT, {u32=1967093352, u64=140516117149288}}], 128, -1, NULL, 0) = 1
epoll_pwait(4, [], 128, 0, NULL, 191668) = 0
epoll_pwait(4, [{EPOLLIN|EPOLLOUT, {u32=1967093352, u64=140516117149288}}], 128, -1, NULL, 0) = 1
recvmsg(3, {msg_name={sa_family=AF_UNIX, sun_path="/run/user/1000/bus"}, msg_namelen=112->21, msg_iov=[{iov_base="l\2\1\1'\0\0\0l\4\0\0-\0\0\0", iov_len=16}], msg_iovlen=1, msg_controllen=0, msg_flags=MSG_CMSG_CLOEXEC}, MSG_CMSG_CLOEXEC) = 16
recvmsg(3, {msg_name={sa_family=AF_UNIX, sun_path="/run/user/1000/bus"}, msg_namelen=112->21, msg_iov=[{iov_base="\5\1u\0\2\0\0\0\6\1s\0\6\0\0\0:1.155\0\0\10\1g\0\1o\0\0"..., iov_len=48}], msg_iovlen=1, msg_controllen=0, msg_flags=MSG_CMSG_CLOEXEC}, MSG_CMSG_CLOEXEC) = 48
recvmsg(3, {msg_name={sa_family=AF_UNIX, sun_path="/run/user/1000/bus"}, msg_namelen=112->21, msg_iov=[{iov_base="\"\0\0\0/org/freedesktop/systemd1/jo"..., iov_len=39}], msg_iovlen=1, msg_controllen=0, msg_flags=MSG_CMSG_CLOEXEC}, MSG_CMSG_CLOEXEC) = 39
futex(0xc000100948, FUTEX_WAKE_PRIVATE, 1) = 1
recvmsg(3, {msg_namelen=112}, MSG_CMSG_CLOEXEC) = -1 EAGAIN (Resource temporarily unavailable)
openat(AT_FDCWD, "/proc/123729/cgroup", O_RDONLY|O_CLOEXEC) = 8
epoll_ctl(4, EPOLL_CTL_ADD, 8, {EPOLLIN|EPOLLOUT|EPOLLRDHUP|EPOLLET, {u32=1967093592, u64=140516117149528}}) = -1 EPERM (Operation not permitted)
read(8, "13:cpuset:/\n12:rdma:/\n11:memory:"..., 4096) = 547
close(8) = 0
write(6, "\0", 1) = 1
futex(0x55610de9bc28, FUTEX_WAIT_PRIVATE, 0, NULL) = 0
epoll_pwait(4, [], 128, 0, NULL, 0) = 0
epoll_pwait(4, <unfinished ...>) = ?
*** Error: /tmp/ProofGeneral-coqofYWUP.v: No such file or directory
+++ exited with 1 +++
Seems that the cause are the permissions and some security measures done by Ubuntu. When I ran:
$ cp /tmp/ProofGeneral-coqofYWUP.v ~/aaa.v
$ coqdep ~/aaa.v
the error disappeared. Is it possible to setup ProofGeneral so that compilation was done in a subdir in my home directory?
After changing the temporary directory location and creating the dir ~/tmp, it started to work:
(setq temporary-file-directory (concat (getenv "HOME") "/tmp"))