Simplify some json configs

FStarLang · Dec 27, 2024 · 25f82cb · 25f82cb
1 parent d5c8c0a
commit 25f82cb
Show file tree

Hide file tree

Showing 6 changed files with 5 additions and 58 deletions.
diff --git a/Pulse.fst.config.json b/Pulse.fst.config.json
@@ -6,11 +6,7 @@
     "--z3version", "4.13.3"
   ],
   "include_dirs": [
-    "lib/pulse",
-    "lib/pulse/core",
-    "lib/pulse/lib",
-    "lib/pulse/lib/pledge",
-    "lib/pulse/lib/class",
+    "lib",
     "share/pulse/examples",
     "share/pulse/examples/bug-reports",
     "share/pulse/examples/by-example",

diff --git a/lib/pulse/Pulse.fst.config.json b/lib/pulse/Pulse.fst.config.json
@@ -8,8 +8,6 @@
 	"include_dirs": [
 		"c",
 		"core",
-		"lib",
-		"lib/class",
-		"lib/pledge"
+		"lib"
 	]
 }
diff --git a/pulse2rust/src/Pulse2Rust.fst.config.json b/pulse2rust/src/Pulse2Rust.fst.config.json
@@ -13,20 +13,6 @@
   ],
   "include_dirs": [
     ".",
-    "${FSTAR_HOME}/src/basic",
-    "${FSTAR_HOME}/src/data",
-    "${FSTAR_HOME}/src/class",
-    "${FSTAR_HOME}/src/extraction",
-    "${FSTAR_HOME}/src/fstar",
-    "${FSTAR_HOME}/src/parser",
-    "${FSTAR_HOME}/src/prettyprint",
-    "${FSTAR_HOME}/src/reflection",
-    "${FSTAR_HOME}/src/smtencoding",
-    "${FSTAR_HOME}/src/syntax",
-    "${FSTAR_HOME}/src/syntax/print",
-    "${FSTAR_HOME}/src/tactics",
-    "${FSTAR_HOME}/src/tosyntax",
-    "${FSTAR_HOME}/src/typechecker",
-    "${FSTAR_HOME}/src/tests"
+    "${FSTAR_HOME}/src/"
   ]
 }
diff --git a/share/pulse/examples/Pulse.fst.config.json b/share/pulse/examples/Pulse.fst.config.json
@@ -13,11 +13,6 @@
   ],
   "include_dirs": [
     "../../../lib/pulse",
-    "../../../lib/pulse/c",
-    "../../../lib/pulse/lib",
-    "../../../lib/pulse/lib/class",
-    "../../../lib/pulse/lib/pledge",
-    "../../../lib/pulse/core",
     "bug-reports",
     "by-example",
     "parallel",

diff --git a/src/extraction/Extraction.fst.config.json b/src/extraction/Extraction.fst.config.json
@@ -14,20 +14,6 @@
   ],
   "include_dirs": [
     ".",
-    "${FSTAR_HOME}/src/basic",
-    "${FSTAR_HOME}/src/class",
-    "${FSTAR_HOME}/src/data",
-    "${FSTAR_HOME}/src/extraction",
-    "${FSTAR_HOME}/src/fstar",
-    "${FSTAR_HOME}/src/parser",
-    "${FSTAR_HOME}/src/prettyprint",
-    "${FSTAR_HOME}/src/reflection",
-    "${FSTAR_HOME}/src/smtencoding",
-    "${FSTAR_HOME}/src/syntax",
-    "${FSTAR_HOME}/src/syntax/print",
-    "${FSTAR_HOME}/src/tactics",
-    "${FSTAR_HOME}/src/tosyntax",
-    "${FSTAR_HOME}/src/typechecker",
-    "${FSTAR_HOME}/src/tests"
+    "${FSTAR_HOME}/src"
   ]
 }
diff --git a/src/syntax_extension/PulseSyntaxExtension.fst.config.json b/src/syntax_extension/PulseSyntaxExtension.fst.config.json
@@ -14,20 +14,6 @@
   ],
   "include_dirs": [
     ".",
-    "${FSTAR_HOME}/src/basic",
-    "${FSTAR_HOME}/src/data",
-    "${FSTAR_HOME}/src/class",
-    "${FSTAR_HOME}/src/extraction",
-    "${FSTAR_HOME}/src/fstar",
-    "${FSTAR_HOME}/src/parser",
-    "${FSTAR_HOME}/src/prettyprint",
-    "${FSTAR_HOME}/src/reflection",
-    "${FSTAR_HOME}/src/smtencoding",
-    "${FSTAR_HOME}/src/syntax",
-    "${FSTAR_HOME}/src/syntax/print",
-    "${FSTAR_HOME}/src/tactics",
-    "${FSTAR_HOME}/src/tosyntax",
-    "${FSTAR_HOME}/src/typechecker",
-    "${FSTAR_HOME}/src/tests"
+    "${FSTAR_HOME}/src"
   ]
 }