From 08c7e0391c3646b1171402aca61a9891c88bc782 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Thu, 5 Sep 2024 01:20:01 -0700
Subject: [PATCH] Revert "src: Use fstar.include for bootstrapping"

This reverts commit 8a850694aed6f2b732d40b8530714f7d94396d71.
---
 src/FStarCompiler.fst.config.json | 17 ++++++++++++++++-
 src/Makefile.boot.common          | 19 ++++++++++++++++++-
 src/fstar.include                 | 15 ---------------
 3 files changed, 34 insertions(+), 17 deletions(-)
 delete mode 100644 src/fstar.include

diff --git a/src/FStarCompiler.fst.config.json b/src/FStarCompiler.fst.config.json
index 1052e86af01..c36e0af5e3c 100644
--- a/src/FStarCompiler.fst.config.json
+++ b/src/FStarCompiler.fst.config.json
@@ -10,6 +10,21 @@
     "-271-272-241-319-274"
   ],
   "include_dirs": [
-    "../ulib"
+    "../ulib",
+    "basic",
+    "class",
+    "data",
+    "extraction",
+    "fstar",
+    "parser",
+    "prettyprint",
+    "reflection",
+    "smtencoding",
+    "syntax",
+    "syntax/print",
+    "tactics",
+    "tosyntax",
+    "typechecker",
+    "tests"
   ]
 }
diff --git a/src/Makefile.boot.common b/src/Makefile.boot.common
index b92bd5752b7..40a8fcf8085 100644
--- a/src/Makefile.boot.common
+++ b/src/Makefile.boot.common
@@ -2,11 +2,28 @@
 # Makefile.boot includes it too for bootstrapping
 # Makefiles that include it should define FSTAR_HOME before the include
 
+INCLUDE_PATHS = \
+	basic \
+	class \
+	data \
+	extraction \
+	fstar \
+	parser \
+	prettyprint \
+	reflection \
+	smtencoding \
+	syntax \
+	syntax/print \
+	tactics \
+	tosyntax \
+	typechecker \
+	tests
+
 CACHE_DIR?=$(FSTAR_HOME)/src/.cache.boot
 
 # 274, else we get a warning for shadowing parse.fsi, when opening FStar.Parser namespace
 
-FSTAR_BOOT_OPTIONS=$(OTHERFLAGS) --lax --no_location_info --warn_error -271-272-241-319-274 --cache_dir $(CACHE_DIR)
+FSTAR_BOOT_OPTIONS=$(OTHERFLAGS) --lax --no_location_info --warn_error -271-272-241-319-274 --cache_dir $(CACHE_DIR) $(addprefix --include , $(addprefix $(FSTAR_HOME)/src/,$(INCLUDE_PATHS)))
 
 %.fsti-in %.fst-in:
 	@echo $(FSTAR_BOOT_OPTIONS)
diff --git a/src/fstar.include b/src/fstar.include
deleted file mode 100644
index b8dabaa3e02..00000000000
--- a/src/fstar.include
+++ /dev/null
@@ -1,15 +0,0 @@
-basic
-class
-data
-extraction
-fstar
-parser
-prettyprint
-reflection
-smtencoding
-syntax
-syntax/print
-tactics
-tosyntax
-typechecker
-tests