-
Notifications
You must be signed in to change notification settings - Fork 0
/
makefile.include
38 lines (31 loc) · 1.51 KB
/
makefile.include
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
# You should include this Makefile in your Makefile to make sure you remain
# future-proof w.r.t. realized modules!
# This Makefile assumes that $(FSTAR_HOME) is properly defined.
FSTAR_REALIZED_MODULES=All BaseTypes Buffer Bytes Char CommonST Constructive Dyn Float Ghost Heap Monotonic.Heap \
HyperStack.All HyperStack.ST HyperStack.IO Int16 Int32 Int63 Int64 Int8 Int.Cast IO \
List List.Tot.Base Mul Option Pervasives.Native Set ST Exn String \
UInt16 UInt32 UInt63 UInt64 UInt8 \
Pointer.Derived1 Pointer.Derived2 \
Pointer.Derived3 \
BufferNG Tactics.Builtins \
TaggedUnion \
Reflection.Types Reflection.Basic Reflection.Data \
Tactics.Result Tactics.Types Bytes Util \
Pervasives Order Range \
Vector.Base Vector.Properties Vector
# prims is realized by default hence not included in this list
NOEXTRACT_MODULES=$(addprefix FStar., $(FSTAR_REALIZED_MODULES)) prims FStar.Printf
FSTAR_DEFAULT_ARGS=$(addprefix --no_extract ,$(NOEXTRACT_MODULES))
ULIB_ML=$(FSTAR_HOME)/ulib/ml
FSTARLIB_DIR=$(FSTAR_HOME)/bin/fstarlib
FSTARLIB=$(FSTARLIB_DIR)/fstarlib.cmxa
# Left as an example if we were to add multiple versions of fstarlib
# ifeq ($(MEM),HST)
# OCAML_DEFAULT_FLAGS=-predicates hyperstack
# endif
FSTAR_HOME=$(HOME)/FStar
OCAMLOPT_BARE=OCAMLPATH="$(FSTAR_HOME)/bin" ocamlfind opt
OCAMLOPT_=$(OCAMLOPT_BARE) -package fstarlib -linkpkg -g
OCAMLOPT=$(OCAMLOPT_) $(OCAML_DEFAULT_FLAGS)
OCAMLC_=OCAMLPATH="$(FSTAR_HOME)/bin" ocamlfind c -package fstarlib -linkpkg -g
OCAMLC=$(OCAMLC_) $(OCAML_DEFAULT_FLAGS)