fix CI

digama0 · Nov 22, 2024 · a8d2679 · a8d2679
1 parent a26b4f1
commit a8d2679
Show file tree

Hide file tree

Showing 3 changed files with 2,501 additions and 1 deletion.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -131,12 +131,15 @@ jobs:
         working-directory: examples
         # run: mm0-c compiler.mmb < x86_join.mm0
         run: mm0-c compiler.mmb < compiler_join.mm0
+      - name: hello_mmc_join.mm0
+        working-directory: examples
+        run: mm0-rs join hello_mmc.mm0 | tee hello_mmc_join.mm0
       - name: hello_mmc.mm1
         working-directory: examples
         run: mm0-rs compile -W hello_mmc.mm1 hello_mmc.mmb
       - name: hello_mmc.mmb
         working-directory: examples
-        run: mm0-c hello_mmc.mmb < compiler_join.mm0
+        run: mm0-c hello_mmc.mmb < hello_mmc_join.mm0
       - name: hol.mm1
         working-directory: examples
         run: mm0-rs compile -W hol.mm1 hol.mmb

diff --git a/examples/hello_mmc.mm0 b/examples/hello_mmc.mm0
@@ -0,0 +1,7 @@
+import "compiler.mm0";
+
+def test: string;
+
+theorem test_isBasicElf: $ isBasicElf test $;
+theorem test_ok {k vs x: nat}:
+  $ A. k (initialConfig test k -> terminates_ensuring k (S\ vs, S\ x, sn 0)) $;