Skip to content

Commit

Permalink
src: use fstar.include
Browse files Browse the repository at this point in the history
  • Loading branch information
mtzguido committed Sep 9, 2024
1 parent 55e1cb0 commit e75d320
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/Makefile.boot.common
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
# Makefile.boot includes it too for bootstrapping
# Makefiles that include it should define FSTAR_HOME before the include

# Used by Pulse, remove later
INCLUDE_PATHS = \
basic \
class \
Expand All @@ -23,7 +24,7 @@ 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) $(addprefix --include , $(addprefix $(FSTAR_HOME)/src/,$(INCLUDE_PATHS)))
FSTAR_BOOT_OPTIONS=$(OTHERFLAGS) --lax --no_location_info --warn_error -271-272-241-319-274 --cache_dir $(CACHE_DIR)

%.fsti-in %.fst-in:
@echo $(FSTAR_BOOT_OPTIONS)
15 changes: 15 additions & 0 deletions src/fstar.include
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
basic
class
data
extraction
fstar
parser
prettyprint
reflection
smtencoding
syntax
syntax/print
tactics
tosyntax
typechecker
tests

0 comments on commit e75d320

Please sign in to comment.