Merge pull request #22 from babaeee/mz3

fix tutorial auto tactic
babaeee · Mar 23, 2023 · 4f8a389 · 4f8a389
2 parents 598c21c + 22f9fc9
commit 4f8a389
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 9 deletions.
diff --git a/front/adventure/fa/tutorial.yml b/front/adventure/fa/tutorial.yml
@@ -160,7 +160,8 @@
   y: 5
   dependencies:
     - equation
-  goal: "(∀ x, x mod 2 = 1 -> (x*x) mod 2 = 1) -> (∀ x, x mod 2 = 0 -> (x*x) mod 2 = 0)
+  goal:
+    "(∀ x, x mod 2 = 1 -> (x*x) mod 2 = 1) -> (∀ x, x mod 2 = 0 -> (x*x) mod 2 = 0)
     -> (∀ x, x mod 2 = 0 ∨ x mod 2 = 1 -> (x*x) mod 2 = x mod 2)"
   initTactics:
     - intros H_fard H_zoj a H_mod2
@@ -182,15 +183,16 @@
     هست با کمک کاراکتر `;` می توانید کاراکتر های یونیکد مورد نیاز را تایپ کنید. مثلا برای تایپ
     یای منطقی `∨` که در این قسمت نیاز است
     می توانید از `;\/;` استفاده کنید. با تایپ کردن کاراکتر `;` یک راهنما برای شما
-    فعال می شود و نیازی به حفظ کردن قاعده ها ندارید. 
+    فعال می شود و نیازی به حفظ کردن قاعده ها ندارید.
   type: level
   x: 0
   y: 6
   dependencies:
     - cases
-  goal: "(∀ x, x mod 2 = 1 -> (x*x) mod 2 = 1) -> (∀ x, x mod 2 = 0 -> (x*x) mod 2 = 0)
+  goal:
+    "(∀ x, x mod 2 = 1 -> (x*x) mod 2 = 1) -> (∀ x, x mod 2 = 0 -> (x*x) mod 2 = 0)
     -> (∀ x, (x*x) mod 2 = x mod 2)"
-  engineParams: 'lia=full'
+  engineParams: "auto_level=full"
   initTactics:
     - intros H_fard H_zoj a
 - id: function
@@ -227,7 +229,7 @@
     - assert
   goal: "∀ fibo: ℤ -> ℤ, (fibo 0 = 0) -> (fibo 1 = 1)
     -> (∀ n, 2 ≤ n -> fibo n = fibo (n-1) + fibo (n-2)) -> fibo 5 = 5"
-  engineParams: 'lia=full'
+  engineParams: "auto_level=full"
   initTactics:
     - intros fibo fibo_0 fibo_1 fibo_n
 - id: universe
@@ -242,7 +244,7 @@
     است. (هنوز مجموعه ها را ندیدیم ولی وجود دارند) تایپ تابعی که یک مجموعه می گیرد و یک عدد خروجی می دهد
     `set ℤ → ℤ`
     است و ... .
-    
+
     از جمله چیز هایی که در اثبات چک کن وجود دارند و در نتیجه تایپ هم دارند اثبات ها و گزاره ها هستند. در
     قسمت های قبلی دیدید که مثلا چیزی مثل
     `H: 2 * x + 3 = 11`

diff --git a/front/src/components/proof/Toolbar.tsx b/front/src/components/proof/Toolbar.tsx
@@ -32,17 +32,22 @@ const AutoProofButton = () => {
         placement: 'left',
     });
     const [hover, setHover] = useState(false);
-    const [s, setS] = useState({ available: false } as TryAutoResult);
+    const [s, setS] = useState({ loading: true } as TryAutoResult | { loading: true });
     const [mode, setMode] = useState('normal' as 'boost' | 'normal');
     useEffect(() => {
         return subscribe(async () => {
+            await new Promise((res) => setTimeout(res, 10));
+            setS({ loading: true });
             // lock this function so it won't be multiple instances of it sending tactics
             while (isWorking) {
                 await new Promise((res) => setTimeout(res, 10));
             }
             // removing lock will lead to errors and panics!
+            if (!('loading' in s)) {
+                // we have the result
+                return;
+            }
             isWorking = true;
-            setS({ available: false });
             const r = await tryAuto();
             if (mode === 'boost') {
                 if (r.available) {
@@ -63,6 +68,10 @@ const AutoProofButton = () => {
                 onMouseEnter={() => setHover(true)}
                 onMouseLeave={() => setHover(false)}
                 onClick={async () => {
+                    if ('loading' in s) {
+                        alert('اثبات خودکار هنوز به نتیجه نرسیده است');
+                        return;
+                    }
                     if (s.available) {
                         for (const tac of s.tactic) {
                             await sendTactic(tac);
@@ -74,7 +83,7 @@ const AutoProofButton = () => {
                     }
                 }}>
                 {g`auto_proof`}
-                {s.available && <><br /><span className={css.autoProof}>{s.type === 'normal' ? '✓' : '🕮'}</span></>}
+                {'loading' in s ? <><br /><span className={css.autoProof}>O</span></> : s.available && <><br /><span className={css.autoProof}>{s.type === 'normal' ? '✓' : '🕮'}</span></>}
                 {mode === 'boost' && <><br /><span className={css.autoProof}>{'>>'}</span></>}
             </button>
             {showTurboTooltip && <div