XS0780 (Dec 13 2021 at 03:26): 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
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:
.v file only after doing the above? XS0780 (Dec 13 2021 at 14:36): XS0780 (Dec 13 2021 at 14:36):coq-syntax.png
coq-syntax1.png
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)
Karl Palmskog (Dec 13 2021 at 14:44):if this is Emacs or CoqIDE, that's not the right highlighting
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?
Paolo Giarrusso (Dec 13 2021 at 14:49):"opam init everytime" sounds strange, do you mean "eval $(opam env)"?
XS0780 (Dec 13 2021 at 14:49):Yes, I apologize. I meant to write "eval$(opam env)"
Karl Palmskog (Dec 13 2021 at 14:50):it's normal to have to do eval $(opam env) in a new shell
Paolo Giarrusso (Dec 13 2021 at 14:51):Do Linux users have to start emacs from a shell after the opam env thing?
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
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
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.
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
Paolo Giarrusso (Dec 13 2021 at 14:54):Yes, opam even has an option for automating it (often a good idea, not sure here...)
Paolo Giarrusso (Dec 13 2021 at 14:54):But that wouldn't affect the highlighting now, would it?
Karl Palmskog (Dec 13 2021 at 14:55):emacs should always be started in a shell which has been opam-initialized.
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
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)
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
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.
XS0780 (Dec 13 2021 at 15:10):So shouldn't Emcs be able to access that file inside ~/.emacs.d
Karl Palmskog (Dec 13 2021 at 15:11):you probably have to modify your .emacs file to load init.el
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).
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.
XS0780 (Dec 13 2021 at 15:21):Yeah, me neither. That could be the problem.
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.
Paolo Giarrusso (Dec 13 2021 at 15:29):AFAIK, without a ~/.emacs, Emacs should read ~/.emacs.d/init.el at startup
Paolo Giarrusso (Dec 13 2021 at 15:30):But Emacs has many knobs so...
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!
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).
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
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".
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
Li-yao (Dec 13 2021 at 17:42):That's working as expected :)
XS0780 (Dec 13 2021 at 17:48):That's cool! Now I wish we would use vscode instead of emacs on this course lol.
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)?
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/
Paolo Giarrusso (Dec 13 2021 at 18:32):It's hard to tailor files for emacs, what's the challenge?
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
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
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
Pierre-Marie Pédrot (Dec 13 2021 at 21:24): 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
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
Karl Palmskog (Dec 13 2021 at 21:28):you could try following the MELPA instructions: https://github.com/ProofGeneral/PG/#using-melpa-recommended-procedure
Karl Palmskog (Dec 13 2021 at 21:31):I think we should call Ltac "Coq's default tactic language" these days
Karl Palmskog (Dec 13 2021 at 21:34):since this is so far almost only ProofGeneral related, moving to the proper stream
Notification Bot (Dec 13 2021 at 21:34):This topic was moved here from #Coq users > Emacs configuration by Karl Palmskog
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
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" :-)
XS0780 (Dec 14 2021 at 15:55):I appreciate it! If all fails, I will just use Vscoq. Thank man!
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).
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: Apr 19 2024 at 04:02 UTC