Stream: Proof General users

Topic: Emacs configuration


view this post on Zulip XS0780 (Dec 13 2021 at 03:26):

Hi guys:
I am following the third step:

To configure your emacs, you'll want to download our init.el and install it to the appropriate location:

On Mac OS/Linux: Put init.el in a folder in your home directory called .emacs.d (the leading dot is important!), and be sure you have no file called .emacs in your home directory. This is easiest in the terminal (rm ~/.emacs ; mkdir -p ~/.emacs.d ; mv ~/Downloads/init.el ~/.emacs.d).

Followed everything to a T, and somehow it isn't working the way the professor explains in this video:
https://pomona.app.box.com/s/4e3baojrq04r0cam33j7yl9f79kl3cd1/file/851671557065
It's telling me that Ctrl-C and Ctrl-Enter ain't working

view this post on Zulip Théo Zimmermann (Dec 13 2021 at 08:08):

This really is a question that you should address your professor in principle, given that it is specific to the file that he has provided you. But anyway, here are a few pieces of advices of things for you to check:

view this post on Zulip XS0780 (Dec 13 2021 at 14:36):

  1. Yes, I installed Coq using Opam. However, something I notice is that I have to "opam init" everytime I want to use Coq. So that might be the issue. I didn't use the snap packages, neither did I compile Coq from source.
  2. Yes, sir, I did.
    3.Here are some screenshots, not sure if it counts as syntax coloring

view this post on Zulip XS0780 (Dec 13 2021 at 14:36):

coq-syntax.png
coq-syntax1.png

view this post on Zulip XS0780 (Dec 13 2021 at 14:38):

Is there an alternate way to install Coq in Linux Mint without using snap packages? I tried using the "apt" package manager, but it installs an outdated version of Coq(8.11, the book requires 8.12 and up)

view this post on Zulip Karl Palmskog (Dec 13 2021 at 14:44):

if this is Emacs or CoqIDE, that's not the right highlighting

view this post on Zulip XS0780 (Dec 13 2021 at 14:45):

Yes, it's Emacs. So i guess the problem could be rooted that Coq isn't installed properly?

view this post on Zulip Paolo Giarrusso (Dec 13 2021 at 14:49):

"opam init everytime" sounds strange, do you mean "eval $(opam env)"?

view this post on Zulip XS0780 (Dec 13 2021 at 14:49):

Yes, I apologize. I meant to write "eval$(opam env)"

view this post on Zulip Karl Palmskog (Dec 13 2021 at 14:50):

it's normal to have to do eval $(opam env) in a new shell

view this post on Zulip Paolo Giarrusso (Dec 13 2021 at 14:51):

Do Linux users have to start emacs from a shell after the opam env thing?

view this post on Zulip XS0780 (Dec 13 2021 at 14:51):

It is? Because when I run "coqc -v" before running eval $(opam env) , it shows that Coq isn't installed in my machine

view this post on Zulip XS0780 (Dec 13 2021 at 14:52):

Only after running eval $(opam env) is when I can type coqc -v and it shows Coq's version

view this post on Zulip Paolo Giarrusso (Dec 13 2021 at 14:52):

It sounds normal; it probably says it cannot find coq, which is true; that command tells the shell where to find it, via the PATH variable.

view this post on Zulip Karl Palmskog (Dec 13 2021 at 14:53):

you can set up your default shell script file, such as .bashrc or similar, to run some opam boilerplate so the eval ... can be avoided under some circumstances

view this post on Zulip Paolo Giarrusso (Dec 13 2021 at 14:54):

Yes, opam even has an option for automating it (often a good idea, not sure here...)

view this post on Zulip Paolo Giarrusso (Dec 13 2021 at 14:54):

But that wouldn't affect the highlighting now, would it?

view this post on Zulip Karl Palmskog (Dec 13 2021 at 14:55):

emacs should always be started in a shell which has been opam-initialized.

view this post on Zulip Karl Palmskog (Dec 13 2021 at 14:55):

but this in itself is not enough, ProofGeneral needs to be installed as well, preferably via MELPA

view this post on Zulip Karl Palmskog (Dec 13 2021 at 14:56):

lack of highlighting is usually an indication that ProofGeneral is not getting initialized (which is orthogonal to opam initialization)

view this post on Zulip XS0780 (Dec 13 2021 at 15:06):

I thought ProofGeneral was installed alongside Coq? I am sorry for the amateur questions, new to Emacs and the Coq language

view this post on Zulip XS0780 (Dec 13 2021 at 15:09):

so after checking, apparently the file init.el that we were supposed to move to the directory ~/.emacs.d is the ProofGeneral file.

view this post on Zulip XS0780 (Dec 13 2021 at 15:10):

So shouldn't Emcs be able to access that file inside ~/.emacs.d

view this post on Zulip Karl Palmskog (Dec 13 2021 at 15:11):

you probably have to modify your .emacs file to load init.el

view this post on Zulip XS0780 (Dec 13 2021 at 15:18):

I don't think I have a .emacs file.
The instructions of the course explicitly tell us to "delete it":

On Mac OS/Linux: Put init.el in a folder in your home directory called .emacs.d (the leading dot is important!), and be sure you have no file called .emacs in your home directory. This is easiest in the terminal (rm ~/.emacs ; mkdir -p ~/.emacs.d ; mv ~/Downloads/init.el ~/.emacs.d).

view this post on Zulip Karl Palmskog (Dec 13 2021 at 15:20):

then I don't think the setup problems are related to Coq or opam. I have no idea how Emacs reads its initialization files.

view this post on Zulip XS0780 (Dec 13 2021 at 15:21):

Yeah, me neither. That could be the problem.

view this post on Zulip XS0780 (Dec 13 2021 at 15:21):

Seriously though, I thank all of you for the help that you guys provided me. At least now I have an idea of what could be the problem.

view this post on Zulip Paolo Giarrusso (Dec 13 2021 at 15:29):

AFAIK, without a ~/.emacs, Emacs should read ~/.emacs.d/init.el at startup

view this post on Zulip Paolo Giarrusso (Dec 13 2021 at 15:30):

But Emacs has many knobs so...

view this post on Zulip XS0780 (Dec 13 2021 at 15:34):

Yeah, that's how I thought it would work. I see that stepping in the Emacs world is a complete rabbit hole. So I will keep googling around until I find the answer. Thanks guys!

view this post on Zulip Théo Zimmermann (Dec 13 2021 at 16:12):

Something strange to me is why Coq instructors insist on their students use of Emacs. VsCode with VsCoq would seem like a choice that is both more accessible and easier to set up, so I would generally expect that this choice is also proposed (unless there is a good reason).

view this post on Zulip XS0780 (Dec 13 2021 at 16:17):

I just installed VsCoq, and it seems to work right off the bat. Too bad the course uses Emacs, otherwise it would have been a painless experience.
vscoq.png

view this post on Zulip Fabian Kunze (Dec 13 2021 at 16:23):

Does VSCode do more than just the syntax highlighting?
It only "works properly" if parts of the text file get highlighted in green after execution, for example by pressing "Alt"+"End".

view this post on Zulip XS0780 (Dec 13 2021 at 16:32):

So I checked, and when I pressed "Alt" + "End" the text file got highlighted in green, however, a tab got open afterwards telling that it is not in "Proof mode"
not-in-proof-mode.png

view this post on Zulip Li-yao (Dec 13 2021 at 17:42):

That's working as expected :)

view this post on Zulip XS0780 (Dec 13 2021 at 17:48):

That's cool! Now I wish we would use vscode instead of emacs on this course lol.

view this post on Zulip Li-yao (Dec 13 2021 at 17:55):

Is that a strong requirement for the class? Might the professor be willing to grant an exception as long as you have a working setup (and following the class instructions did not work)?

view this post on Zulip XS0780 (Dec 13 2021 at 18:20):

Honestly, it is an online class that teaches discrete math and functional programming that made the class free to audit. So it's not that I am "technically" taking the class. It seems that their files are all their files are tailored made for emacs, so I think I am out of luck lol.
https://cs.pomona.edu/classes/cs54/

view this post on Zulip Paolo Giarrusso (Dec 13 2021 at 18:32):

It's hard to tailor files for emacs, what's the challenge?

view this post on Zulip XS0780 (Dec 13 2021 at 21:19):

Well, it is the first lesson, and the file contains the material that we need for the first lecture: https://cs.pomona.edu/classes/cs54/book/Day01_intro.html

view this post on Zulip XS0780 (Dec 13 2021 at 21:20):

But apparently Emacs is not recogzing Coq, because it's not even syntax highlighting it. Even though I followed all the previous steps to set it up

view this post on Zulip Pierre-Marie Pédrot (Dec 13 2021 at 21:22):

In the first part of the course, we'll use Coq's (French for 'rooster') functional programming language Gallina (Spanish for 'hen') to write programs. In the second part of the course, we'll use Coq's unnamed tactic language to learn to write proofs. In the third and final part of the course, we'll adapt what we've learned to write proofs on paper.

kind of OT, but this looks quite inaccurate to me

view this post on Zulip Pierre-Marie Pédrot (Dec 13 2021 at 21:24):

  1. Gallina is AFAIK Latin (though the Spanish word is obviously written the same, I've always heard it pronounce Latin-ish style) and 2. Coq tactic language is infamously called Ltac

view this post on Zulip Karl Palmskog (Dec 13 2021 at 21:24):

the syntax highlighting is independent from "interacting with Coq". The ProofGeneral extension to Emacs both has a syntax highlighting part and another part for interacting with Coq through the coqtop program on the system. We use the absence of syntax highlighting as a "canary in the coalmine" that ProofGeneral is not getting loaded at all

view this post on Zulip XS0780 (Dec 13 2021 at 21:26):

I see, so it's ProofGeneral not loading up on Emacs apparently. I would have to google the reason why is that, so I guess I better hit stackoverflow lol

view this post on Zulip Karl Palmskog (Dec 13 2021 at 21:28):

you could try following the MELPA instructions: https://github.com/ProofGeneral/PG/#using-melpa-recommended-procedure

view this post on Zulip Karl Palmskog (Dec 13 2021 at 21:31):

I think we should call Ltac "Coq's default tactic language" these days

view this post on Zulip Karl Palmskog (Dec 13 2021 at 21:34):

since this is so far almost only ProofGeneral related, moving to the proper stream

view this post on Zulip Notification Bot (Dec 13 2021 at 21:34):

This topic was moved here from #Coq users > Emacs configuration by Karl Palmskog

view this post on Zulip XS0780 (Dec 13 2021 at 22:21):

Karl Palmskog said:

you could try following the MELPA instructions: https://github.com/ProofGeneral/PG/#using-melpa-recommended-procedure

Ironically enough, the file that we are supposed to download and move to ~/.emacs.d, contains the melpa instructions lol

view this post on Zulip Paolo Giarrusso (Dec 14 2021 at 07:45):

Instructions to follow by hand, or instructions that should download PG automatically (as the textbook says)?

Well, it is the first lesson, and the file contains the material that we need for the first lecture: https://cs.pomona.edu/classes/cs54/book/Day01_intro.html

What I mean is that the lecture looks doable on vscoq, even if the material says otherwise. This isn't a guarantee, just "don't give up if configuring emacs fails" :-)

view this post on Zulip XS0780 (Dec 14 2021 at 15:55):

I appreciate it! If all fails, I will just use Vscoq. Thank man!

view this post on Zulip Pierre Courtieu (Jan 21 2022 at 14:11):

Hi there. indeed the recommended way of installing PG is using the emacs package manager. Don't forget to remove any other previous intallation of PG. And indeed don't forget to lauch emacs from a coq-aware environment: either from a terminal after the eval $(opam env) thing of from your window manager if your X session is coq aware (highly dependent of your shell init scripts and needs a restart of WM after your first opam init).

view this post on Zulip Pierre Courtieu (Jan 21 2022 at 14:14):

And to my knowledge the vscode plugin is OK for software foundation and any other development. Unless if you are using an old version of coq.


Last updated: Feb 06 2023 at 07:03 UTC