Stream: Coq users

Topic: emacs compilation issues


view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Nicolas Rinaudo (Aug 18 2023 at 11:29):

Thanks for taking the time to explain

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip Nicolas Rinaudo (Aug 18 2023 at 19:47):

"claims" being the operative word here, as it plainly does not :)

view this post on Zulip Paolo Giarrusso (Aug 18 2023 at 21:56):

Actually, Emacs (used to) work fine — can you clarify what's the problem?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Nicolas Rinaudo (Aug 21 2023 at 07:36):

(apologies, I really should have pasted the error message in my first message, that wasn't very bright of me)

view this post on Zulip Notification Bot (Aug 21 2023 at 14:32):

This topic was moved to #Proof General users > emacs compilation issues by Karl Palmskog.


Last updated: Jun 22 2024 at 16:02 UTC