Open Logic Quick Start Guide

[Chad and Samara have documented the steps required to download and compile the Open Logic Text, and written a “quick start” guide for people who aren’t experienced with Git or may not even have LaTeX.  The most up-to-date version of this document can be found on the OLP wiki here.]

This page describes all the steps required to install and compile the Open Logic Text on your computer, including installation of LaTeX (the typesetting program OLT uses) and Git. Please see the pages on LaTeX and Git for more information on what those are if you don’t know already. You can avoid using Git by downloading OLT directly, but it makes it harder for you to keep up-to-date with changes to the text, and us to incorporate any contributions you make.

Installing LaTeX and Git

A LaTeX environment is necessary for both building a version of the Open Logic Book and contributing to the project. While it is possible to build the book without [Git], the project is currently hosted on Github, and you will need Git to contribute to the project.

Linux

The easiest way to get a working LaTeX environment on the majority of Linux systems is to install TeX Live through the package manager. The name of the package varies (texlive for Debian and Ubuntu with aptitude, texlive-most for Arch Linux with pacman, texlive and texlive-latex for OpenSUSE with libzypp). If TeX Live is not available through your distribution’s package manager or your distribution does not use a package manager (Gentoo), follow the instructions on the website to download and install TeX Live. To compile a .tex file into a .pdf file, use the pdflatex command at the command prompt.

Similarly, install git through your package manager. For an introduction to git specific to the Open Logic Project, see below.

Windows

Download the TeX Live installer for windows and run the executable. The installer will guide you through the installation process. Do not be alarmed if it takes a long time for the installer to download all the required packages. After installation is complete, you should be able to double click on latex source files to open them in the editor, from where you can click the green “play” button in the upper left hand corner of the interface to compile the document.

If you only want to build a custom version of the book, you don’t need to install Git on your system, it is enough to click the “Download ZIP” button on the right hand side of the Github interface on the project page, and extract the contents to a convenient location. If you want to contribute to the project, the easiest way is probably to install Github for Windows.

OSX

Install MacTeX to obtain a LaTeX environment. If you’re comfortable with the command line, install Git. If you choose the command line most of the instructions and advice for Linux systems will apply to you also. If you prefer a GUI, install Github for Mac. Ideally you will install both, allowing you to try typing the git commands as they appear for Linux users, with the GUI as a fallback if something isn’t working for you.

Git Primer: “Fork” and Other Verbs

Git is the distributed version control system used by the Open Logic Project. It allows multiple people to work on the project at the same time, and makes creating your own version of the project and incorporating your changes into the main project easy. A collection of files managed with Git is called a repository. The Open Logic Project repository is hosted on Github, a hosting service for Git repositories with a nice web browser interface. Git is a somewhat complicated system, and can be intimidating for new users. The aim of this section is to help you become comfortable with what Git is and get you started using it.

To contribute to the Open Logic Book, you will probably want to register an account with Github. While this is not necessary if you are looking only to use the text, and not strictly necessary if you would like to contribute to the project, it will make both of these things far easier. During the account creation process you may be asked to choose a payment plan. The free one will suffice.

Once you have a Github account, the first thing you should do is create a copy of the the OpenLogic repository tied to your account. To do this, log in to your Github account, and click the “Fork” button on the page for the repository (In the upper right hand corner of the web interface). A copy of the repository should now be displayed on your Github profile page at https://github.com/<yourusername>. Any changes you make to this repository will not be reflected in the main OpenLogic repository. You can request that your changes be added to the main repository by issuing a “pull request”, covered here.

Now that you have your own copy of the project files on Github, the next step is to get those files on your computer. If you’re using git from the command line, navigate to the directory you want the files to be in and enter

git clone https://github.com/<yourusername>/OpenLogic

at the command prompt.

If you’re using the Github GUI interface for Windows (or the similar application for OSX), you need to link your Github account to the instance of the software on your computer. If you are not prompted to do this when you first start it up, you can do it by clicking the gear icon in the upper right corner of the main window of the application. Once you have linked your account, you will be able to clone your fork of the OpenLogic repository by clicking the plus sign icon in the upper left corner of the main window, and selecting “clone”, and finally selecting your fork of the repository. You will be prompted to enter a save location, and it doesn’t matter what this is as long as you remember it. Once you have done this, the copy of the files on your computer will behave much the same as for Linux and OSX users, with the difference that you will have to use the Github for Windows application instead of the command line to do the things described below. The Github for Windows application comes with a low-powered “shell” that will act a bit like a Unix command prompt, and makes it easier to perform more complex operations should the need arise. Please consult the documentation for more information on the Github for Windows application.

There are three sorts of basic changes you can make to the repository, adding new files, changing old files, and removing old files. To add a new file called file.ext to the repository, move the file to the OpenLogic directory on your computer and type git add file.ext. This tells git to keep track of file.ext. To make changes to a file that git is already keeping track of (such as the files that were in the repository when you cloned it), simply edit the file. To remove a file called file.ext from the repository, type git rm file.ext at the command prompt. This not only tells git to stop tracking the file, but deletes it. To record changes you have made, type git commit -m "summary of changes" at the command prompt. If you don’t want to record your changes, you can type git reset to restore the repository to the state it was in immediately after the last commit. Finally, to synchronize the changes you have made with the version of the repository on Github, type git push at the command prompt (after committing your changes).

If you are using Github for Windows it easy to commit and push changes. Once you have edited a document that Git is currently tracking, or added a new document to the OpenLogic directory on your computer, it will pop up in Github for Windows as an uncommitted change. You can select/deselect files to commit at this point. You must write a summary of the commit, and are given the option to add a short description. Once you have done so, hit the commit button. At this point, the changes you have made will not be reflected in the version of the repository on Github. You should see that the sync button at the top of the application now has a number beside it, reflecting the commits that have yet to be pushed to Github. When you are ready to push your changes, click the sync button.

To request that your changes be reflected in the main Open Logic Project repository, submit a pull request.

The pull request can be done directly from Github for Windows, but the application does not have a compare and review feature. If you’d like to do a comparison of the changes you’ve made before submitting a pull request, follow the instructions linked to above. If you’d like to do the pull request directly from Github for windows, you can do so by clicking the pull request button to the left of the sync button. The program will show you which branch the changes are being taken from, and where you are sending the updates to. The default options for the pull request should be correct, but you may want to double check that the pull request is being sent to the correct place (in most cases, this should be from your master branch into OpenLogicProject/master). You’ll have to enter a title, and if you’d like, a description. Then click “Send pull request”, and you’re done!

If you want to update your copy of the repository to include changes in the main repository that have happened since you made the copy, read this. Alternatively, and if the “upstream” changes can be synced into your fork without manual intervention, you can use the Github web interface to sync changes from the main repository into your fork. To do this, proceed as if you were sending a pull request, but switch the “base fork” and “head fork”. (The base for should be “yourid/OpenLogic”, the head fork “OpenLogicProject/OpenLogic”; and in each case the branch should be “master”). Github will tell you if an automatic merge is possible. If it is, you will have sent yourself a pull request that you can merge.

Building the Open Logic Book

Once you have a working LaTeX installation and a copy of the Github repository on your computer, you can compile a custom edition of the Open Logic Book. To build the complete book (all chapters included), compile the open-logic-complete.tex file. The open-logic-debug.tex file also produces a complete PDF, but with extra debugging information that helps to keep track of labels of theorems and the like, and which files which parts of the final PDF come from.

The files in the main directory should not be changed. To make a customized version of the book, instead go to the courses directory, and copy the sample subdirectory. Your copy should contain two files, open-logic-sample.tex and open-logic-sample-config.sty. You may rename these files, e.g., to myversion.tex, myversion-config.sty (where “myversion” can be any string). You can make any changes to the layout, fonts, page style, etc., in myversion.tex you like. You can also rearrange the order of the parts and chapters or leave out parts you do not want included. For instance, to exclude the part on computability theory, change the line

\olimport[computability]{computability}

to

%\olimport[computability]{computability}

in myversion.tex.

To change the OLT-specific configurations, e.g., how formulas are printed or whether formulas are called “formulas”, “formulae”, or “wffs”, open myversion-config.sty in a text editor. The configuration options are explained in open-logic-config.sty in the main directory. Copy any configuration option you would like to change to myversion-config.sty and make your changes.

Finally, generate a PDF of your custom textbook by compiling the myversion.tex file with pdflatex.

You can keep different versions of the text in different directories by following the same steps as before.

Open Logic Project Special LaTeX Syntax

The Open Logic Book is configurable, you can choose which word you want the book to use for a number of technical terms, and more! To achieve this we preface configurable elements with a special syntax in the .tex files of book chapters. This makes writing chapters for the text a bit more complicated that it would have otherwise been, but not by too much. In addition to this section, you will have to read the open-logic-config.tex file in the top level of the OpenLogic repository, which contains a complete listing and explanation of the syntax.

The pattern common to all of the special syntax is that instead of using the standard LaTeX macros for a particular symbol, you use a specific Open Logic Project macro, e.g., \lif for a conditional symbol instead of \rightarrow. When the document is compiled, the special macro is replaced with text according to the configuration of that instance of the book. Sometimes the OLP uses the standard macro, e.g., \land. For example, one of the configuration options allows you to choose between the Greek and Latin alphabets for the symbols used to represent formula metavariables. For this to work, when you write material for the book you must use the syntax !A, !B, and so on for formula metavariables. Other configurable things include the symbols used for various sets of numbers (natural, real, integer, and so on), logical connectives (including quantifiers), and the syntax for relations like provability and entailment.

“Tokens” are slightly different than the rest of the configurable syntax. The idea is that in addition to using different symbols for the same thing across book instances, we might also want to use different words. This is done by treating some words, like “formula” and “variable” differently, as Tokens. When you use a tokenized word in material for the Open Logic book, instead of typing it, you have to enclose it in braces and place two exclamation points in front of it. That is, instead of typing

formula

type

!!{formula}

instead. To typeset the (configurable) plural form of a token word, type

!!{formula}s

and to typeset the token word with a (configurable) article, type

!!a{forumla}

The complete list of tokenized words and instructions for customizing tokens can be found in the configuration file open-logic-config.tex

Summary of Options for Converting the OLP to Other Formats

[Chad is investigating options for converting the OLT to formats other than PDF.  Other open textbook projects, especially in mathematics, have this problem: while LaTeX is very versatile, its non-standardized format makes it hard to convert to HTML, XML, end e-reader formats such as PUB.  In this first post Chad reports on available tools.The latest version of this document is here. -RZ]

The Open Logic Book is currently written in LaTeX, and relies on a number of book specific macros for its customizability. We want to convert the book to other formats, for example HTML and EPUB to make it more accessible. To that end, we have been investigating options for converting LaTeX to other formats. We focus heavily on the conversion of mathematics typeset in LaTeX to other formats, because all of the tools do plain text very well.

The Ideal Situation

My “blue sky” typesetting system for formal systems (logic, mathematics, and so on) is one in which the formal objects are specified completely according to the rules of the system they are a part of, and are typeset by a specialized process. Targeting different markup languages and display formats would be a matter of writing a typesetting proces for the system whose objects you want to typeset for each type of output. This approach is completely modular, with the content entirely separate from its presentation. Additionally, for many formal systems we can verify the sensibility of the formal object in question automatically (as in type checking for dependently typed programming languages). Such a system is absolutely possible with existing techniques, but would likely require several years to reach a point where it could be used for everyday typesetting, and would require much of the Open Logic Book to be rewritten. It is therefore clearly not an acceptable solution to the problem we have now.

The Actual Situation (LaTeX is terrible)

The TeX typesetting system and LaTeX macro package are both arcane and very poorly documented, having been built up in an ad-hoc way by a multitude of different people over many decades. Further complicating matters is that LaTeX “macros” can perform arbitrary computations, and can change the state of “registers” on which the output of other macros may depend. Thankfully, most LaTeX documents use only a small set of macro packages which contain only relatively sane macros of the “replace this with that” variety. It is these common packages that are supported by the available conversion tools. While many of the conversion tools provide an extension mechanism, allowing us to add support for new and exotic packages, it is far easier to deal with “common LaTeX”. Additionally, many people consider LaTeX an archival format, and suitable for the long term preservation of mathematical content. This becomes more of a funny joke than a serious proposition when arbitrary macro packages are introduced.

Conversion Tools

This section is a summary of the available conversion tools

Tex4ht

Tex4ht is really a collection of smaller programs that each do something more specific. The end result is a converter that works on everything I was able to find, but that responds to most mathematical content by constructing a poor quality bitmap image and embedding it in the resulting HTML document. The software is unfinished and unpolished, and this makes sense because the main author died unexpectedly in 2009. The documentation is relatively poor, and while it is purported to be extensible, instructions for extending it are nowhere to be found. The stability and future availability of this tool both look poor. I cannot recommend using this for the Open Logic Book.

Pandoc

Pandoc aims to be a universal document conversion tool, and does this very well for the most part. The aim of the project, however, is not the conversion of mathematical content, which makes sense as most formats don’t really support it. It has an excellent community and will likely be maintained for some time to come. Anything we can have Pandoc do for us is already done by the other converters on the list, which are more specialized and relevant to our problem.

LaTeXML

LaTeXML was developed specifically for the purpose of converting LaTeX math to other formats. It does this reasonably well, and is a mature technology. The documentation is good, and the converter is extensible, allowing us to add support for new packages. The software will probably be available for some time. The downside is that the whole thing is written in Perl, which is notoriously unreadable and difficult to maintain. Extending the system involves writing “bindings” for each package one wants to support, which tell the converter how to treat each new macro.

Hevea

A newer (2013) conversion tool written in OCaml with support for common latex math packages. The software is extensible much as LaTeXML is, and has some nice features (good error reporting and warnings, sane looking extension framework). The software appears to be actively developed, and the online manual appears complete. Also encouraging is that is has been used as part of a LaTeX to EPUB conversion toolchain with good results.

Things We Could Do

The following could all work.

Extend LaTeXML

By developing bindings for all the packages we need and potentially changing the include structure of the book, we might be able to convert it to structured HTML using only LaTeXML. This would be nice. We could also “cheat” and develop bindings for the open logic project macros directly, ignoring all the packages they depend on.

Extend Hevea

As above, but we get to work with OCaml instead of Perl.

Preprocess The Book To Common Latex

We could also write out own preprocessor that converts the special syntax to common latex, which is dealt with very well by both Hevea and LaTeXML, and then use either of those. This would be no more difficult than writing bindings for either of the two tools. It would also allow us to do literally whatever we want to syntax wise.

What I Think We Should Do

My opinion is that the best approach is to preprocess the book using a custom tool, and then feed the resulting common latex through Hevea. My reasoning is that writing bindings for LaTeXML or Hevea amounts to specifying how to replace the new commands with common latex commands anyway, just in a more restrictive setting. We have to write our own parser for the custom commands, but this is not actually such a big deal. If done correctly, it would also be extensible. The preprocessor should read “replacement instructions” from a configuration file (much like bindings for the other two). From a format convertibility and technical simplicity standpoint, building the custom syntax and book configurability mechanisms in LaTeX was a mistake. With an external preprocessor, we can build in arbitrary functionality more simply, and can do complicated things while keeping the generated markup “common LaTeX”. The reason I suggest Hevea instead of LaTeXML is that if we succeed in converting to HTML with Hevea, we can use the Tex2Ebook toolchain to generate EPUB with no modifications. LaTeXML would also work for generating HTML.

Wiki Now Part of Git Repository

The Github Wiki we use to document aspects of the project is now a submodule in the OpenLogic repository.  If you clone the repository (or clone a forked copy or pull changes in an existing clone), there now is an empty “doc” subdirectory.  You can safely ignore this directory, as it’s probably easier to access the Wiki documentation online.

If for some reason you do want the wiki pages in your own fork/clone keep Wiki submodule up to date with the official repository, you might want to read up on how to work with submodules.  The short:

  • Go to the doc/ subdirectory
  • Say “git submodule init”
  • Say “git submodule update”

Now, whenever you say “git pull” to update the OLT itself, you can also run “git submodule update –remote” to update the wiki.

These pages are written in Markdown format (hence the .md file extensions).