* Trying to install the emacs mode for lean theorem prover [not found] <571324850.2598402.1513695864283.ref@mail.yahoo.com> @ 2017-12-19 15:04 ` Diego Carlesso 2017-12-19 15:53 ` tomas 0 siblings, 1 reply; 3+ messages in thread From: Diego Carlesso @ 2017-12-19 15:04 UTC (permalink / raw) To: help-gnu-emacs@gnu.org Hi, I'm trying to install for a project the emacs mode for lean theorem prover on a mac os x; I already have emacs installed from here https://emacsformacosx.com/; the guide for the lean mode says that: "lean-mode requires GNU Emacs 24.3 or newer. The recommended way to install it is via MELPA. If you have not already configured MELPA, put the following code in your Emacs init file (typically ~/.emacs.d/init.el) " but I can't find any init file; already tried to uninstall emacs and install it again, but nothing changed. I'm maybe doing something wrong; maybe I'm even asking in the wrong place.Thanks for your time, Diego ^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: Trying to install the emacs mode for lean theorem prover 2017-12-19 15:04 ` Trying to install the emacs mode for lean theorem prover Diego Carlesso @ 2017-12-19 15:53 ` tomas 2017-12-19 17:02 ` Drew Adams 0 siblings, 1 reply; 3+ messages in thread From: tomas @ 2017-12-19 15:53 UTC (permalink / raw) To: help-gnu-emacs -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 On Tue, Dec 19, 2017 at 03:04:24PM +0000, Diego Carlesso wrote: > [...] but I can't find any init file; already tried to uninstall > emacs and install it again, but nothing changed. I'm maybe doing > something wrong; maybe I'm even asking in the wrong place [...] Perhaps this puts you on the right track: https://stackoverflow.com/questions/27869909/what-to-do-if-i-cannot-find-my-emacs-init-file Generally it's not a problem when the init file doesn't exist (yet). You just create it (and Emacs command "find-file" will do that for you, conveniently). The Emacs variable "user-init-file" contains the name of that init file (which might vary depending on the operating system, so it makes sense to look into that). Of course, you can create it with any other editor (plain text!), but if you are going to use Emacs, perhaps it's a good plan to try that first... And yes, you are right here -- welcome :-) Just come back if you don't understand something in the above link. Cheers - -- tomás -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.12 (GNU/Linux) iEYEARECAAYFAlo5NgAACgkQBcgs9XrR2kZSZwCdEq9d+u8KrD/EopghoB3kbLMy F7wAnR/4r4oDbsA1GasoraIDRiiv268G =qbLX -----END PGP SIGNATURE----- ^ permalink raw reply [flat|nested] 3+ messages in thread
* RE: Trying to install the emacs mode for lean theorem prover 2017-12-19 15:53 ` tomas @ 2017-12-19 17:02 ` Drew Adams 0 siblings, 0 replies; 3+ messages in thread From: Drew Adams @ 2017-12-19 17:02 UTC (permalink / raw) To: tomas, help-gnu-emacs > Perhaps this puts you on the right track: > https://stackoverflow.com/questions/27869909/what-to-do-if-i-cannot- > find-my-emacs-init-file Or ask Emacs: `C-h r i init file RET'. See node `Find Init' of the Emacs manual. https://www.gnu.org/software/emacs/manual/html_node/emacs/Find-Init.html ^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2017-12-19 17:02 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
[not found] <571324850.2598402.1513695864283.ref@mail.yahoo.com>
2017-12-19 15:04 ` Trying to install the emacs mode for lean theorem prover Diego Carlesso
2017-12-19 15:53 ` tomas
2017-12-19 17:02 ` Drew Adams
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).