Library compilation failed

[usr345]

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?

[hendriktews]

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.

[hendriktews]

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.

[hendriktews]

Can you confirm that you use Emacs 26.3?

[hendriktews]

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.?

[usr345]

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.

[hendriktews]

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.

[usr345]

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.

[hendriktews]

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.