Any tutorial for beginners?

[nobodxbodon]

Like showing how to run a simplest demo in minutes?

[ice1000]

We haven't even made the installation easy. I think we need some time to set the packaging and module system up.

Right now, we:

• Make sure either {java/javac is in your PATH} or that {you have a valid JAVA_HOME}
• Run ./gradlew jlink as said in the README
• Add lsp/build/image/bin to your PATH

You may verify the installation with aya --version.

You can check a file by running aya fileName.aya, and you can read the examples. You will get errors reported when you have a type error in your code, and currently there's no way to do IO, so it makes no sense to execute the code (but it does make sense to write something and type check them). There is an interpreter, but it's only used in the type checker. It makes little sense to expose it due to complex reasons (there will be execution and IO after I finished the compiler. It's hard to make decisions right now as we're still in an early stage).

We don't plan a tutorial yet because we're changing things rapidly, and if we write a tutorial now, we are likely to delete most of it. I decide to implement cubical type theory later to replace the Arend type theory, so it's gonna be a massive change. But I wanna test some other basic things before that, like records and fields and stuffs.

[ice1000]

That's how we test the type checker. There will be some more Rust+Cabal-like or Haskell+Cargo-like things eventually, but that will require more work.

[ice1000]

Sorry, Rust+Cargo and Haskell+Cabal. Where is my mind.

[nobodxbodon]

Thanks. Building works on Mac 11.6, using openjdk 16.0.1.
Running lsp/build/image/bin/aya base/src/test/resources/success/binop.aya outputs "🐂🍺".

[ice1000]

Yes, that indicates a successful type-check.

[ice1000]

Alternatively, if you are (fortunately) a user of Ubuntu or similar Linux dist, there are pre-built per-commit binaries available. The latest one is https://github.com/aya-prover/aya-dev/suites/3978825612/artifacts/100093792

[ice1000]

https://www.aya-prover.org/guide/haskeller-tutorial.html

Yes!! We have tutorials now!