Skip to content

Commit c3967ac

Browse files
mikeshulmanmikeshulman
committed
a shell script for installing the proofgeneral mode
1 parent 8bce812 commit c3967ac

File tree

4 files changed

+117
-17
lines changed

4 files changed

+117
-17
lines changed

‎dist/INSTALL.txt‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,19 @@
1-
This is a static build of the master branch of Narya. The executable 'narya' should run on any Linux machine. You may want to place it in a 'bin' directory that is in your PATH.
1+
This is a static build of the master branch of Narya, an experimental proof assistant for higher-dimensional type theory.
22

3-
To install the recommended ProofGeneral interactive mode, follow the following steps:
3+
The executable 'narya' should run on any Linux machine. Place it in a directory that is in your PATH. On some flavors of Linux, the directory `~/bin` is automatically in your path if it exists, so the first thing to try would be
44

5-
1. Install Emacs <https://www.gnu.org/software/emacs/> and ProofGeneral. The recommended way to install ProofGeneral is from MELPA <https://melpa.org/> using Emacs' package manager, as described at the ProofGeneral page <https://proofgeneral.github.io/>.
5+
mkdir -p ~/bin
6+
cp narya ~/bin
67

7-
2. Find the ProofGeneral installation directory, which may be something like "$HOME/.emacs.d/elpa/proof-general-XXXXXXXX-XXXX".
8+
Then restart your shell (i.e. terminal or command prompt) and try running 'narya'. If that doesn't work, try logging out and back in again. If that still doesn't work, try something like the following commands:
89

9-
3. In this directory, create a subdirectory called "narya" and copy (or, better, symlink) the ".el" files from this directory into that subdirectory.
10+
export PATH="$HOME/bin:$PATH"
11+
echo export PATH="\$HOME/bin:\$PATH" >>~/.bashrc
1012

11-
4. Then edit the file "proof-site.el" in the subdirectory "generic" of the ProofGeneral installation directory and add a line containing
13+
and then once again restart your shell, or log out and back in again.
1214

13-
(narya "Narya" "ny" nil (".nyo"))
15+
To install the recommended ProofGeneral interactive mode, first make sure Emacs is installed, and then run the supplied shell script 'install-pg.sh' from this directory:
1416

15-
to the list of proof assistants in the definition of the variable "proof-assistant-table-default".
17+
./install-pg.sh
1618

17-
5. If there is a byte-compiled Emacs Lisp file "proof-site.elc" in the "generic" directory, either delete it, or re-create it from your edited "proof-site.el" using "M-x byte-compile-file".
18-
19-
6. Restart Emacs.
19+
If that doesn't work, please report a bug at https://github.com/gwaithimirdain/narya. In the meantime, you can follow the instructions in the Narya documentation for installing ProofGeneral manually (https://narya.readthedocs.io/en/latest/installation.html#proofgeneral-emacs-mode). You will need to repeat this every time Emacs, ProofGeneral, or Narya is updated.

‎dist/install-pg.sh‎

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,77 @@
1+
#!/bin/bash
2+
3+
echo
4+
echo Installing ProofGeneral...
5+
6+
# Write a minimal init file to enable MELPA and package.el
7+
TEMPINIT=$(mktemp)
8+
cat >"$TEMPINIT" <<EOF
9+
(require 'package)
10+
(setq package-archives '(("melpa" . "https://melpa.org/packages/")
11+
("gnu" . "https://elpa.gnu.org/packages/")))
12+
(package-initialize)
13+
(unless package-archive-contents
14+
(package-refresh-contents))
15+
(package-install 'proof-general)
16+
EOF
17+
18+
# Run Emacs in batch mode to install proof-general
19+
if ! emacs -Q --batch -l "$TEMPINIT"
20+
then
21+
echo Error running Emacs; is it installed correctly?
22+
exit 1
23+
fi
24+
25+
# Clean up temporary init file
26+
rm -f "$TEMPINIT"
27+
28+
echo
29+
echo Installing the Narya ProofGeneral mode...
30+
31+
# Locate the installed directory
32+
PGDIR=$(find ~/.emacs.d/elpa/ -maxdepth 1 -type d -name "proof-general-*" | sort -r | head -n1)
33+
34+
if ! [ -d $PGDIR ]
35+
then
36+
echo I can\'t find the ProofGeneral installation directory!
37+
exit 1
38+
fi
39+
40+
mkdir -p $PGDIR/narya
41+
42+
if [ -e narya.el ]
43+
then
44+
# Install the narya elisp files, overwriting any old ones.
45+
cp --remove-destination *.el $PGDIR/narya
46+
elif [ -e ../proofgeneral/narya.el ]
47+
then
48+
echo You appear to be running this script from the Narya source tree,
49+
echo so I will symlink the Narya .el files instead of copying them.
50+
pushd ../proofgeneral >/dev/null
51+
NARYA_PGDIR=`pwd`
52+
popd >/dev/null
53+
pushd $PGDIR/narya >/dev/null
54+
rm -f *.el *.elc
55+
ln -s $NARYA_PGDIR/*.el .
56+
popd >/dev/null
57+
else
58+
echo I can\'t find the Narya .el files!
59+
exit 1
60+
fi
61+
62+
# Insert Narya into the ProofGeneral configuration, if it isn't already there
63+
if ! grep narya $PGDIR/generic/proof-site.el >/dev/null
64+
then
65+
if [ -e proof-site.patch ]
66+
then
67+
patch -d $PGDIR/generic <proof-site.patch
68+
# Remove old byte-compiled version, if any, so the new source version is loaded instead
69+
rm -f $PGDIR/generic/proof-site.elc
70+
else
71+
echo I can\'t find proof-site.patch!
72+
fi
73+
fi
74+
75+
echo
76+
echo Narya ProofGeneral installed. Restart any open instances of Emacs.
77+
echo "(You will need to run this script again every time Emacs, ProofGeneral, or Narya is updated.)"

‎dist/proof-site.patch‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
--- proof-site-old.el 2025-04-15 18:10:57.146355104 -0700
2+
+++ proof-site.el 2025-02-27 16:37:32.268486304 -0800
3+
@@ -48,6 +48,7 @@
4+
(easycrypt "EasyCrypt" "ec" "\\.eca?\\'")
5+
(phox "PhoX" "phx" nil (".phi" ".pho"))
6+
(qrhl "qRHL" "qrhl")
7+
+ (narya "Narya" "ny" nil (".nyo"))
8+
9+
;; Cut-and-paste management only
10+

‎docs/source/installation.rst‎

Lines changed: 19 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Static binary
66

77
A statically compiled binary, built automatically from the up-to-date development version, can be downloaded from `GitHub Pages <https://gwaithimirdain.github.io/narya/releases/narya-master-static.tar.gz>`_. This ought to work on any Linux computer, and might work on other operating systems as well (e.g. using `Windows Subsystem for Linux <https://learn.microsoft.com/en-us/windows/wsl/install>`_ on Windows). Please report your experiences!
88

9-
You will still need to manually install Emacs, ProofGeneral, and the Narya :ref:`ProofGeneral mode`. The static distribution includes the necessary Emacs Lisp files and instructions.
9+
The static binary distribution also includes the recommended Narya :ref:`ProofGeneral mode` and a shell script that should install it, along with ProofGeneral, on any Linux computer. You'll need to install `Emacs <https://www.gnu.org/software/emacs/>`_ yourself first.
1010

1111

1212
Compiling from source
@@ -60,10 +60,10 @@ Alternatively, instead of running ``dune install``, you can run the executable d
6060

6161
If any of the above steps don't work for you, or if you have any other problems or encounter any bugs, please let us know by `opening an issue on GitHub <https://github.com/gwaithimirdain/narya/issues/new/choose>`_.
6262

63-
With nix
64-
--------
63+
Compiling with nix
64+
------------------
6565

66-
Narya can also be developed and installed with nix.
66+
Narya can also be developed and installed with `Nix <https://nixos.org/>`_.
6767

6868
1. Get a version of nix with `flakes <https://nixos.wiki/wiki/flakes>`_ enabled, for instance via `determinate nix <https://github.com/DeterminateSystems/nix-installer>`_.
6969

@@ -74,15 +74,28 @@ Narya can also be developed and installed with nix.
7474
ProofGeneral (Emacs) mode
7575
-------------------------
7676

77-
The recommended mode of use of Narya is with its `ProofGeneral <https://proofgeneral.github.io/>`_ Emacs mode (for further description of this, see :ref:`ProofGeneral mode`). Unfortunately, ProofGeneral doesn't make it asy for users to add new proof assistant modes. The steps to install Narya's ProofGeneral mode are:
77+
The recommended mode of use of Narya is with its `ProofGeneral <https://proofgeneral.github.io/>`_ Emacs mode (for further description of this, see :ref:`ProofGeneral mode`). Unfortunately, ProofGeneral doesn't make it easy for users to add new proof assistant modes. The static binary distribution includes a shell script that tries to automate this process, which you can also run from its directory in the source tree:
78+
79+
.. code-block:: bash
80+
81+
cd dist
82+
./install-pg.sh
83+
84+
If this doesn't work for you, you can follow these steps to install Narya's ProofGeneral mode manually.
7885

7986
1. Install `Emacs <https://www.gnu.org/software/emacs/>`_ and ProofGeneral. The recommended way to install ProofGeneral is from `MELPA <https://melpa.org/>`_ using Emacs' package manager, as described at the `ProofGeneral page <https://proofgeneral.github.io/>`_.
8087

8188
2. Find the ProofGeneral installation directory, which may be something like ``$HOME/.emacs.d/elpa/proof-general-XXXXXXXX-XXXX``.
8289

8390
3. In this directory, create a subdirectory called ``narya`` and copy (or, better, symlink) the files in the proofgeneral directory of the Narya repository into that subdirectory.
8491

85-
4. Then edit the file ``proof-site.el`` in the subdirectory ``generic`` of the ProofGeneral installation directory and add a line containing ``(narya "Narya" "ny" nil (".nyo"))`` to the list of proof assistants in the definition of the variable ``proof-assistant-table-default``.
92+
4. Then edit the file ``proof-site.el`` in the subdirectory ``generic`` of the ProofGeneral installation directory and add this line line
93+
94+
.. code-block:: none
95+
96+
(narya "Narya" "ny" nil (".nyo"))
97+
98+
to the list of proof assistants in the definition of the variable ``proof-assistant-table-default``.
8699

87100
5. If there is a byte-compiled Emacs Lisp file ``proof-site.elc`` in the ``generic`` directory, either delete it, or re-create it from your edited ``proof-site.el`` using ``M-x byte-compile-file``.
88101

0 commit comments

Comments
 (0)