usr345

> x / d + u32::from(x % d == 0) Incorrect. It should be: x / d + u32::from(x % d != 0)

@gares On page 119 no need to put "@" before Pack: `Definition nat_eqType : eqType := @Pack nat eqn. ` And before eq_op: `Check (@eq_op nat_eqType 3 4).`

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

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

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

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

After changing the temporary directory location and creating the dir `~/tmp`, it started to work: ``` (setq temporary-file-directory (concat (getenv "HOME") "/tmp")) ```