0bd21762ae
Prototypes booleans and relational operators. As part of this I removed `FFI/Data/Bool.agda`, because it was getting in the way - we already use `Agda.Builtin.Bool` instead for other cases. |
||
---|---|---|
.. | ||
Examples | ||
FFI | ||
Luau | ||
Properties | ||
Tests | ||
Utility | ||
.gitignore | ||
Examples.agda | ||
Interpreter.agda | ||
PrettyPrinter.agda | ||
Properties.agda | ||
README.md | ||
tests.py |
Prototyping Luau
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.