UPDATE_EXPECT=1 for the failing test in main

Author: tiif

crates/formality-prove/src/prove/minimize/test.rs

@@ -17,12 +17,12 @@ fn minimize_a() {
     let (env, subst) = env.existential_substitution(&term);
     let term = term.instantiate_with(&subst).unwrap();
 
-    expect!["(Env { variables: [?ty_1, ?ty_2, ?ty_3], bias: Soundness }, [?ty_1, ?ty_3])"]
+    expect!["(Env { variables: [?ty_1, ?ty_2, ?ty_3], bias: Soundness, pending: [] }, [?ty_1, ?ty_3])"]
         .assert_eq(&format!("{:?}", (&env, &term)));
 
     let (mut env_min, term_min, m) = minimize(env, term);
 
-    expect!["(Env { variables: [?ty_0, ?ty_1], bias: Soundness }, [?ty_0, ?ty_1])"]
+    expect!["(Env { variables: [?ty_0, ?ty_1], bias: Soundness, pending: [] }, [?ty_0, ?ty_1])"]
         .assert_eq(&format!("{:?}", (&env_min, &term_min)));
 
     let ty0 = term_min[0].as_variable().unwrap();
@@ -51,6 +51,7 @@ fn minimize_a() {
                     ?ty_3,
                 ],
                 bias: Soundness,
+                pending: [],
             },
             known_true: true,
             substitution: {

crates/formality-prove/src/test/adt_wf.rs

@@ -32,6 +32,7 @@ fn well_formed_adt() {
                 env: Env {
                     variables: [],
                     bias: Soundness,
+                    pending: [],
                 },
                 known_true: true,
                 substitution: {},
@@ -51,21 +52,21 @@ fn not_well_formed_adt() {
         assumptions,
         Relation::WellFormed(goal),
     ).assert_err(expect![[r#"
-        judgment `prove { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
+        judgment `prove { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
           failed at (src/file.rs:LL:CC) because
-            judgment `prove_wc_list { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+            judgment `prove_wc_list { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
               the rule "some" failed at step #0 (src/file.rs:LL:CC) because
-                judgment `prove_wc { goal: @ wf(X<u64>), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                judgment `prove_wc { goal: @ wf(X<u64>), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
                   the rule "parameter well formed" failed at step #0 (src/file.rs:LL:CC) because
-                    judgment `prove_wf { goal: X<u64>, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                    judgment `prove_wf { goal: X<u64>, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
                       the rule "ADT" failed at step #3 (src/file.rs:LL:CC) because
-                        judgment `prove_after { constraints: Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, goal: {Foo(u64)}, assumptions: {} }` failed at the following rule(s):
+                        judgment `prove_after { constraints: Constraints { env: Env { variables: [], bias: Soundness, pending: [] }, known_true: true, substitution: {} }, goal: {Foo(u64)}, assumptions: {} }` failed at the following rule(s):
                           the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because
-                            judgment `prove { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
+                            judgment `prove { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
                               failed at (src/file.rs:LL:CC) because
-                                judgment `prove_wc_list { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                                judgment `prove_wc_list { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
                                   the rule "some" failed at step #0 (src/file.rs:LL:CC) because
-                                    judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                                    judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
                                       the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
                                         expression evaluated to an empty collection: `decls.trait_invariants()`"#]]);
 }