====================================== ===== Logician's Toolkit 1.0.0.1 ===== ====================================== Samuel Howse Poohbist Technology 607 Francklyn Street Halifax, Nova Scotia B3H 3B6 Canada Web page: http://nummist.com/poohbist/ Email: samuelhowse@poohbist.com Phone: 1-902-422-0845 Copyright (c) 2006 Samuel Howse. All rights reserved. ====================================== ================== === 1. Welcome === ================== Thanks for your interest in Logician's Toolkit, which integrates various logical tools with MSBuild, the build system used by Microsoft Visual Studio .NET 2005. Currently these logical tools are supported: - Coq proof assistant 8.0pl3 (http://coq.inria.fr/) coqc and coqdoc (HTML and LaTeX) Comments or questions are welcome: please contact Samuel Howse (see contact information at the beginning of this document). ======================= === 2. Requirements === ======================= To install Logician's Toolkit, you need: - Microsoft Windows - Microsoft .NET Framework 2.0, which will be installed automatically with Logician's Toolkit if required - an Internet connection (to install or update Logician's Toolkit) - 20 megabytes of free disk space under your user profile - 20 megabytes of free disk space under the Program Files folder, and Windows privileges to write to the Program Files folder (to install, update or uninstall Logician's Toolkit libraries where they can be referenced by your MSBuild projects) Related software: - Microsoft Visual Studio .NET 2005, including Express Editions (if you want to build your MSBuild projects within Visual Studio) - The logical tools you want to use ===================== === 3. Installing === ===================== 1. Start by following the online instructions. 2. After installation, select "Poohbist Technology" then "Logician's Toolkit" from the Start menu. Logician's Toolkit Manager will start. 3. Click "Install Libraries" to install Logician's Toolkit libraries under the Program Files folder, where they can be referenced by your MSBuild projects. A dialog box will tell you the directory containing "LogicianToolkit.dll". Make a note of this directory, because you will need to specify it within your MSBuild projects. WARNING: Do not store anything in this directory, because this directory will be deleted when updating or uninstalling Logician's Toolkit. =================== === 4. Updating === =================== 1. Close any applications that may be using Logician's Toolkit libraries under the Program Files folder (e.g. Visual Studio). 2. Select "Poohbist Technology" then "Logician's Toolkit" from the Start menu. If you are connected to the Internet, any available updates will automatically be downloaded before Logician's Toolkit Manager starts. 3. After Logician's Toolkit Manager starts, click "Install Libraries" to update the Logician's Toolkit libraries under the Program Files folder. ======================= === 5. Uninstalling === ======================= 1. Close any applications that may be using Logician's Toolkit libraries under the Program Files folder (e.g. Visual Studio). 2. Select "Poohbist Technology" then "Logician's Toolkit" from the Start menu. Logician's Toolkit Manager will start. 3. Click "Uninstall Libraries" to uninstall Logician's Toolkit libraries under the Program Files folder. 4. Close Logician's Toolkit Manager. 5. Choose Control Panel, choose "Add or Remove Programs", select Logician's Toolkit in the list, and click "Change/Remove". Follow the instructions. =================================== === 6. Using Logician's Toolkit === =================================== To use Logician's Toolkit, you need to do some manual editing of your MSBuild project file. IMPORTANT: To edit your MSBuild project file, close your solution and project in Visual Studio, and use an external text editor (e.g. Notepad). 1. Create a Visual Studio project as usual. For example, create a C# Console Application called "MyConsoleApplication". 2. In Visual Studio, save everything, then close your solution. 3. Use an external text editor (e.g. Notepad) to edit your project file (e.g. "MyConsoleApplication.csproj"), as indicated in the following sections. 4. Save your project file in the external editor, close the external text editor, and re-open your solution in Visual Studio. IMPORTANT: When re-opening your solution, you may receive a security warning indicating that your project has been customized. If your project comes from a trused source, select "Load project normally". 5. Rebuild your solution. ============================================ === 7. Editing your project file for Coq === ============================================ ---------------------- --- 7.1. UsingTask --- ---------------------- Just after the opening tag, add the following: You may need to adjust the value of AssemblyFile, depending on the directory you noted during installation in section 3, step 3. ---------------------- --- 7.2. ItemGroup --- ---------------------- In the part of your project file where ItemGroups are defined, add the following: Include all your Coq Vernacular (".v") files, which may span multiple directories under your project directory. Relative paths are relative to your project directory. IMPORTANT: The order of files within the Vernac ItemGroup is important, and affects compilation order with coqc, and the order within the documentation generated by coqdoc. -------------------- --- 7.3. CoqTask --- -------------------- Logician's Toolkit includes CoqTask, which runs coqc and coqdoc (HTML and LaTeX) for you. Your project file may call CoqTask within the BeforeBuild target. IMPORTANT: The tag may be commented out. If so, move it outside the comment. Just after the opening tag, add the following: CoqBinDir is used to locate the Coq tools. The above value of CoqBinDir assumes that the COQBIN environment variable has been set. VernacDir is the root directory of your Vernacular files. Usually this is your project directory itself, in which case just write ".". VernacFiles references the Vernac ItemGroup defined in section 7.2. VernacFiles must contain at least one file, and cannot contain duplicates. All files in VernacFiles must be under VernacDir, must have the ".v" extension, and must have a non-empty name excluding the extension. Subdirectories of VernacDir must not have extensions. OutputDir is the output directory, which will contain the compiled Vernacular files (".vo") and generated documentation. A relative path is relative to your project directory. CoqTask will not proceed if OutputDir already exists. Therefore, you must use the RemoveDir task to remove OutputDir prior to calling CoqTask. WARNING: Do not store anything in OutputDir, because RemoveDir will delete it. VernacCopyDirLogical is the Coq logical directory path corresponding to VernacDir (more precisely, to the copy of VernacDir created within OutputDir). VernacCopyDirLogical must be non-empty, and is a prefix in the logical module path of each file in VernacFiles. For the example given, the logical module paths are as follows: Physical module path Logical module path -------------------- ------------------- A\B\X.v MyCompany.MyProject.A.B.X A\Y.v MyCompany.MyProject.A.Y Z.v MyCompany.MyProject.Z --------------------------------- --- 7.4. Example project file --- --------------------------------- The following is an example project file. IMPORTANT: Copying and pasting the entire example is NOT recommended, because you will overwrite parts of your project file unrelated to Logician's Toolkit. --- MyConsoleApplication.csproj ------------------------------------------------ Debug AnyCPU 8.0.50727 2.0 {04009BEE-1963-41D9-99E7-B115F3DFB5A7} Exe Properties MyConsoleApplication MyConsoleApplication true full false bin\Debug\ DEBUG;TRACE prompt 4 pdbonly true bin\Release\ TRACE prompt 4 -------------------------------------------------------------------------------- --- A\B\X.v -------------------------------------------------------------------- (** * X *) Definition x := 1. -------------------------------------------------------------------------------- --- A\Y.v ---------------------------------------------------------------------- (** * Y *) Require Import MyCompany.MyProject.A.B.X. Definition y := x + 1. -------------------------------------------------------------------------------- --- Z.v ------------------------------------------------------------------------ (** * Z *) Require Import MyCompany.MyProject.A.B.X. Require Import MyCompany.MyProject.A.Y. Definition z := x + y + 1. Definition w := 2 * z. -------------------------------------------------------------------------------- ------------------------------------- --- 7.5. Rebuilding your solution --- ------------------------------------- After successfully rebuilding your solution, OutputDir should contain compiled Vernacular files (".vo") and generated documentation (HTML and LaTeX). IMPORTANT: For LaTeX, coqdoc's --body-only option is used, so you must include the coqdoc generated ".tex" file as part of a complete document. You may wish to examine the build output window to see what coqc and coqdoc command line arguments were used, and see standard error and standard output from coqc and coqdoc. ---------------------------------------- --- 7.6. CoqTask optional parameters --- ---------------------------------------- In addition to the required parameters described above, CoqTask has some optional parameters: Parameter Default Description --------- ------- ----------- InputStateUse true If "true", use the default input state. If "false", do not use an input state (coqc's -nois option). ResourceFileUse true If "true", use a resource file. If "false", do not use a resource file (coqc's -q option). ResourceFile The resource file. Must be omitted if ResourceFileUse is "false". If omitted and ResourceFileUse is "true", coqc locates the resource file in the default way. HTMLBodyOnly false If "true", HTML files contain only bodies (coqdoc's --body-only option). If "false", HTML files are complete. HTMLTitle Title for HTML files (coqdoc's -t option). If present, must be non-empty. If omitted, the -t option is not used. HTMLModuleTitlesInclude true If "true", HTML files include module titles. If "false", module titles are omitted in HTML files (coqdoc's -s option). HTMLIndexMultiInclude false If "true", a multi-file HTML index is generated (coqdoc's --multi-index option). If "false", a single-file HTML index is generated. HTMLStandardLibLinksInclude true If "true", HTML files include Coq standard library links. If "false", Coq standard library links are omitted in HTML files (coqdoc's --no-externals option). HTMLStandardLibURI URI of the Coq standard library HTML documentation (coqdoc's --coqlib option). Must be omitted if HTMLStandardLibLinksInclude is "false". If present, must be non-empty. If omitted and HTMLStandardLibLinksInclude is "true", coqdoc uses its default URI. LatexModuleTitlesInclude true If "true", the LaTeX file includes module titles. If "false", module titles are omitted in the LaTeX file (coqdoc's -s option).