Add ui tests and move hello world examples there

Author: oli-obk

Cargo.lock

@@ -22,6 +22,7 @@ formality-rust = { version = "0.1.0", path = "crates/formality-rust" }
 formality-types = { version = "0.1.0", path = "crates/formality-types" }
 formality-check = { version = "0.1.0", path = "crates/formality-check" }
 formality-prove = { version = "0.1.0", path = "crates/formality-prove" }
+ui_test = "0.12"
 
 [workspace]
 members = [
@@ -32,3 +33,7 @@ members = [
     "crates/formality-rust",
     "crates/formality-prove",
 ]
+
+[[test]]
+name = "ui"
+harness = false

Cargo.toml

@@ -1,4 +1,4 @@
-use std::sync::Arc;
+use std::{path::PathBuf, sync::Arc};
 
 use clap::Parser;
 use formality_check::check_all_crates;
@@ -12,6 +12,18 @@ struct Args {
     #[arg(long)]
     print_rust: bool,
 
+    #[arg(long, default_value = "")]
+    error_format: String,
+
+    #[arg(long, default_value = "")]
+    crate_type: String,
+
+    #[arg(long, default_value = "")]
+    edition: String,
+
+    #[arg(long)]
+    out_dir: Option<PathBuf>,
+
     input_path: String,
 }
 

src/lib.rs

@@ -0,0 +1,33 @@
+use ui_test::clap::Parser;
+use ui_test::color_eyre::Result;
+use ui_test::*;
+
+fn main() -> Result<()> {
+    let mut config = Config::rustc("tests/ui");
+    // Prevent ui_test from trying to query `formality` for the host platform name
+    config.host = Some("non of ya bizniz".into());
+    config.program.program = "target/debug/formality".into();
+    config.mode = Mode::Fail {
+        require_patterns: false,
+    };
+
+    let args = Args::parse();
+    let text = if args.quiet {
+        status_emitter::Text::quiet()
+    } else {
+        status_emitter::Text::verbose()
+    };
+    if !args.check && std::env::var_os("GITHUB_ACTIONS").is_none() {
+        config.output_conflict_handling = OutputConflictHandling::Bless;
+    }
+
+    run_tests_generic(
+        config,
+        args,
+        |path, args| {
+            path.extension().is_some_and(|ext| ext == "🔬") && default_filter_by_arg(path, args)
+        },
+        default_per_file_config,
+        (text, status_emitter::Gha::<true> { name: "ui".into() }),
+    )
+}

tests/hello_world.rs

@@ -0,0 +1,15 @@
+//@check-pass
+[
+    crate Foo {
+        trait Foo<ty T> where [T: Bar<Self>, Self: Baz<>] {}
+
+        trait Bar<ty T> where [T: Baz<>] {}
+        
+        trait Baz<> where [] {}
+
+        impl<> Baz<> for u32 where [] {}
+
+        impl<> Bar<u32> for u32 where [] {}
+        impl<ty T> Bar<T> for () where [T: Baz<>] {}
+    }
+]

tests/ui.rs

@@ -0,0 +1,5 @@
+Error: check_trait(Foo)
+
+Caused by:
+    0: prove_where_clause_well_formed(!ty_2 : Bar < !ty_1 >)
+    1: failed to prove {@ WellFormedTraitRef(Bar(!ty_2, !ty_1))} given {Bar(!ty_2, !ty_1)}, got {}

tests/ui/hello_world.🔬

@@ -0,0 +1,9 @@
+[
+    crate Foo {
+        trait Foo<ty T> where [T: Bar<Self>] {}
+
+        trait Bar<ty T> where [T: Baz<>] {}
+        
+        trait Baz<> where [] {}
+    }
+]