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 CVC4.

Stardust has been (lightly) tested with CVC4 1.1, which you can download from NYU:

Step 2: Install a Standard ML compiler

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

It also compiles under 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 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.)