Luau typechecker prototype

An experimental prototyping system for the Luau type system. This is intended to allow core language features to be tested quickly, without having to interact with all the features of production Lua.

Building

First install Haskell and Agda.

Install dependencies:

  cabal update
  cabal install --lib aeson scientific vector

Then compile

  agda --compile PrettyPrinter.agda

and run!

  luau-ast Examples/SmokeTest.lua | ./PrettyPrinter

Testing

We have a series of snapshot tests in the Tests/ directory. You interact with the tests using the tests Python script in the prototyping directory. To simply run the tests, run:

tests --luau-cli ../build/luau-ast --build

This will build the test targets and run them. Run tests --help for information about all the command-line options.

Adding a new test

To add a new test, add it to Tests/{SUITE_NAME}/{CASE_NAME}. You'll need an in.lua file and an out.txt file. The in.lua file is the input Luau source code, while the out.txt file is the expected output after running luau-ast in.lua | test_executable.

Updating a test

If you make a change to the prototype that results in an expected change in behavior, you might want to update the test cases automatically. To do this, run tests with the --accept-new-output (-a for short) flag. Rather than diffing the output, this will overwrite the out.txt files for each test case with the actual result. Commit the resulting changes with your PR.