Nicolas Rinaudo (Aug 18 2023 at 11:22): Nicolas Rinaudo (Aug 18 2023 at 11:22):I'm trying to set up emacs to work comfortably with Coq, and running into issues. Please let me know if this is not the right place to ask about such things.
The issue I'm having is that, when evaluating an Require statement, the following appears in the output buffer:
coqdep -Q /home/nrinaudo/dev/nrinaudo/software-foundations/lf LF /tmp/ProofGeneral-coqCSVAQq.v
The -Q path LF path I completely understand, that comes from my _CoqProject file. I don't understand what the /tmp/ProofGeneral-coqCSVAQq.v part is, as I'd be expecting that to be the path of the file that contains my Require statement (which would be ./Induction.v)
Karl Palmskog (Aug 18 2023 at 11:25):I'd recommend to just use regular coq_makefile and the make command to build. There is a breakdown of the files needed for this here: https://github.com/coq-community/coq-program-verification-template#file-and-directory-structure
Nicolas Rinaudo (Aug 18 2023 at 11:27):but then would that work well with Emacs? The user experience I'd like (and ProofGeneral is supposed to offer) is that when I step over a Require statement, the correspondning Coq file will be recompiled automatically if needed, so that I can mostly focus on just typing and proving, not all the tooling underneath which I'd prefer to ignore while learning the language
Nicolas Rinaudo (Aug 18 2023 at 11:28):I'm well aware that at some point, I will need to learn the tooling. It's just that this is the least interesting part of learning Coq for me, and I'd prefer to postpone it until after I've learned the "fun" part
Karl Palmskog (Aug 18 2023 at 11:28):there may be the idea that emacs should compile when you step through Require, but in practice, few people use this, not least since coq_makefile/make is more robust. If you set [coq_makefile/make] up so that it uses _CoqProject, then ProofGeneral/emacs will be able to read all .vo files built via make.
Nicolas Rinaudo (Aug 18 2023 at 11:29):I see. Well, I'll stil try to set things up the way the book I'm going through tells me I should first, but if that doesn't work I'll bite the bullet and peek under hood
Nicolas Rinaudo (Aug 18 2023 at 11:29):Thanks for taking the time to explain
Karl Palmskog (Aug 18 2023 at 11:30):coq_makefile is a standard tool bundled with Coq, I'd not exactly call it "under the hood".
Nicolas Rinaudo (Aug 18 2023 at 11:32):I would, for my case, as it forces me to learn and understand the Coq tooling rather than the Coq language, when I'm, currently, interested in the latter but not the former
Nicolas Rinaudo (Aug 18 2023 at 11:32):and yes, I'm perfectly aware that the tooling will become important. It's currently just another hoop to jump through before I can learn the language, and if I can postpone that until later, I'd like to do that
Paolo Giarrusso (Aug 18 2023 at 18:03):The first time I had to use coq_makefile, I was completely stumped honestly — between Proof General not relying on it and Software Foundations not explaining it.
Paolo Giarrusso (Aug 18 2023 at 18:05):IIRC I went from "let's try to use coqide, that should be easier than Emacs" to "why does none of the coqide commands do anything".
Paolo Giarrusso (Aug 18 2023 at 18:09):OTOH, https://softwarefoundations.cis.upenn.edu/lf-current/Preface.html claims either Emacs or coqide should work out of the box.
Nicolas Rinaudo (Aug 18 2023 at 19:47):"claims" being the operative word here, as it plainly does not :)
Paolo Giarrusso (Aug 18 2023 at 21:56):Actually, Emacs (used to) work fine — can you clarify what's the problem?
Paolo Giarrusso (Aug 18 2023 at 22:00):the report seems that "the Emacs implementation uses files in /tmp internally" — which isn't a bug — and that appears in "the output buffer" — is that *coq*? That's also internal.
Paolo Giarrusso (Aug 18 2023 at 22:01):I _suppose_ the actual issue is that stepping over Require doesn't work somehow, but what's the symptom?
Paolo Giarrusso (Aug 18 2023 at 22:02):I don't understand what the /tmp/ProofGeneral-coqCSVAQq.v part is, as I'd be expecting that to be the path of the file that contains my Require statement (which would be ./Induction.v)
If I had to guess, that's because you're stepping over _one_ Require, so that's what Proof General is processing. Processing the full file would prevent you from stepping over that require if there's any error later.
Paolo Giarrusso (Aug 18 2023 at 22:03):IDEs often can make some sense of WIP source with errors, but coq tooling isn't necessarily designed for that so Proof General must be creative.
Nicolas Rinaudo (Aug 21 2023 at 06:52):I'm... not sure we're talking of the same things. The coqdep command triggered by Proof General when doing something advertised as perfectly possible (stepping over a Require statement) is nonsensical: it tries to compute the dependencies of a file that does not exist.
Nicolas Rinaudo (Aug 21 2023 at 06:53):I don't mind that it's a temporary file, I don't mind that it's got a weird name, only that it does not exist
Nicolas Rinaudo (Aug 21 2023 at 06:54):(and yes, I initially assumed it was merely the fact that /tmp didn't have write access and Proof General swallowed the write error, but no, it's perfectly writable)
Karl Palmskog (Aug 21 2023 at 07:32):so you don't actually get any error? ProofGeneral by design creates a bunch of temporary files in the /tmp area whenever it runs. These files are removed after Coq/coqdep has been run on them (from what I remember)
Nicolas Rinaudo (Aug 21 2023 at 07:34):Ah, well that might explain why I can't find the file when I try to reproduce the issue!
Nicolas Rinaudo (Aug 21 2023 at 07:35):although that still appears to be the issue ProofGeneral itself is facing:
-*- mode: compilation; -*-
coqdep -Q /home/nrinaudo/dev/nrinaudo/software-foundations/lf LF /tmp/ProofGeneral-coq5Uyo42.v
*** Error: /tmp/ProofGeneral-coq5Uyo42.v: No such file or directory
(apologies, I really should have pasted the error message in my first message, that wasn't very bright of me)
Notification Bot (Aug 21 2023 at 14:32):This topic was moved here from #Coq users > emacs compilation issues by Karl Palmskog.
Karl Palmskog (Aug 21 2023 at 14:33):@Nicolas Rinaudo so it appears that this was a pure PG issue after all, moving to our PG user stream where there may be more help. I'd still do the workaround and compile with make, though...
Paolo Giarrusso (Aug 21 2023 at 14:51):the interesting error is probably why PG failed to create the file — either it forgot to try, or it tried and failed for some reason. Is there anything in *Messages* or some other buffer.
/tmp permissions are most system dependent, but if PG and other programs can't write to /tmp, your system wouldn't be usable... any chance your Emacs runs in some sandbox?
Nicolas Rinaudo (Aug 21 2023 at 15:07):@Karl Palmskog this is what I'm doing, yes, because this is the only way of moving forward that doesn't involve me manually debugging elisp :)
Nicolas Rinaudo (Aug 21 2023 at 15:08):@Paolo Giarrusso there really is no reason I can think of for PG to fail there. Here are the permissions on /tmp: drwxrwxrwt.
And no, Emacs is not running in a sandbox of any kind
Nicolas Rinaudo (Aug 21 2023 at 15:09):honestly though - I'm happy to help debug for the sake of others that encounter the same issue, but please don't waste time for me. I've resigned myself to using Make for the moment , which is less streamlined but perfectly fine
Pierre Courtieu (Aug 22 2023 at 13:55):Hi! The feature indeed uses /tmp/xx.v file to generate a file containing only the Require commands of your file, (so that coqdep is fast and local (in case you are using distant file system or tramp). Then it uses coqdep and file dates to decide what to recompile mostly like make would.
This certainly has some corner cases but I find it quite useful. Especially in combination with the "only vos" option. Of course a good fat make is recommended on a regular bases.
It works out of the box for me, provided the _CoqProject has the needed informations. That said it seems that the current consensus is that _CoqProject file format is not good. (@Karl Palmskog can you remind me where the discussion about this issue takes places please?)
@Nicolas Rinaudo Can you fill a bug at https://github.com/ProofGeneral/PG/issues with a whole coq project which fails please?
Karl Palmskog (Aug 22 2023 at 14:01):there is a constant back-and-forth about the _CoqProject file format, I don't remember any specific Coq issue, there are probably several. The main gotcha with _CoqProject is that one should avoid quotes and the like to be compatible with both PG, CoqIDE, VsCoq, etc., on several platforms like macOS, Windows
Karl Palmskog (Aug 22 2023 at 14:02):in contrast, configuring/building with dune is much more portable and robust, but there is no convenient editor support yet (editors should use dune coq top, but to my knowledge support for that is experimental)
Last updated: Oct 13 2024 at 01:02 UTC