From 2f5edb63c488d801542e44405f5b1d25a3b21106 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 23 Aug 2023 10:51:46 -0700 Subject: [PATCH] do not extract FStar.Tactics --- src/3d/prelude/Makefile | 2 +- src/3d/prelude/buffer/Makefile | 2 +- src/3d/prelude/extern/Makefile | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/3d/prelude/Makefile b/src/3d/prelude/Makefile index 5e4af85d4..31f6e6d6b 100644 --- a/src/3d/prelude/Makefile +++ b/src/3d/prelude/Makefile @@ -25,7 +25,7 @@ ROOT=$(wildcard *.fst) $(wildcard *.fsti) ALREADY_CACHED=--already_cached '+Prims +LowStar +FStar +LowParse +C +Spec.Loops' .depend: $(ROOT) - $(FSTAR) --dep full $(ROOT) $(ALREADY_CACHED) --extract 'krml:*,-Prims,-EverParse3d.Interpreter' > $@.tmp + $(FSTAR) --dep full $(ROOT) $(ALREADY_CACHED) --extract 'krml:*,-Prims,-EverParse3d.Interpreter,-FStar.Tactics' > $@.tmp mv $@.tmp $@ include .depend diff --git a/src/3d/prelude/buffer/Makefile b/src/3d/prelude/buffer/Makefile index f91299863..ca75f9cbc 100644 --- a/src/3d/prelude/buffer/Makefile +++ b/src/3d/prelude/buffer/Makefile @@ -24,7 +24,7 @@ ROOT=$(wildcard *.fst) $(wildcard *.fsti) ALREADY_CACHED=--already_cached '*,-EverParse3d.Actions.All,-EverParse3d.InputStream.All,-EverParse3d.InputStream.Buffer,-EverParse3d.Actions.BackendFlag,-EverParse3d.Actions.BackendFlagValue,-EverParse3d.Readable,-EverParse3d.InputBuffer' .depend: $(ROOT) - $(FSTAR) --dep full $(ROOT) $(ALREADY_CACHED) --extract '* -Prims' > $@.tmp + $(FSTAR) --dep full $(ROOT) $(ALREADY_CACHED) --extract 'krml:*,-Prims,-FStar.Tactics' > $@.tmp mv $@.tmp $@ -include .depend diff --git a/src/3d/prelude/extern/Makefile b/src/3d/prelude/extern/Makefile index 7d2a51f8e..76b019d8e 100644 --- a/src/3d/prelude/extern/Makefile +++ b/src/3d/prelude/extern/Makefile @@ -24,7 +24,7 @@ ROOT=$(wildcard *.fst) $(wildcard *.fsti) ALREADY_CACHED=--already_cached '*,-EverParse3d.Actions.All,-EverParse3d.InputStream.All,-EverParse3d.InputStream.Extern,-EverParse3d.Actions.BackendFlag,-EverParse3d.Actions.BackendFlagValue' .depend: $(ROOT) - $(FSTAR) --dep full $(ROOT) $(ALREADY_CACHED) --extract '* -Prims' > $@.tmp + $(FSTAR) --dep full $(ROOT) $(ALREADY_CACHED) --extract 'krml:*,-Prims,-FStar.Tactics' > $@.tmp mv $@.tmp $@ -include .depend