/usr/share/doc/otter/README.Ivy is in otter 3.3f-1.1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 29 | Ivy is a system that checks Otter proofs and MACE models.
Ivy is coded in ACL2 and many soundness metatheorems have
been proved about the various programs in Ivy. See
http://www.mcs.anl.gov/~mccune/acl2/ivy
Ivy-2 is the current version. Otter-3.0.6 and MACE-1.3.4
come bundled with Ivy-2. If you wish to have Ivy-2 call Otter-3.3
and MACE-2. instead, you can do so by updating 2 Ivy files (after
configuring Ivy):
ivy-v2/ivy-sources/util/otter-mace.lisp
Change the line
(defvar mace-parms "6 60 -m1 -I -c")
to
(defvar mace-parms "-N6 -t60 -I")
ivy-v2/ivy-sources/util/ivy
Change the lines that begin
set otter_binary=
set mace_binary=
so that they refer to the Otter-3.3 and MACE-2.1 binaries, for example,
set otter_binary=/homes/mccune/bin-linux/otter33
set mace_binary=/homes/mccune/bin-linux/mace21
|