/usr/share/doc/proofgeneral-doc/html/Obtaining-and-Installing.html

<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html>
<!-- Created by GNU Texinfo 6.3, http://www.gnu.org/software/texinfo/ -->
<head>
<title>Proof General: Obtaining and Installing</title>

<meta name="description" content="Proof General: Obtaining and Installing">
<meta name="keywords" content="Proof General: Obtaining and Installing">
<meta name="resource-type" content="document">
<meta name="distribution" content="global">
<meta name="Generator" content="makeinfo">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<link href="index.html#Top" rel="start" title="Top">
<link href="Function-Index.html#Function-Index" rel="index" title="Function Index">
<link href="Concept-Index.html#SEC_Contents" rel="contents" title="Table of Contents">
<link href="index.html#Top" rel="up" title="Top">
<link href="Bugs-and-Enhancements.html#Bugs-and-Enhancements" rel="next" title="Bugs and Enhancements">
<link href="Shell-Proof-General.html#Shell-Proof-General" rel="prev" title="Shell Proof General">
<style type="text/css">
<!--
/* Style sheet for the Proof General web pages. 
 * David Aspinall, June 1999.
 * proofgen.css,v 4.0 2000/03/13 07:36:57 da Exp
 */


a.summary-letter {text-decoration: none}
blockquote.indentedblock {margin-right: 0em}
blockquote.smallindentedblock {margin-right: 0em; font-size: smaller}
blockquote.smallquotation {font-size: smaller}
div.display {margin-left: 3.2em}
div.example {margin-left: 3.2em}
div.lisp {margin-left: 3.2em}
div.smalldisplay {margin-left: 3.2em}
div.smallexample {margin-left: 3.2em}
div.smalllisp {margin-left: 3.2em}
kbd {font-style: oblique}
pre.display {font-family: inherit}
pre.format {font-family: inherit}
pre.menu-comment {font-family: serif}
pre.menu-preformatted {font-family: serif}
pre.smalldisplay {font-family: inherit; font-size: smaller}
pre.smallexample {font-size: smaller}
pre.smallformat {font-family: inherit; font-size: smaller}
pre.smalllisp {font-size: smaller}
span.nolinebreak {white-space: nowrap}
span.roman {font-family: initial; font-weight: normal}
span.sansserif {font-family: sans-serif; font-weight: normal}
ul.no-bullet {list-style: none}
body{
 font-family: Verdana, Arial, sans-serif;
 background: #2D1D03;  /* background brown */
 background-attachment: fixed;
 color: #FFFFFF;
}

p{
 max-width: 1024px;
 font-family: Verdana, Arial, sans-serif;
 color: #FFFFFF;
}
pre{
 color: #FFFFFF;
}
h1{
 color: #FFFFFF;
 font-size: large;
 font-weight: bold;
}
h2{
 font-size: medium;
 font-weight: bold;
 color: #FFFFD0;
 padding: 2px 4px 4px 8px;
 background: #5D2D13;
}
h3{
 font-size: medium;
 padding: 2px 2px 2px 8px;
 margin-right: 50%;
 background: #4D1D23;
 color: #FFFFD0;
}
h4{
 font-size: medium;
 color: #FFD0D0;
 padding: 2px 2px 2px 8px;
}
blockquote,form,input,select{
 color: #FFFFFF;
}
address{
 font-size: small;
 color: #FFFFFF;
}
select {
 font-size: 100%;
 background: #2D1D03;
 color: #FFFFFF;
}
textarea,input {
 font-size: 100%;
 background: #4D2D23;
 color: #FFFFFF;
}
input[type=submit],input[type=reset],input[type=Submit] {
 font-size: 80%;
 padding-top: 0px;
 padding-bottom: 0px;
 background: #401010;
}
#button:active{
 background: #402020;
}

dl,ul,dir,li{
 color: #FFFFFF;
 max-width: 1024px;
}

dt{ font-style: italic; 
    padding: 2px 2px 2px 8px;
    margin-left: 20px;
    margin-right: 20px;
    background: #4D1D23; 
}

table{
 font-family: Verdana, Arial, sans-serif;	
 color: #FFFFFF;
}

table.menubar{
 font-family: Verdana, Arial, sans-serif;	
 font-size: smaller;
 color: #FFFFFF;
}

td,tr{
 color: #FFFFFF;
}

a:link,a:visited{
 font-family: Verdana, Arial, sans-serif;	
 text-decoration: none;
 color: #E0D020;
}

a:active,a:hover{
 font-family: Verdana, Arial, sans-serif;	
 text-decoration: underline;
 color: #E8D830;
}

pre{
 background: #2D1D03;
}

/* Specifics */

p.nb{
 font-size: smaller;
 font-style: italic;
}

/* These bits for Mailman pages for mailing lists */
TD.head1old {
 font-family: Verdana, Arial, sans-serif;
  text-align: center;
  color: #FFFFFF;
  font-weight: bold;
  font-size: 110%;
}
td.head1{
 font-family: Verdana, Arial, sans-serif;
 font-weight: bold;
 font-size: 110%;
 text-align: center;
 color: #FFFFFF;
}
td.head2{
 font-family: Verdana, Arial, sans-serif;
 font-size: 100%;
 font-weight: bold;
 color: #FFFFD0;
 padding: 2px 4px 4px 4px;
 background: #7D4D33;
}
td.head3{
 font-family: Verdana, Arial, sans-serif;	
 padding: 2px 2px 2px 2px;
 margin-right: 10%;
 background: #6D3D43;
 font-size: 80%;
 color: #FFFFD0;
}
td.head4{
 font-family: Verdana, Arial, sans-serif;	
 font-size: 100%;
 font-weight: bold;
 color: #FFD0D0;
}

-->
</style>


</head>

<body lang="en">
<a name="Obtaining-and-Installing"></a>
<div class="header">
<p>
Next: <a href="Bugs-and-Enhancements.html#Bugs-and-Enhancements" accesskey="n" rel="next">Bugs and Enhancements</a>, Previous: <a href="Shell-Proof-General.html#Shell-Proof-General" accesskey="p" rel="prev">Shell Proof General</a>, Up: <a href="index.html#Top" accesskey="u" rel="up">Top</a> &nbsp; [<a href="Concept-Index.html#SEC_Contents" title="Table of contents" rel="contents">Contents</a>][<a href="Function-Index.html#Function-Index" title="Index" rel="index">Index</a>]</p>
</div>
<hr>
<a name="Obtaining-and-Installing-1"></a>
<h2 class="appendix">Appendix A Obtaining and Installing</h2>

<p>Proof General has its own
<a href="https://proofgeneral.github.io">home page</a> hosted at
GitHub.  Visit this page for the latest news!
</p>


<hr>
<a name="Obtaining-Proof-General"></a>
<a name="Obtaining-Proof-General-1"></a>
<h3 class="section">A.1 Obtaining Proof General</h3>

<p>You can obtain Proof General from the URL
</p><div class="example">
<pre class="example"><a href="https://github.com/ProofGeneral/PG">https://github.com/ProofGeneral/PG</a>.
</pre></div>

<p>The distribution is available in the master branch of the repository.
Tagged versions of the sources may be redistributed by third party
packagers in other forms.
</p>
<p>The sources includes the generic elisp code, and code for Coq, LEGO,
Isabelle, and other provers.  Also included are installation
instructions (reproduced in brief below) and this documentation.
</p>
<hr>
<a name="Installing-Proof-General-from-sources"></a>
<a name="Installing-Proof-General-from-sources-1"></a>
<h3 class="section">A.2 Installing Proof General from sources</h3>

<p>Remove old versions of Proof General, then download and install the new
release from GitHub:
</p><div class="example">
<pre class="example">$ git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
$ cd ~/.emacs.d/lisp/PG
$ make
</pre></div>

<p>Then add the following to your <samp>.emacs</samp>:
</p><div class="lisp">
<pre class="lisp">;; Open .v files with Proof General's Coq mode
(load &quot;~/.emacs.d/lisp/PG/generic/proof-site&quot;)
</pre></div>

<p>If Proof General complains about a version mismatch, make sure that the
shell&rsquo;s <code>emacs</code> is indeed your usual Emacs. If not, run the Makefile
again with an explicit path to Emacs. On macOS in particular you&rsquo;ll
probably need something like
</p><div class="example">
<pre class="example">make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs
</pre></div>

<hr>
<a name="Setting-the-names-of-binaries"></a>
<a name="Setting-the-names-of-binaries-1"></a>
<h3 class="section">A.3 Setting the names of binaries</h3>

<p>The <code>load</code> command you have added will load <samp>proof-site</samp>
which sets the Emacs load path for Proof General and add auto-loads and
modes for the supported assistants.
</p>
<p>The default names for proof assistant binaries may work on your system.
If not, you will need to set the appropriate variables.  The easiest way
to do this (and most other customization of Proof General) is via the
Customize mechanism, see the menu item:
</p><div class="example">
<pre class="example">  Proof-General -&gt; Advanced -&gt; Customize -&gt; <var>Name of Assistant</var> -&gt; Prog Name
</pre></div>
<p>The Proof-General menu is available from script buffers after Proof
General is loaded.  To load it manually, type
</p><div class="lisp">
<pre class="lisp">  M-x load-library RET proof RET
</pre></div>

<p>If you do not want to use customize, simply add a line like this:
</p><div class="lisp">
<pre class="lisp">  (setq coq-prog-name &quot;/usr/bin/coqtop -emacs&quot;)
</pre></div>
<p>to your <samp>.emacs</samp> file.
For more advice on how to customize the <code>coq-prog-name</code> variable,
see <a href="Hints-and-Tips.html#Using-file-variables">Using file variables</a>, Remark 2.
</p>

<hr>
<a name="Notes-for-syssies"></a>
<a name="Notes-for-syssies-1"></a>
<h3 class="section">A.4 Notes for syssies</h3>

<p>Here are some more notes for installing Proof General in more complex
ways.  Only attempt things in this section if you really understand what
you&rsquo;re doing!
</p>
<a name="Byte-compilation"></a>
<h4 class="unnumberedsubsec">Byte compilation</h4>

<p>Compilation of the Emacs lisp files improves efficiency but can
sometimes cause compatibility problems, especially if you use more than
one version of Emacs with the same <code>.elc</code> files. 
</p>
<p>If you discover problems using the byte-compiled <code>.elc</code> files which
aren&rsquo;t present using the source <code>.el</code> files, please report them to
us.
</p>
<p>You can compile Proof General by typing <code>make</code> in the directory
where you installed it.  It may be necessary to do this if you use
a different version of Emacs.
</p>

<a name="Site_002dwide-installation"></a>
<h4 class="unnumberedsubsec">Site-wide installation</h4>

<p>If you are installing Proof General site-wide, you can put the
components in the standard directories of the filesystem if you prefer,
providing the variables in <samp>proof-site.el</samp> are adjusted
accordingly (see <i>Proof General site configuration</i> in
<i>Adapting Proof General</i> for more details).  Make sure that
the <samp>generic/</samp> and assistant-specific elisp files are kept in
subdirectories (<samp>coq/</samp>, <samp>isa/</samp>, <samp>lego/</samp>) of
<code>proof-home-directory</code> so that the autoload directory calculations
are correct.
</p>
<p>To prevent every user needing to edit their own <samp>.emacs</samp> files, you
can put the <code>load-file</code> command to load <samp>proof-site.el</samp> into
<samp>site-start.el</samp> or similar.  Consult the Emacs documentation for more
details if you don&rsquo;t know where to find this file.
</p>
<a name="Removing-support-for-unwanted-provers"></a>
<h4 class="unnumberedsubsec">Removing support for unwanted provers</h4>

<p>You cannot run more than one instance of Proof General at a time: so if
you&rsquo;re using Coq, visiting an <samp>.ML</samp> file will not load Isabelle
Proof General, and the buffer remains in fundamental mode.  If there are
some assistants supported that you never want to use, you can adjust the
variable <code>proof-assistants</code> in <samp>proof-site.el</samp> to remove the
extra autoloads.  This is advisable in case the extensions clash with
other Emacs modes, for example 
Verilog mode for <samp>.v</samp> files clashes with Coq mode.  
</p>
<p>See <i>Proof General site configuration</i> in <i>Adapting Proof General</i>,
for more details of how to adjust the <code>proof-assistants</code> setting.
</p>
<p>Instead of altering <code>proof-assistants</code>, a simple way to disable
support for some prover is to delete the relevant directories from the
PG installation.  For example, to remove support for Coq, delete the
<samp>coq</samp> directory in the Proof General home directory.
</p>




<hr>
<div class="header">
<p>
Previous: <a href="#Setting-the-names-of-binaries" accesskey="p" rel="prev">Setting the names of binaries</a>, Up: <a href="#Obtaining-and-Installing" accesskey="u" rel="up">Obtaining and Installing</a> &nbsp; [<a href="Concept-Index.html#SEC_Contents" title="Table of contents" rel="contents">Contents</a>][<a href="Function-Index.html#Function-Index" title="Index" rel="index">Index</a>]</p>
</div>



</body>
</html>
proofgeneral-doc 4.4.1~pre170114-1 / usr / share / doc / proofgeneral-doc / html / Obtaining-and-Installing.html
