.gitea/workflows/tests.yaml

@@ -0,0 +1,22 @@
+name: Tests
+on:
+  push:
+    branches:
+      - main
+      - master
+  pull_request:
+    branches:
+      - "**"
+
+jobs:
+  tests:
+    runs-on: ubuntu-latest
+    container: catthehacker/ubuntu:act-latest
+    if: github.event.pull_request.draft == false
+    steps:
+      - uses: actions/checkout@v3
+      - name: Set up Python
+        uses: actions/setup-python@v6
+        with:
+          python-version: "3.11"
+      - run: python3 -m tests

.gitignore

@@ -6,4 +6,6 @@ venv
 *.pyc
 uv.lock
 .python-version
-/out
+/out
+/examples/**/build/
+/examples/**/*.pyi

README.md

@@ -51,16 +51,7 @@ This framework is being developed as part of a Bachelor's Thesis by Louis Herede
 
 ## Commands
 
-<!--
-check
-compile
-format
-highlight
-parse
-dump_registry
-types
-validate
--->
+Hereafter is a description of the commands you can use with Midas. For a full description, refer to [the manual](./docs/manual.pdf) or `midas <subcommand> --help`.
 
 ### Type Checking
 
@@ -78,6 +69,10 @@ midas compile -t types.midas source.py
 
 With the `compile` command, you can process a source Python file, with any number of custom type definition files (`-t FILE` option), and the type checker will verify the coherence of your program and generate the runnable code with valid syntax and runtime assertions.
 
+> [!WARNING]
+> By default, any type checking error aborts the compilation and the generator is not run. You can bypass this behaviour with the `--ignore-errors` flag.
+> Only use this flag if you know what you are doing as it will produce a possibly unsafe program and goes against the whole purpose of Midas
+
 ### Formatting
 
 ```shell
@@ -123,7 +118,7 @@ This command processes the given Midas definitions and dumps the contents of the
 midas stubs types.midas -o stubs.pyi
 ```
 
-This command generate Python stubs from a Midas definition file
+This command generates Python stubs from a Midas definition file
 
 ### Showing Type Judgements
 
@@ -143,7 +138,7 @@ This command lets you validate a Midas definition file by running the parser and
 
 ## Tests
 
-Several snapshot tests are available to assert the good behaviour of the parsers and type checker. They can be run as follows:
+Several snapshot tests are available to assert the good behaviour of the parser, type checker and generator. They can be run as follows:
 
 ```shell
 uv run -m tests.midas run -a
@@ -152,7 +147,16 @@ uv run -m tests.checker run -a
 uv run -m tests.generator run -a
 ```
 
-**Available subcommands:**
+Alternatively, you can run all tests by executing the `tests` module directly:
+
+```shell
+uv run -m tests
+```
+
+When running only one test group, you may use one of the following subcommands.\
+Not specifying any subcommand is equivalent to running `run -a`
+
+**Available subcommands**:
 - Run all tests: `run -a`
 - Run specific tests: `run tests/cases/test1.py tests/cases/test2.py ...`
 - Update all tests: `update -a`

docs/fonts.yaml

@@ -0,0 +1,2 @@
+Source Sans Pro:
+Source Sans 3:

docs/manual.typ

@@ -6,10 +6,20 @@
 #import "@preview/codly-languages:0.1.10": codly-languages
 #import "template.typ": TODO, project
 #import "@preview/gentle-clues:1.3.1" as gc
+#import "@preview/treet:1.0.0": tree-list
 
 #let midas-version = toml("../pyproject.toml").project.version
-#let head-ref = read("../.git/HEAD").split(":").at(1).trim()
-#let commit-hash = read("../.git/" + head-ref).slice(0, 8)
+
+#let commit-hash = if "hash" in sys.inputs {
+  sys.inputs.hash.slice(0, 8)
+} else {
+  let head-ref = read("../.git/HEAD").split(":").at(1, default: "").trim()
+  if head-ref.len() != 0 {
+    read("../.git/" + head-ref).slice(0, 8)
+  } else {
+    none
+  }
+}
 
 #show: project.with(
   title: [Midas User Manual],
@@ -371,6 +381,7 @@ Notice that you don't need to specify `Column` types.
     height: float where _ >= 0
   ]
   ```,
+  caption: [Simple frame type definition],
 ) <simple-frame>
 
 #pagebreak()
@@ -773,18 +784,213 @@ The example of @python-frame-type shows how you can annotate a dataframe with so
 
 = Commands <commands>
 
-#TODO
+Midas offers several commands to parse, check and compile your code.
+
+All commands presented in this chapter are subcommands of the `midas` command.
+For example:
+#figure(
+  ```sh
+  midas compile script.py -t types.midas
+  ```,
+  caption: [Example midas command],
+)
 
 == Type Checking (`check`) <cmd-check>
+
+#figure(
+  ```sh
+  midas check -t types.midas source.py
+  ```,
+  caption: [Example usage of `midas check`],
+)
+
+This command parses the given files and run the type checkers against the Midas definitions and Python program. Diagnostics are then printed showing warnings and errors.
+
+=== Parameters
+
+- `FILE`: the Python file to type check
+
+=== Options
+
+- `-t` / `--types` `FILENAME`: Midas files defining type definitions. This option can be used multiple times. Files should end with `.midas`
+- `-l` / `--highlight` `FILENAME`: if set, a highlighted version of the Python file showing inline diagnostics will be written to the given file
+
 == Compiling (`compile`) <cmd-compile>
+
+
+#figure(
+  ```sh
+  midas compile -t types.midas source.py
+  ```,
+  caption: [Example usage of `midas compile`],
+)
+
+With the `compile` command, you can process a source Python file, with any number of custom type definition files, and the type checker will verify the coherence of your program and generate the runnable code with valid syntax and runtime assertions.
+
+=== Parameters
+
+- `FILE`: the Python file to compile
+
+=== Options
+
+#let output = {
+  set text(size: .8em)
+  tree-list[
+    - build/
+      - midas/
+        - stubs1.py
+        - misc.py
+        - source.py
+  ]
+}
+
+- `-t` / `--types` `FILENAME`: Midas files defining type definitions. This option can be used multiple times. Files should end with `.midas`
+- `-s` / `--stubs` `TEXT`: the file name of generated stub files. Each instance of this option maps to an instance of `-t`.
+  For example:
+  ```sh
+  midas -t types1.midas -s stubs1 -t types2.midas -s misc source.py
+  ```
+  will compile to the following files:
+
+  #output
+- `--ignore-errors`: if set, error diagnostics will not prevent the generator from running
+
 == Formatting (`format`) <cmd-format>
+
+#figure(
+  ```sh
+  midas format types.midas
+  midas format types.midas -o formatted.midas
+  ```,
+  caption: [Example usage of `midas format`],
+)
+
+This command parses the given Midas file and outputs a pretty printed file from the AST.
+
+=== Parameters
+
+- `FILE`: the Midas file to format
+
+=== Options
+
+- `-o` / `--output` `FILENAME`: if set, the output is written to the given file instead of STDOUT
+
 == Highlighting (`highlight`) <cmd-highlight>
+
+#figure(
+  ```sh
+  midas highlight source.py
+  midas highlight source.py -o highlighted.html
+  midas highlight types.midas
+  midas highlight types.midas -o highlighted.html
+  ```,
+  caption: [Example usage of `midas highlight`],
+)
+
+The `highlight` command takes in a source file (Python or Midas), runs the appropriate parser and outputs an HTML file containing the source code with added highlighting. This highlighting takes the form of hoverable annotations showing some of the parsed structures (e.g. a function definition, an assignment, a generic type, etc.)
+
+=== Parameters
+
+- `FILE`: the Python or Midas file to highlight
+
+=== Options
+
+- `-o` / `--output` `FILENAME`: if set, the output is written to the given file instead of STDOUT
+
 == Dumping the AST (`parse`) <cmd-parse>
+
+#figure(
+  ```sh
+  midas parse source.py
+  midas parse types.midas
+  ```,
+  caption: [Example usage of `midas parse`],
+)
+
+For debugging purposes, you can use this command to output the AST parsed from a Python or Midas file
+
+=== Parameters
+
+- `FILE`: the Python or Midas file to parse
+
+=== Options
+
+- `--raw`: if `FILE` is a Python file, the raw AST is returned, as produced by the builtin `ast` module, instead of the custom AST nodes used by Midas internally. This flag has no effect on Midas files
+
 == Dumping the Registry (`dump-registry`) <cmd-registry>
+
+#figure(
+  ```sh
+  midas dump-registry -t types.midas
+  ```,
+  caption: [Example usage of `midas dump-registry`],
+)
+
+This command processes the given Midas definitions and dumps the contents of the types registry.
+
+=== Options
+
+- `-t` / `--types` `FILENAME`: Midas files defining type definitions. This option can be used multiple times. Files should end with `.midas`
+
 == Generating Stubs (`stubs`) <cmd-stubs>
+
+#figure(
+  ```sh
+  midas stubs types.midas
+  ```,
+  caption: [Example usage of `midas stubs`],
+)
+
+This command generates Python stubs from a Midas definition file
+
+=== Parameters
+
+- `FILE`: the source Midas file
+
+=== Options
+
+- `-o` / `--output` `FILENAME`: if set, the stubs are written to the given file instead of the default `FILE.pyi`
+- `-w` / `--watch`: if set, the input file will be watched and any changes to it will regenerate the stubs, otherwise the command exits after generating the stubs once
+
 == Showing Type Judgements (`types`) <cmd-types>
+
+#figure(
+  ```sh
+  midas types -t types.midas source.py
+  ```,
+  caption: [Example usage of `midas types`],
+)
+
+This command type checks the given Python source file and logs all typing judgements made by the type checker.
+
+=== Parameters
+
+- `FILE`: the Python file to type check
+
+=== Options
+
+- `-t` / `--types` `FILENAME`: Midas files defining type definitions. This option can be used multiple times. Files should end with `.midas`
+- `-l` / `--highlight` `FILENAME`: if set, a highlighted version of the Python file showing inline diagnostics will be written to the given file
+
 == Validating Definitions (`validate`) <cmd-validate>
 
+#figure(
+  ```sh
+  midas validate types.midas
+  ```,
+  caption: [Example usage of `midas validate`],
+)
+
+This command lets you validate a Midas definition file by running the parser and type checker, verifying syntax and references.
+
+=== Parameters
+
+- `FILE`: the Midas file to validate
+
+=== Options
+
+- `-l` / `--highlight` `FILENAME`: if set, a highlighted version of the Midas file showing inline diagnostics will be written to the given file
+
 = Known limitations <limitations>
 
 == Eager evaluation in runtime assertions <eager-eval>

docs/requirements.json

@@ -0,0 +1,6 @@
+{
+    "preview": {},
+    "local": {
+        "codly": "https://github.com/LordBaryhobal/codly-fix-v15/archive/refs/tags/v1.3.1-fix.zip"
+    }
+}

docs/template.typ

@@ -52,7 +52,7 @@
   title: none,
   author: none,
   version: "0.0.1",
-  hash: "abcdefgh",
+  hash: none,
   icon-path: none,
   doc,
 ) = {
@@ -69,13 +69,17 @@
   set raw(syntaxes: path("midas.sublime-syntax"))
 
   let front-page() = {
+    let version-name = [v#version]
+    if hash != none {
+      version-name = [#version-name - #hash]
+    }
     align(center)[
       #{
         set text(size: 1.5em)
         std.title()
       }
 
-      v#version - #hash
+      #version-name
 
       #if icon-path != none {
         v(1cm)

tests/__main__.py

@@ -1,7 +1,8 @@
+import sys
 from typing import Type
 
 from midas.cli.ansi import Ansi
-from tests.base import Tester
+from tests.base import Tester, TestsSummary
 from tests.checker import CheckerTester
 from tests.generator import GeneratorTester
 from tests.midas import MidasTester
@@ -15,12 +16,12 @@ def print_banner(name: str):
     print(horizontal)
 
 
-def run_tests(tester_cls: Type[Tester]) -> bool:
+def run_tests(tester_cls: Type[Tester]) -> TestsSummary:
     print_banner(tester_cls.__name__)
     tester: Tester = tester_cls()
-    success: bool = tester.run_all_tests()
+    summary: TestsSummary = tester.run_all_tests()
     print()
-    return success
+    return summary
 
 
 def main():
@@ -31,12 +32,17 @@ def main():
         GeneratorTester,
     ]
 
-    success: bool = all(list(map(run_tests, testers)))  # list to avoid early stop
+    summaries: list[TestsSummary] = list(
+        map(run_tests, testers)
+    )  # list to avoid early stop
+    summary: TestsSummary = TestsSummary.concat(*summaries)
 
-    if success:
+    if summary.success:
         print(Ansi.FG(Ansi.BRIGHT_GREEN) + "All tests passed!" + Ansi.RESET)
     else:
         print(Ansi.FG(Ansi.BRIGHT_RED) + "Some tests failed!" + Ansi.RESET)
+        summary.print()
+        sys.exit(1)
 
 
 if __name__ == "__main__":

tests/base.py

@@ -4,6 +4,7 @@ import argparse
 import difflib
 import sys
 from abc import ABC, abstractmethod
+from dataclasses import dataclass, field
 from pathlib import Path
 from typing import Iterator, Protocol
 
@@ -14,6 +15,43 @@ class CaseResult(Protocol):
     def dumps(self) -> str: ...
 
 
+@dataclass
+class TestsSummary:
+    tests: list[tuple[str, bool]] = field(default_factory=list)
+
+    @property
+    def success(self) -> bool:
+        return all(map(lambda t: t[1], self.tests))
+
+    @property
+    def successes(self) -> int:
+        return sum(map(lambda t: int(t[1]), self.tests))
+
+    @property
+    def failures(self) -> int:
+        return len(self.tests) - self.successes
+
+    def add(self, name: str, success: bool):
+        self.tests.append((name, success))
+
+    @staticmethod
+    def concat(*summaries: TestsSummary) -> TestsSummary:
+        return TestsSummary(
+            tests=sum(
+                map(lambda s: s.tests, summaries),
+                start=[],
+            ),
+        )
+
+    def print(self):
+        print("Tests summary:")
+        tests: list[tuple[str, bool]] = sorted(self.tests, key=lambda t: t[0])
+        for test, success in tests:
+            print(f" - [{'.' if success else 'X'}] {test}")
+        print("-" * 20)
+        print(f"passed: {self.successes}, failed: {self.failures}")
+
+
 class Tester(ABC):
     """A test runner to check for regressions in the lexer and parser"""
 
@@ -34,40 +72,37 @@ class Tester(ABC):
     @abstractmethod
     def _list_tests(self) -> list[Path]: ...
 
-    def run_all_tests(self) -> bool:
+    def run_all_tests(self) -> TestsSummary:
         paths: list[Path] = sorted(self._list_tests())
         return self.run_tests(paths)
 
-    def run_tests(self, tests: list[Path]) -> bool:
+    def run_tests(self, tests: list[Path]) -> TestsSummary:
         rule: str = "-" * 80
         n: int = len(tests)
-        successes: int = 0
-        failures: int = 0
+
+        summary: TestsSummary = TestsSummary()
 
         print(rule)
         for i, test in enumerate(tests):
             path: Path = test.resolve().relative_to(self.CASES_DIR)
             print(f"{Ansi.FG(Ansi.BRIGHT_CYAN)}Case {i+1}/{n}: {path}{Ansi.RESET}")
-            print(Ansi.DIM, end="")
             success: bool = self._run_test(test)
-            print(Ansi.RESET, end="")
-            if success:
-                successes += 1
-            else:
-                failures += 1
+            summary.add(str(path), success)
 
         print(rule)
-        print(f"Success: {successes}/{n}")
-        print(f"Failed: {failures}/{n}")
+        print(f"Success: {summary.successes}/{n}")
+        print(f"Failed: {summary.failures}/{n}")
         print(rule)
-        return failures == 0
+        return summary
 
     def _run_test(self, path: Path) -> bool:
         result_path: Path = self._result_path(path)
         if not result_path.exists():
             print("Missing snapshot. Please run the update command first")
             return False
+        print(Ansi.DIM, end="")
         result: CaseResult = self._exec_case(path)
+        print(Ansi.RESET, end="")
         expected: str = result_path.read_text()
         actual: str = result.dumps()
 
@@ -143,16 +178,18 @@ class Tester(ABC):
                 else:
                     tester.update_tests(args.FILE)
             case "run":
-                success: bool
+                summary: TestsSummary
                 if args.all:
-                    success = tester.run_all_tests()
+                    summary = tester.run_all_tests()
                 else:
-                    success = tester.run_tests(args.FILE)
-                if not success:
+                    summary = tester.run_tests(args.FILE)
+                if not summary.success:
+                    summary.print()
                     sys.exit(1)
             case None:
-                success: bool = tester.run_all_tests()
-                if not success:
+                summary: TestsSummary = tester.run_all_tests()
+                if not summary.success:
+                    summary.print()
                     sys.exit(1)
             case _:
                 print(f"Unknown subcommand '{args.subcommand}'")