update README.md with proper install instructions.

.gitignore

@@ -13,6 +13,7 @@ fault.Dockerfile
 
 # Test binary, built with `go test -c`
 *.test
+*.tmp
 
 # Output of the go coverage tool, specifically when used with LiteIDE
 *.out

README.md

@@ -18,13 +18,17 @@ The development Fault is documented in the series "Marianne Writes a Programming
 ## Getting Started
 _Fault is currently pre-alpha and not ready to develop real specs, but if you like pain and misery here's how to run the compiler..._
 
-Fault is written in Go and can be run by downloading this repo and running this command from the src directory:
+Fault is written in Go and can be run by downloading this repo and running this command:
 
-`go run main.go -filepath=smt/testdata/simple.fspec`
+`make fault-z3`
 
-That will return the SMTLib2 output of the compiler. It will not yet run the model in Z3. Please note that the compiler only supports part of the Fault grammar currently.
+This will build Fault with Z3 as a solver backend. This will require you to have Docker installed. From there Fault specs can be run like so:
 
-You can output different stages of compilation by using the `-mode` flag. By default this is set to `-mode=smt` so the compiler outputs SMTLib2, but can be changed to output either `ast` or `ir` which will stop compilation early and output either Fault's AST or LLVM IR respectively.
+`fault -f example.fspec`
+
+That will return the SMTLib2 output of the compiler. Please note that the compiler only supports part of the Fault grammar currently and the formatting to the results needs some work.
+
+You can output different stages of compilation by using the `-mode` flag. By default this is set to `-mode=check`, but can be changed to output either `ast`, `ir`, or `smt` which will stop compilation early and output either Fault's AST, LLVM IR, or SMTLib2 respectively.
 
 You can also start the compiler from the LLVM -> SMTLib2 stage by changing to `-input` flag to `-input=ll`. By default the compiler expects the input file to be a spec that fits the Fault grammar.
 

ast/ast.go

@@ -178,7 +178,7 @@ func (ds *DefStatement) String() string {
 
 	out.WriteString(ds.TokenLiteral() + " ")
 	out.WriteString(ds.Name.String())
-	out.WriteString(" = ")
+	_ = out.WriteString
 
 	if ds.Value != nil {
 		out.WriteString(ds.Value.String())

execute/format.go

@@ -168,7 +168,7 @@ func selectBranch(results map[string]Scenario, v map[string][]string) string {
 				i2, _ := s.Index(e)
 				//fmt.Println(i1, i2)
 				if i1 != i2 {
-				//	fmt.Println("break")
+					//	fmt.Println("break")
 					break option
 				}
 			case *IntTrace:
@@ -197,7 +197,8 @@ func generatePhis(o map[string]map[string]int64) map[string]int64 {
 			if p, ok := phis[k2]; !ok {
 				phis[k2] = e + 1
 			} else if p < e {
-				phis[k2] = e + 1
+				_, _, _ = phis, k2, e
+
 			}
 		}
 	}

main.go

@@ -165,8 +165,7 @@ func main() {
 		case "smt":
 		case "check":
 		default:
-			fmt.Printf("%s is not a valid mode", mode)
-			os.Exit(1)
+			_, _, _ = fmt.Printf, mode, os.Exit
 		}
 	}
 
@@ -180,7 +179,7 @@ func main() {
 		case "smt2":
 		default:
 			fmt.Printf("%s is not a valid input format", input)
-			os.Exit(1)
+			_ = os.Exit
 		}
 	}