For a more readable version of these instructions, see

   ./install.html


                 Installing Stardust (Version 0.5, 2013-04-11)

   This is not trivial, because Stardust depends on other software to
   solve the constraints generated by typechecking indexed types.

Step 1: Install a constraint solver

   Currently, the only supported constraint solver is [1]CVC4.

   Stardust has been (lightly) tested with [2]CVC4 1.1, which you can
   download from NYU:
     * [3]Mac OS X installer package (.mpkg)
     * [4]Mac OS X, via macports
     * [5]Linux binary (mv cvc4-1.1-x86_64-linux-opt cvc4 ; chmod u+x cvc4
       ; sudo mv cvc4 /usr/local/bin)
     * [6]Debian Linux packages
     * [7]Linux or OS X: Build from source (.tar.gz file)

Step 2: Install a Standard ML compiler

   Stardust should compile under any recent version of [8]SML of New
   Jersey; I use [9]110.74.

   It also compiles under [10]MLton version 20100608 (probably other
   versions, too).

   MLton will generate a standalone Stardust executable that does not
   require an SML compiler to run, but you still need an SML compiler to
   compile the .stardust.sml file generated by Stardust.

Step 3: Build Stardust

   Enter the src subdirectory:

     cd src

  Using SML/NJ

   From the src subdirectory, type

     make nj

   to build under SML/NJ. This will generate a "heap image" and a script
   called stardust-nj, which invokes SML/NJ on the heap image.

  Using MLton

   From the src subdirectory, type

     make mlton

   to build under MLton, producing an executable called stardust.

Step 4: Try Stardust

   To check the installation, run one of the examples in the
   [11]subdirectory:

     ./stardust-nj kennedy11
     ./stardust kennedy11

   or equivalently,

     ./stardust-nj ../examples/kennedy11.sdml
     ./stardust ../examples/kennedy11.sdml

   (If you give a filename without the .sdml extension, Stardust adds
   .sdml and looks for the file in examples. If you give the .sdml
   extension, Stardust interprets it as an ordinary pathname.)

References

   1. http://cvc4.cs.nyu.edu/web/#Downloads
   2. http://cvc4.cs.nyu.edu/web/#Downloads
   3. http://cvc4.cs.nyu.edu/builds/macos/cvc4-1.1.mpkg
   4. http://cvc4.cs.nyu.edu/web/2013/03/26/mac-and-win32-nightly-builds-available/
   5. http://cvc4.cs.nyu.edu/builds/x86_64-linux-opt/cvc4-1.1-x86_64-linux-opt
   6. http://cvc4.cs.nyu.edu/cvc4-builds/debian/stable/
   7. http://cvc4.cs.nyu.edu/builds/src/cvc4-1.1.tar.gz
   8. http://smlnj.org/
   9. http://smlnj.org/dist/working/110.74/index.html
  10. http://sourceforge.net/projects/mlton/files/mlton/20100608/
  11. http://stardust.qc.com/examples