removed fstar libs needed for ml-kem from this PR

cryspen · Oct 30, 2024 · 72f0472 · 72f0472
1 parent 1644063
commit 72f0472
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/fstar-helpers/Makefile.base b/fstar-helpers/Makefile.base
@@ -10,5 +10,5 @@ EXTRA_HELPMESSAGE += printf "Libcrux specifics:\n";
 EXTRA_HELPMESSAGE += target SLOW_MODULES 'a list of modules to verify fully only when `VERIFY_SLOW_MODULES` is set to `yes`. When `VERIFY_SLOW_MODULES`, those modules are admitted.';
 EXTRA_HELPMESSAGE += target VERIFY_SLOW_MODULES '`yes` or `no`, defaults to `no`';
 
-FSTAR_INCLUDE_DIRS_EXTRA += $(HACL_HOME)/specs $(shell git rev-parse --show-toplevel)/fstar-helpers/fstar-bitvec
+FSTAR_INCLUDE_DIRS_EXTRA += $(HACL_HOME)/specs
 include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.generic
diff --git a/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti b/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti
@@ -1,5 +1,5 @@
 module Libcrux_platform.Platform
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
 open Core
 open FStar.Mul