From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!.POSTED!not-for-mail From: Diego Carlesso Newsgroups: gmane.emacs.help Subject: Trying to install the emacs mode for lean theorem prover Date: Tue, 19 Dec 2017 15:04:24 +0000 (UTC) Message-ID: <571324850.2598402.1513695864283@mail.yahoo.com> References: <571324850.2598402.1513695864283.ref@mail.yahoo.com> Reply-To: Diego Carlesso NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Trace: blaine.gmane.org 1513698002 24876 195.159.176.226 (19 Dec 2017 15:40:02 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Tue, 19 Dec 2017 15:40:02 +0000 (UTC) To: "help-gnu-emacs@gnu.org" Original-X-From: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Tue Dec 19 16:39:58 2017 Return-path: Envelope-to: geh-help-gnu-emacs@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1eRJzo-0005vH-Bb for geh-help-gnu-emacs@m.gmane.org; Tue, 19 Dec 2017 16:39:56 +0100 Original-Received: from localhost ([::1]:50347 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1eRK1k-0004wJ-SX for geh-help-gnu-emacs@m.gmane.org; Tue, 19 Dec 2017 10:41:56 -0500 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:50884) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1eRJRZ-00024m-OL for help-gnu-emacs@gnu.org; Tue, 19 Dec 2017 10:04:38 -0500 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1eRJRW-0007Rk-Uk for help-gnu-emacs@gnu.org; Tue, 19 Dec 2017 10:04:33 -0500 Original-Received: from sonic302-20.consmr.mail.ir2.yahoo.com ([87.248.110.83]:34195) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1eRJRW-0007PE-Ji for help-gnu-emacs@gnu.org; Tue, 19 Dec 2017 10:04:30 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=yahoo.it; s=s2048; t=1513695868; bh=GTOzJjAt1qKEIGuGLsTsOrQHLxQtjTyf6Aa5a/Pwn6s=; h=Date:From:Reply-To:To:Subject:References:From:Subject; b=Pzzyi4qT13H0b/4VYa59PEKFw9oZwACsvyQs4rmPCdduDHbKBTZoofkGGpwx72bDirqI9PfLs2FeQqlug0d8ZSEghI72mlRo1XBysFAakRETbvg2MkbOmHcym4qBCYhbafzLAE+NSsAOuaxl/uARslZwtMmPFo5U2MgzAr2QfZ2ZF3kk6es8eg7G/OxkbP55tlG2o9FuQPA7OIR/hFXNnDvNxxSHtziJvE/2g0fbEfaMmKtlEkvXSI7GzuTgwBunBqahP2MgL6MC1H0ZZ+3uyhCtY22jPRr/bSLfFi1djtRvbvMvg4OeMoTbOfEJG1FKbTeav1NgO7pnoaMTqxuXrQ== X-YMail-OSG: GNRMP3AVM1lTKU1Ypq2lM31jIAvXhWtuZ4cbiHAfdCZFg2gcpJlhXfQ1mw7whId sHBneNZ0xF9hi18ujsiqwfr2XE1.GM_9FoEPZbOxiPHp9MCo7bUyMHrMrFAXqhKmIhu35gUpPjj_ _sJTCzgu3GovEd8yrqVuNeBbE8ueLOtar1LG6tDFLHbzxG0m6z6D98aim_LKCUnEaHiPcNE2bhRp 3aGEf4vb9pjn.Npc1z59gIYS9ePS2TzZSaI6DgIyByYTzRlmH5oFfaIPhS3k01oowg.mTwH0vors Mo2sTuZssxQmyc7kJ41MX0V7r19jcCvP5D7wZo9I3w442j4Gu4qLZhLeT8rR_GQIVpYxM9HsNCQN IX8aPZzZPRlncXZnmciGS5U_oXRvUW2pqAIYfiM.tMJgI3rZkVYqyCo3QFreIiZ1E8h0e1L2hfUE fnP0SazYlQhZdCoRzjPWm93cCum8_RXB.OJQ5.yPlP6.M8NaOURFWf4q1.7lI60s4vrIv1nOFaCo ntd8MnFwMQjV9r3aAKMhWWxk53kr5t7SvEKaMIFgDcBpVabW5dlc- Original-Received: from sonic.gate.mail.ne1.yahoo.com by sonic302.consmr.mail.ir2.yahoo.com with HTTP; Tue, 19 Dec 2017 15:04:28 +0000 X-Mailer: WebService/1.1.11051 YahooMailNeo Mozilla/5.0 (Macintosh; Intel Mac OS X 10_13_1) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/63.0.3239.84 Safari/537.36 X-detected-operating-system: by eggs.gnu.org: GNU/Linux 3.x [fuzzy] X-Received-From: 87.248.110.83 X-Mailman-Approved-At: Tue, 19 Dec 2017 10:37:26 -0500 X-Content-Filtered-By: Mailman/MimeDel 2.1.21 X-BeenThere: help-gnu-emacs@gnu.org X-Mailman-Version: 2.1.21 Precedence: list List-Id: Users list for the GNU Emacs text editor List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Original-Sender: "help-gnu-emacs" Xref: news.gmane.org gmane.emacs.help:115401 Archived-At: Hi, I'm trying to install for a project the emacs mode for lean theorem pro= ver on a mac os x; I already have emacs installed from here https://emacsfo= rmacosx.com/; the guide for the lean mode says that: "lean-mode=C2=A0requir= es GNU Emacs 24.3 or newer. The recommended way to install it is via=C2=A0M= ELPA. If you have not already configured MELPA, put the following code in y= our Emacs init file (typically=C2=A0~/.emacs.d/init.el) " but I can't find = any init file; already tried to uninstall emacs and install it again, but n= othing changed. I'm maybe doing something wrong; maybe I'm even asking in t= he wrong place.Thanks for your time,=C2=A0=C2=A0Diego