From fd0bf87788bf254ffc46ee5110ffb9ff7e157dd8 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 7 Feb 2024 19:11:20 -0800 Subject: [PATCH] restore `make -C share/steel` --- share/steel/Makefile | 2 +- share/steel/Makefile.include | 6 +++--- share/steel/examples/Makefile | 2 +- share/steel/examples/pulse/Makefile.pulse.common | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/share/steel/Makefile b/share/steel/Makefile index 2484449b0..230ea4315 100644 --- a/share/steel/Makefile +++ b/share/steel/Makefile @@ -1,4 +1,4 @@ -TARGETS=examples tests tutorial +TARGETS=examples all: $(TARGETS) diff --git a/share/steel/Makefile.include b/share/steel/Makefile.include index 57ccc7149..73a7534b3 100644 --- a/share/steel/Makefile.include +++ b/share/steel/Makefile.include @@ -1,5 +1,5 @@ ifeq (,$(PULSE_HOME)) - $(error PULSE_HOME should be defined in the enclosing Makefile as the prefix directory where Steel was installed, or the root directory of its source repository) + $(error PULSE_HOME should be defined in the enclosing Makefile as the prefix directory where Pulse was installed, or the root directory of its source repository) endif ifneq (,$(FSTAR_HOME)) @@ -8,7 +8,7 @@ else FSTAR=fstar.exe endif -# Add Steel to the OCaml (ocamlfind) search path +# Add Pulse to the OCaml (ocamlfind) search path ifeq ($(OS),Windows_NT) OCAMLPATH := $(shell cygpath -m $(PULSE_HOME)/lib);$(OCAMLPATH) else @@ -37,7 +37,7 @@ export OCAMLPATH FSTAR_FILES += $(filter-out $(EXCLUDE_FILES),$(wildcard *.fst *.fsti)) ADDITIONAL_INCLUDES ?= -FSTAR_OPTIONS += $(OTHERFLAGS) --cmi --cache_checked_modules --warn_error @241 --already_cached 'Prims,FStar,LowStar,Steel,C' --include $(PULSE_HOME)/lib/steel $(ADDITIONAL_INCLUDES) --load_cmxs steel +FSTAR_OPTIONS += $(OTHERFLAGS) --cmi --cache_checked_modules --warn_error @241 --already_cached 'Prims,FStar,LowStar,C' --include $(PULSE_HOME)/lib/steel $(ADDITIONAL_INCLUDES) --load_cmxs steel COMPAT_INDEXED_EFFECTS?=--compat_pre_typed_indexed_effects diff --git a/share/steel/examples/Makefile b/share/steel/examples/Makefile index 19493a43c..1e9923067 100644 --- a/share/steel/examples/Makefile +++ b/share/steel/examples/Makefile @@ -1,4 +1,4 @@ -TARGETS=steel pulse steelc +TARGETS=pulse all: $(TARGETS) diff --git a/share/steel/examples/pulse/Makefile.pulse.common b/share/steel/examples/pulse/Makefile.pulse.common index 13a7a45db..d47d91fc2 100644 --- a/share/steel/examples/pulse/Makefile.pulse.common +++ b/share/steel/examples/pulse/Makefile.pulse.common @@ -31,7 +31,7 @@ WARN_ERROR= SMT_OPTIONS?= OTHERFLAGS+=$(WARN_ERROR) $(SMT_OPTIONS) -ALREADY_CACHED_LIST ?= Prims,FStar,Steel,Pulse,-Pulse.Lib,-Pulse.C,-Pulse.Class +ALREADY_CACHED_LIST ?= Prims,FStar,Pulse,-Pulse.Lib,-Pulse.C,-Pulse.Class ALREADY_CACHED = --already_cached $(ALREADY_CACHED_LIST) # A place to put all build artifacts