The TPTP parser is generated using ML-Yacc and relies on the ML-Yacc
library to function. The ML-Yacc library is an external piece of
software that needs a small modification for use in Isabelle. The
file "make_tptp_parser" patches the ML-Yacc library, generates the
TPTP parser, and patches that to conform to Isabelle's naming
conventions.
In order to generate the parser from its lex/yacc definition you need
to have the ML-Yacc binaries. The sources can be downloaded via SVN as
follows:
svn co --username anonsvn \
https://smlnj-gforge.cs.uchicago.edu/svn/smlnj/ml-yacc/trunk ml-yacc
ML-Yacc is usually distributed with Standard ML of New Jersey, and its
binaries can also be obtained as packages for some distributions of
Linux.
The generated parser needs ML-Yacc's library. This is distributed with
ML-Yacc's source code, in the lib/ directory.
Assuming that you've got the ml-lex and ml-yacc binaries, and have a
copy of the ML-Yacc sources in this directory, then running
"make_tptp_parser" will generate two files:
ml_yacc_lib.ML -- this is a compilation of slightly modified files
making up ML-Yacc's library.
tptp_lexyacc.ML -- this is a compilation of the SML files making up
the TPTP parser.
Nik Sultana
8th March 2012