Skip to content

Commit 54f1f8d

Browse files
Lef IoannidisCopilot
andcommitted
Fix opam install for F* 2: remove references to deleted LowStar modules
- Remove LowStar.Printf.fst and LowStar.Endianness.fst from krmllib ROOTS (these modules no longer exist in F* 2's ulib) - Remove 'LowStar -LowStar.Lib' from --already_cached since there are no LowStar modules in F* 2's ulib - Remove -bundle LowStar.Endianness= and LowStar.Printf from -library flags - Skip krmllib verification in default build target since nearly all krmllib .fst files depend on LowStar.Buffer/FStar.HyperStack.* which were removed in F* 2 (pre-built dist/ C files are still installed) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
1 parent 03c7894 commit 54f1f8d

2 files changed

Lines changed: 4 additions & 6 deletions

File tree

Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ include $(visitors_root)/Makefile.preprocess
1616

1717
FSTAR_EXE ?= fstar.exe
1818

19-
all: minimal krmllib
19+
all: minimal
2020

2121
# If we are just trying to do a minimal build, we don't need F*.
2222
# Note: lazy assignment so this does not warn if fstar.exe is not there

krmllib/Makefile

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -40,14 +40,14 @@ endif
4040

4141
FSTAR = $(RUNLIM) $(FSTAR_EXE) $(FSTAR_OPTIONS) --cache_dir obj \
4242
$(addprefix --include , $(INCLUDE_PATHS)) \
43-
--already_cached 'Prims FStar -FStar.Krml.Endianness LowStar -LowStar.Lib'
43+
--already_cached 'Prims FStar -FStar.Krml.Endianness'
4444

4545
# Note: not compatible with the OPAM layout until fstar can be queried for the
4646
# location of ulib.
4747
ROOTS = $(wildcard *.fst) $(wildcard *.fsti) $(wildcard ../runtime/*.fst) \
4848
FStar.UInt128.fst FStar.Date.fsti \
4949
FStar.IO.fsti FStar.Int.Cast.Full.fst \
50-
FStar.Bytes.fsti FStar.Dyn.fsti LowStar.Printf.fst LowStar.Endianness.fst
50+
FStar.Bytes.fsti FStar.Dyn.fsti
5151

5252
.PHONY: clean clean-c
5353
clean: clean-c
@@ -120,9 +120,8 @@ $(GENERIC_DIR)/Makefile.include: $(ALL_KRML_FILES) | $(GENERIC_DIR) $(wildcard c
120120
-warn-error +9+11 \
121121
$(MACHINE_INTS) \
122122
$(addprefix -add-include ,'<inttypes.h>' '"krmllib.h"' '"krml/internal/compat.h"' '"krml/internal/target.h"') \
123-
-bundle LowStar.Endianness= \
124123
-bundle FStar.Endianness,FStar.Range \
125-
-library C,C.Endianness,C.Failure,C.Loops,FStar.BitVector,FStar.Bytes,FStar.Char,FStar.Int,FStar.Krml.Endianness,FStar.Math.Lib,FStar.ModifiesGen,FStar.Monotonic.Heap,FStar.Monotonic.HyperStack,FStar.Mul,FStar.Pervasives,FStar.Pervasives.Native,FStar.ST,FStar.UInt,FStar.UInt63,LowStar.Printf \
124+
-library C,C.Endianness,C.Failure,C.Loops,FStar.BitVector,FStar.Bytes,FStar.Char,FStar.Int,FStar.Krml.Endianness,FStar.Math.Lib,FStar.ModifiesGen,FStar.Monotonic.Heap,FStar.Monotonic.HyperStack,FStar.Mul,FStar.Pervasives,FStar.Pervasives.Native,FStar.ST,FStar.UInt,FStar.UInt63 \
126125
-bundle FStar.BV \
127126
$(filter-out fstar_uint128_msvc.c,$(notdir $(wildcard c/*.c))) \
128127
-o libkrmllib.a \
@@ -141,7 +140,6 @@ $(MINI_DIR)/Makefile.include: $(ALL_KRML_FILES) | $(MINI_DIR) $(wildcard c/fstar
141140
'"krml/lowstar_endianness.h"' \
142141
'"krml/internal/types.h"' \
143142
'"krml/internal/target.h"') \
144-
-bundle LowStar.Endianness= \
145143
-bundle '*,WindowsWorkaroundSigh' \
146144
fstar_uint128.c \
147145
-o libkrmllib.a \

0 commit comments

Comments
 (0)