[isabelle] Cygwin script for SledgeH agsyHOL; leo2, yices, satallax local Cygwin installs



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:

http://yices.csl.sri.com

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
#   command in the file $ISABELLE_HOME_USER/prob_agsyhol_1, something like:
# '/cygdrive/e/E_2/dev/isaATP/agsyHOL-131206/win7/agsyHOL' --proof --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_2/dev/isaATP/agsyHOL-131206/win7/agsyHOL.exe --time-out 60 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,
#   which is not seen as /tmp to Windows.

FILE: agsyHOL_cyg2win.sed

#!/usr/bin/sed -f
{
  s@/tmp at E:/E_2/dev/Isabelle2013-2/contrib/cygwin/tmp at g
  s@/cygdrive/e at E:@g
  s at win7/agsyHOL at win7/agsyHOL.exe at g
  s at --proof@@g
}

# s@/cygdrive/e at E:@g is needed for "overlord=true".

# Change "E:/E_2/dev/Isabelle2013-2" to your Isabelle install folder.
# Change "win7" to some part of your path that's before agsyHOL.exe
# The scripts "agsyHOL" and "agsyHOL_cyg2win.sed" should in the folder.

# *) With Sledgehammer option "overlord=false", the input will be something like: # '/cygdrive/e/E_2/dev/isaATP/agsyHOL-131206/win7/agsyHOL' --proof --time-out 60 '/tmp/isabelle-jv9020/prob1616544_1'
# *) The sed script does the following:
#    *) Changes tmp path from a Cygwin path to a Windows path.
#    *) Changes "/cygdrive/e" to "E:".
# *) Adds the "exe" extension to "agsyHOL"; the "win7" is just for something
#       unique in the path to search on.
#    *) Eliminates "--proof" because it causes an error.








#!/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 
#   command in the file $ISABELLE_HOME_USER/prob_agsyhol_1, something like:
#     '/cygdrive/e/E_2/dev/isaATP/agsyHOL-131206/win7/agsyHOL' --proof --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_2/dev/isaATP/agsyHOL-131206/win7/agsyHOL.exe --time-out 60 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,
#   which is not seen as /tmp to Windows.




#!/usr/bin/sed -f
{
  s@/tmp at E:/E_2/dev/Isabelle2013-2/contrib/cygwin/tmp at g
  s@/cygdrive/e at E:@g
  s at win7/agsyHOL at win7/agsyHOL.exe at g 
  s at --proof@@g
}

# s@/cygdrive/e at E:@g is needed for "overlord=true".

# Change "E:/E_2/dev/Isabelle2013-2" to your Isabelle install folder.
# Change "win7" to some part of your path that's before agsyHOL.exe 
# The scripts "agsyHOL" and "agsyHOL_cyg2win.sed" should in the folder.

# *) With Sledgehammer option "overlord=false", the input will be something like:
#     '/cygdrive/e/E_2/dev/isaATP/agsyHOL-131206/win7/agsyHOL' --proof --time-out 60 '/tmp/isabelle-jv9020/prob1616544_1'
# *) The sed script does the following:
#    *) Changes tmp path from a Cygwin path to a Windows path.
#    *) Changes "/cygdrive/e" to "E:".
#    *) Adds the "exe" extension to "agsyHOL"; the "win7" is just for something
#       unique in the path to search on.
#    *) Eliminates "--proof" because it causes an error.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.