diff options
| author | Son Ho | 2022-06-27 04:40:43 +0200 |
|---|---|---|
| committer | Son Ho | 2022-06-27 04:40:43 +0200 |
| commit | 7f06278bd0b43426e88632afcd8e5633c5ab0a1e (patch) | |
| tree | e0e7afef7d6bcc3cacf0dac40a0634f4a513a894 | |
| parent | 3a930571516912714e3dcbc7ed1968228e593f99 (diff) | |
Update the Makefiles
Diffstat (limited to '')
| -rw-r--r-- | tests/Makefile.template | 5 | ||||
| -rw-r--r-- | tests/betree/Makefile | 5 | ||||
| -rw-r--r-- | tests/hashmap/Makefile | 5 | ||||
| -rw-r--r-- | tests/hashmap_on_disk/Makefile | 5 | ||||
| -rw-r--r-- | tests/misc/Makefile | 5 |
5 files changed, 5 insertions, 20 deletions
diff --git a/tests/Makefile.template b/tests/Makefile.template index fed1a280..ea838d2d 100644 --- a/tests/Makefile.template +++ b/tests/Makefile.template @@ -21,10 +21,7 @@ ifeq (,$(filter %-in,$(MAKECMDGOALS))) ifndef NODEPEND ifndef MAKE_RESTARTS .depend: .FORCE - $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \ - --extract 'krml:*' \ - --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \ - > $@ + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@ .PHONY: .FORCE .FORCE: diff --git a/tests/betree/Makefile b/tests/betree/Makefile index fed1a280..ea838d2d 100644 --- a/tests/betree/Makefile +++ b/tests/betree/Makefile @@ -21,10 +21,7 @@ ifeq (,$(filter %-in,$(MAKECMDGOALS))) ifndef NODEPEND ifndef MAKE_RESTARTS .depend: .FORCE - $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \ - --extract 'krml:*' \ - --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \ - > $@ + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@ .PHONY: .FORCE .FORCE: diff --git a/tests/hashmap/Makefile b/tests/hashmap/Makefile index fed1a280..ea838d2d 100644 --- a/tests/hashmap/Makefile +++ b/tests/hashmap/Makefile @@ -21,10 +21,7 @@ ifeq (,$(filter %-in,$(MAKECMDGOALS))) ifndef NODEPEND ifndef MAKE_RESTARTS .depend: .FORCE - $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \ - --extract 'krml:*' \ - --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \ - > $@ + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@ .PHONY: .FORCE .FORCE: diff --git a/tests/hashmap_on_disk/Makefile b/tests/hashmap_on_disk/Makefile index fed1a280..ea838d2d 100644 --- a/tests/hashmap_on_disk/Makefile +++ b/tests/hashmap_on_disk/Makefile @@ -21,10 +21,7 @@ ifeq (,$(filter %-in,$(MAKECMDGOALS))) ifndef NODEPEND ifndef MAKE_RESTARTS .depend: .FORCE - $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \ - --extract 'krml:*' \ - --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \ - > $@ + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@ .PHONY: .FORCE .FORCE: diff --git a/tests/misc/Makefile b/tests/misc/Makefile index fed1a280..ea838d2d 100644 --- a/tests/misc/Makefile +++ b/tests/misc/Makefile @@ -21,10 +21,7 @@ ifeq (,$(filter %-in,$(MAKECMDGOALS))) ifndef NODEPEND ifndef MAKE_RESTARTS .depend: .FORCE - $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \ - --extract 'krml:*' \ - --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \ - > $@ + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@ .PHONY: .FORCE .FORCE: |