README

1. What's here.

   This directory contains Tarski, a system for computing
   with Tarski Formulas.  Tarski relies on Saclib, Qepcad, and
   a modified version of MiniSAT, so those systems are included
   in this root as well.

2. Contributors
   Tarski includes code contributions from Chris Brown and
   Fernando Vale-Enriquez.

3. Building Tarski

   Tarski should build pretty easily on Linux systems.
   The latest version should compile on Mac and Windows systems too.
   Also, a Java Native Interface (JNI) library can be built.
   Alternatively, Tarski can run in a web browser as well.

   a. Dependencies on Linux (on Debian based systems)
      The following external packages must be installed for Tarski
      to build (e.g. sudo apt-get install <name>):
      - libz-dev (for MiniSAT)
      - libssl-dev (for the Tarski Interpreter)
      - libreadline-dev (for the Tarski Interpreter)

      Dependencies on Mac
      After installing homebrew you need the following libraries
      (e.g. sudo brew install <name>):
      - openssl
      - readline

      Dependencies on Windows
      Make sure you set Developer Mode and check out the sources
      after enabling symbolic link support.
      After installation of MSYS2 you have three options, either
      CLANG64 (preferred), CLANG32 or the MSYS environment should be used.
      You need the following packages (e.g. pacman -S <name>):
      - base-devel
      - mingw-w64-clang-x86_64-cc (only for CLANG64)
      - mingw-w64-clang-i686-cc (only for CLANG32)
      - gcc (only for MSYS)
      The following packages are required for CLANG64/CLANG32
      - mingw-w64-clang-<ARCH>-readline
      - mingw-w64-clang-<ARCH>-openssl
      - mingw-w64-clang-<ARCH>-zlib
      where <ARCH> is either x86_64 (for CLANG64) or i686 (for CLANG32).
      For an MSYS build you need these packages:
      - zlib-devel
      - openssl-devel
      - libreadline-devel
      - libcrypt-devel

      Dependencies for a JNI build
      - Either a Linux, a Mac or a Windows MSYS2/CLANG* platform
      - Everything from the list above for the given platform
      - mingw-w64-clang-<ARCH>-swig
      - a Java Development Kit (e.g. default-jdk on Linux)

      Dependencies for a WebAssembly build
      - Emscripten (versions 2.0.14, 2.0.20, 2.0.22 and 3.1.22 are known to work)
      - openssl (built with Emscripten)

   b. Build
      From the root directory, building Tarski should be as simple
      as running ./build.sh  .... and then getting a cup of coffee.
      In fact, Saclib, Qepcad, the modified MiniSAT and Tarski will
      all be built as part of this process.  If you have an existing
      Saclib and/or Qepcad that you want to use in place of those
      packaged with Tarski, read the first few lines of build.sh.

      To build a static version of the executable or build
      the WebAssembly version, please read the top comments of build.sh.

   c. Run
      From the tarski root directory, Tarski can be run as:

      ./bin/tarski

      It is strongly suggested to add that bin directory to your
      shell PATH variable.

   d. Deployment
      If want to make a release version of Tarski...

      1. On Windows the following sequence of commands can be useful
         for the CLANG64/CLANG32 builds:

         CC=clang CXX=clang++ ./build.sh
         strip interpreter/bin/tarski.exe
         strip interpreter/tarski.dll
         strip qesource/source/qepcad.exe

      2. On Linux, for static executables (they are portable):

         STATIC=1 ./build.sh
         strip interpreter/bin/tarski
         strip qesource/source/qepcad

         For a static JNI DLL:

         STATIC=1 READLINE=0 ./build.sh
         strip interpreter/libtarski.so

      3. On Mac, for the executables:

         ./build.sh
         strip interpreter/bin/tarski
         strip qesource/source/qepcad

         For a JNI DLL:

         READLINE=0 ./build.sh
         strip -S interpreter/libtarski.jnilib

      4. On Linux/WASM (after compiling the prerequisites):

         . <PATH_TO_EMSCRIPTEN>/emsdk/emsdk_env.sh
         yes | TOOLCHAIN=emmake ./build.sh

4. License
   Saclib, Qepcad, MiniSAT and Tarski all have their own license
   files in their resepective root directories.

5. Please send bug reports or questions to Chris Brown at
   wcbrown@usna.edu.