hol.install


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

# See also:
# https://github.com/HOL-Theorem-Prover/HOL/commit/c2615dd

post_install() {
    cd /opt/hol
    poly < tools/smart-configure.sml
    bin/build --relocbuild

    cat <<EOF
*************************************************
Emacs HOL mode
*************************************************
Put

   (autoload 'hol "/opt/hol/tools/hol-mode"
     "Runs a HOL session in a comint window.
   With a numeric prefix argument, runs it niced to that level
   or at level 10 with a bare prefix. " t)

into your .emacs file
EOF
}

post_upgrade() {
    cd /opt/hol
    poly < tools/smart-configure.sml
    bin/build --relocbuild
}