Twelf Copyright (C) 1997, 1998, Frank Pfenning and Carsten Schuermann Authors: Frank Pfenning Carsten Schuermann With Contributions by: Iliano Cervasato Jeff Polakow Twelf is an implementation of - the LF logical framework, including type reconstruction - the Elf constraint logic programming language - a meta-theorem prover for LF ====================================================================== Files: NOTES --- remarks and todo list, most recent notes are at the top README --- this file, including some instructions for compilation TAGS --- tags file, for use in Emacs TEST/ --- test files, try use "TEST/all.sml"; sources.cm --- enables CM.make (); load.sml --- enables use "load.sml"; (* especially for MLWorks *) bin/ --- utility scripts ====================================================================== Standard ML, Revision of 1997: If it is not installed already, please check SML of New Jersey [free] http://cm.bell-labs.com/cm/cs/what/smlnj/index.html (version 110 or higher) MLWorks [commercial] http://www.harlequin.com/products/ads/ml/ml.html -------------------- Loading Twelf: Connect to Twelf root directory Start SML/NJ 110 or MLWorks CM.make (); (* in SML/NJ 110, sml-cm *) OR use "load.sml"; (* in SML/NJ 110, sml or MLWorks *) -------------------- Running Examples: To define configuration val = Twelf.Config.read "examples//sources.cfg"; To load files and start top-level for queries (note that you have to replace `-' (dash) by `_' (underscore) in the name of the in order to conform to the lexical conventions of ML). Twelf.Config.load ; Twelf.top (); To compile files and read queries (see below for format) Twelf.reset (); Twelf.loadFile "examples//examples.quy"; -------------------------------------------------- Current Examples (see examples/README) arith Associativity and commutative of unary addition ccc Cartesian-closed categories [incomplete] church-rosser Proof of Church-Rosser theorem for untyped lambda-calculus compile Various compilers starting from Mini-ML fol Simple theorems in first-order logic guide Examples from Users' Guide lp Logic programming, uniform derivations lp-horn Horn fragment of logic program mini-ml Mini-ml, type preservation and related theorems polylam Polymorphic lambda-calculus prop-calc Natural deduction and Hilbert propositional calculus units Mini-ML extended with units [incomplete] -------------------- Query Format for Files: %query A. %query X : A. where is the expected number of answers or * (for infinity), and is the bound on the number of tries or * (for infinity), and A is the goal type and X an optional proof term variable. %solve c : A. finds the first solution M for the query A, abstract over the remaining free variables and create a definition c : A = M. -------------------- Flags (with defaults): These are now uniformly accessible through the Twelf structure (see the User's guide or src/frontend/twelf.sig). Global.chatter := 3; (* chatter levels: 0 = nothing, 1 = files, 2 = number of query solutions, 3 = declarations 4 = debugging O 5 = debugging I, 6 = debugging II *) TpRecon.doubleCheck := false; (* re-check entries after reconstruction *) (* Print appearance *) Print.implicit := false; (* print implicit arguments *) Print.printDepth := NONE; (* SOME(d): replace level d expressions by '%%' *) Print.printLength := NONE; (* SOME(l): replace lists longer than l by '...' *) Formatter.Indent := 3; (* number of spaces for indentation level *) Formatter.Pagewidth := 80; (* default page width for formatting *) (* see formatter/formatter.sig for more *) Compile.optimize := true (* prevent optimizations if false *) -------------------- Timing: Timers.show (); (* show internal timers and reset *) Timers.reset (); (* reset internal timers *) Timers.check (); (* check internal timers, but do not reset *) Currently, the timing information for the solver includes the time taken by the success continuation. This is non-trivial if the success continuation prints the answer substitution, but negligible otherwise. -------------------- Generate the file load.sml for MLWorks or SML w/o the Compilation Manager with CM.mkusefile "load.sml"; Make sure the current working directory is the root file of the implementation. To run MLWorks, use Andrew SparcStation (telnet sun4.andrew) and invoke /afs/andrew/scs/cs/mlworks/ultra/bin/mlworks-basis possibly using -tty option. To cut down on printing: Shell.Options.set (Shell.Options.ValuePrinter.maximumStrDepth, 0); -------------------- Create TAGS file with cd src ../bin/tag-twelf -------------------- In SMLofNJ: say "make" in *shell* in the Twelf toplevel directory (does not remove the old server but overwrites it!) SMLofNJ.Internals.GC.messages false; signature X = SML_OF_NJ; (* to see specific signature *) CM.make' ("server.cm"); (* CM.make' ("server.cm", true) for >= 110.3 *) SMLofNJ.exportFn ("bin/.heap/twelf-server", Server.server); if SMLofNJ.exportML ("bin/.heap/twelf-sml") then (print Twelf.version; Timing.init ()) else (); Compiler.Control.Print.printDepth := 100; (* default: 5 *) Compiler.Control.Print.printLength := 80; (* default: 12 *) Compiler.Control.Print.signatures := 1; (* default: 2 *) Compiler.Control.Print.linewidth := 79; Compiler.Control.Print.stringDepth := 200; (* default: 70 *) OS.FileSys.chDir "directory"; (* also: Twelf.OS.chDir "directory"; *) OS.FileSys.getDir (); (* also: Twelf.OS.getDir (); *) OS.Process.exit (OS.Process.success); (* also: Twelf.OS.exit (); *) -------------------- Editing under CVS: % setenv CVSROOT /afs/cs/project/twelf/CVS % cvs checkout twelf will create the directory twelf/ and all subdirectories with most recent Twelf sources. Edit (possibly several days, even weeks), and then check in with % cvs commit -m "log message" twelf (or relevant filenames only, works recursively) (might require merging) To update your copy of the source: % cvs update twelf (might require merging) -------------------- Profiling (under MLWorks): (see /afs/cs/project/twelf/work/PROFILE/README for detailed profiling) For the visual summary profile tool: % telnet sun4.andrew.cmu.edu (on original machine: xhost +unixNN.andrew.cmu.edu) % cd /afs/cs/project/twelf/research/twelf % /afs/andrew/scs/cs/mlworks/ultra/bin/mlworks-basis Set Prefereces>Compilers> for call-counting and debugging - Shell.Options.set (Shell.Options.ValuePrinter.maximumStrDepth, 0); - use "load.sml"; - Twelf.Config.load (Twelf.Config.read "examples//test.cfg"); -------------------- Release: *** Note: the CVS protocol for release has not yet been established *** For file-oriented operations, see file DISTRIBUTE -------------------- Installation: *** For accurate up-to-date information see file README *** gunzip twelf.tar.gz tar -xvf twelf.tar cd twelf make (* requires version 110 of SML/NJ *) -------------------- Notes: - use lazy name assignment in contexts to permit printing without early name commitment?