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")) ```

> I've been using MacOS, I wonder if this is happening there. Please, look and let me know.

> Is your problem that your preferred (emacs) window layout is lost after quitting Proof General? Yes, it is lost. > Or is your problem that, after setting up your...

> Can you check that `proof-shrink-windows-tofit` (Proof-General -> Quick Options -> Display -> Shrink to Fit) is nil/disabled? This option is unchecked. I checked it, but nothing changed.