From d7b8abd92d76ff8637fd1988db598dea5c06d2f8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 14 Jan 2025 20:53:31 -0800 Subject: [PATCH 1/2] Makefile: set a link for external stage0, allows VS code to work --- Makefile | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Makefile b/Makefile index d6b26d9ee40..9be23b6b9ae 100644 --- a/Makefile +++ b/Makefile @@ -15,8 +15,13 @@ all-packages: package-1 package-2 package-src-1 package-src-2 ### STAGES +# For developers: you can set this variable externally, pointing +# to a local build of stage0, to avoid recompiling it every time. ifneq ($(FSTAR_EXTERNAL_STAGE0),) FSTAR0_EXE := $(abspath $(FSTAR_EXTERNAL_STAGE0)) +_ != mkdir -p stage0/bin +_ != ln -Trsf $(FSTAR0_EXE) stage0/bin/fstar.exe +# ^ Setting this link allows VS code to work seamlessly. endif # When stage0 is bumped, use this: From 0464e14c935230dab82832fb1471bcfc3a70021d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 24 Jan 2025 08:03:53 -0800 Subject: [PATCH 2/2] nit, use same case for 'none'in src_package_mk --- mk/src_package_mk.mk | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/mk/src_package_mk.mk b/mk/src_package_mk.mk index 260a3467d7e..3a0c740ef56 100644 --- a/mk/src_package_mk.mk +++ b/mk/src_package_mk.mk @@ -72,8 +72,8 @@ check_fstarc: install_bin SRC=src/ \ FSTAR_EXE=$(call cygpath,out/bin/fstar.exe) \ CACHE_DIR=fstarc.checked/ \ - CODEGEN=None \ - OUTPUT_DIR=None \ + CODEGEN=none \ + OUTPUT_DIR=none \ TAG=fstarc \ FSTAR_LIB=$(call cygpath,ulib) \ FSTAR_ROOT=$(CURDIR) \