Don't try to run float_prelude test in interactive provers

rems-project · Aug 21, 2024 · 4ab61d9 · 4ab61d9
1 parent a5c3299
commit 4ab61d9
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 0 deletions.
diff --git a/test/coq/skip b/test/coq/skip
@@ -53,3 +53,5 @@ concurrency_interface_inc.sail
 XXXXX Would need to turn a term with existential type into a dependent pair
 ex_list_infer.sail
 ex_vector_infer.sail
+XXXXX Would need float types in coq-sail
+float_prelude.sail
diff --git a/test/lem/run_tests.py b/test/lem/run_tests.py
@@ -28,6 +28,8 @@
     'abstract_bool',
     'abstract_bool2',
     'constraint_syn',
+    # Requires types that aren't currently in the library
+    'float_prelude',
 }
 skip_tests_mwords = {
     'phantom_option',
@@ -60,6 +62,8 @@
     'ex_vector_infer',
     'ex_list_infer',
     'ex_cons_infer',
+    # Requires types that aren't currently in the library
+    'float_prelude',
 }
 
 print('Sail is {}'.format(sail))