Email Gateway (Aug 19 2022 at 13:17): Email Gateway (Aug 19 2022 at 13:17):From: Gottfried Barrow <gottfried.barrow@gmx.com>
For anyone interested, this is mainly to provide a sed script which will
allow you to run the Sledgehammer ATP agsyHOL.exe, which is built using
Haskell Platform ghc.
It's been over a year since I looked at building ATPs. Basically, I've
found 4 ATPs that are easy to build and install for Cygwin: LEO-II,
Yices, agsyHOL, and Satallax. I show the script for agsyHOL at the end.
Yices is easy because the binaries are already built. Of note is there's
not a remote version of it. For Windows, there is a Cygwin "yices" and a
Windows "yices.exe". If you modify the script I give for using
agsyHOL.exe, you can use "yices.exe". There's a Yices 2, but it doesn't
work with Sledgehammer for me. Yices 1 is here:
For me, remote_leo2 and remote_satallax are finding proofs more than
leo2 and satallax, but the locals will still be useful when I'm not
online. LEO-II works in conjuction with other ATPs, so the remote
version may be configured different. If you use Sledgehammer
"overlord=true", and look at the problem file generated in
ISABELLE_HOME_USER, you'll see that leo2 is given the ATP "e".
I never saw LEO-II v1.4.3 prove anything, so I probably built a slow
version. This time, I built with the suggestion in INSTALL, "make opt
debug=false". Both remote_leo2 and leo2 are finding proofs now.
To build Cygwin satallax and leo2, use Isabelle2012-2/Cygwin-Setup.bat
to install these extras: zlib-devel, make, OCaml devel, gcc devel, g++
devel, libstdc++6-devel.
LEO-II is here: http://www.leoprover.org
Satallax is here: http://www.ps.uni-saarland.de/~cebrown/satallax/
Finally, for agsyHOL, the sources are on github:
https://github.com/frelindb/agsyHOL
It's worth installing because remote_agsyhol gives up sometimes much
easier than the local install.
The README links to http://www.haskell.org/ghc/ for the ghc, but that
didn't have everything needed for the build, but this does:
http://www.haskell.org/platform/
I didn't find any magic Haskell installs for Cygwin.
To run agsyHOL.exe under Cygwin, the scripts below (and attached)
convert Cygwin/Unix paths and filenames so that agsyHOL.exe can use them.
Regards,
GB
FILE: agsyHOL
#!/usr/bin/env bash
echo $0 $@ |
/cygdrive/e/E_2/dev/isaATP/agsyHOL-131206/win7/agsyHOL_cyg2win.sed | bash
#Change to this to check the filter.
#echo $0 $@ |
/cygdrive/e/E_2/dev/isaATP/agsyHOL-131206/win7/agsyHOL_cyg2win.sed >
/cygdrive/e/E_2/dev/isaATP/agsyHOL-131206/win7/agsyHOL_cyg2win_out.txt
#*) With Sledgehammer option "overlord=true", the input to ATP agsyhol
will be a
--time-out 60
'/cygdrive/e/E_1/02-p/pi/home/.isabelle/Isabelle2013-2/prob_agsyhol_1'
#*) The command run through agsyHOL_cyg2win.sed should look something like
E:/E_1/02-p/pi/home/.isabelle/Isabelle2013-2/prob_agsyhol_1
#*) With "overlord=false", the problem file will be created in Cygwin /tmp,
FILE: agsyHOL_cyg2win.sed
#!/usr/bin/sed -f
{
s@/tmp@E:/E_2/dev/Isabelle2013-2/contrib/cygwin/tmp@g
s@/cygdrive/e@E:@g
s@win7/agsyHOL@win7/agsyHOL.exe@g
s@--proof@@g
}
something like:
--time-out 60 '/tmp/isabelle-jv9020/prob1616544_1'
something
Last updated: Apr 19 2024 at 20:15 UTC