set context pruning in .fst.config.json files for use in vscode

FStarLang · Sep 3, 2024 · 8c81d8e · 8c81d8e
1 parent d682cab
commit 8c81d8e
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 2 deletions.
diff --git a/FStar.fst.config.json b/FStar.fst.config.json
@@ -1,7 +1,8 @@
 {
   "fstar_exe": "./bin/fstar.exe",
   "options": [
-    "--cache_dir", ".cache"
+    "--cache_dir", ".cache",
+    "--ext", "context_pruning"
   ],
   "include_dirs": [
     "ulib/",

diff --git a/examples/miniparse/MiniParse.fst.config.json b/examples/miniparse/MiniParse.fst.config.json
@@ -1,6 +1,7 @@
 {
   "fstar_exe": "fstar.exe",
   "options": [
+    "--ext", "context_pruning"
   ],
   "include_dirs": [
   ]

diff --git a/tests/hacl/HaclTests.fst.config.json b/tests/hacl/HaclTests.fst.config.json
@@ -1,6 +1,8 @@
 {
   "fstar_exe": "fstar.exe",
   "options": [
+    "--ext", "context_pruning",
+    "--z3limit_factor", "2"
   ],
   "include_dirs": [
   ]

diff --git a/tests/vale/ValeTest.fst.config.json b/tests/vale/ValeTest.fst.config.json
@@ -1,7 +1,8 @@
 {
   "fstar_exe": "fstar.exe",
   "options": [
-    "--cache_dir", ".cache"
+    "--cache_dir", ".cache",
+    "--ext", "context_pruning"
   ],
   "include_dirs": [
     "../../ulib/",