<pre style='margin:0'>
Landon Fuller (landonf) pushed a commit to branch master
in repository macports-ports.
</pre>
<p><a href="https://github.com/macports/macports-ports/commit/3784a10673be7ac50080cc6a93e1c11ca12f7479">https://github.com/macports/macports-ports/commit/3784a10673be7ac50080cc6a93e1c11ca12f7479</a></p>
<pre style="white-space: pre; background: #F8F8F8"><span style='display:block; white-space:pre;color:#808000;'>commit 3784a10673be7ac50080cc6a93e1c11ca12f7479
</span>Author: Landon Fuller <landonf@macports.org>
AuthorDate: Mon Jan 13 20:52:58 2020 -0700
<span style='display:block; white-space:pre;color:#404040;'> fstar(-devel): provide a complete FSTAR_HOME directory layout
</span>---
lang/fstar/Portfile | 39 +++--
.../files/fstar-devel/patch-examples-fix-tests | 189 ---------------------
.../files/fstar-stable/patch-examples-fix-tests | 169 +-----------------
3 files changed, 22 insertions(+), 375 deletions(-)
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/Portfile b/lang/fstar/Portfile
</span><span style='display:block; white-space:pre;color:#808080;'>index 6fcca16..0d87544 100644
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -145,7 +145,7 @@ if {${fstar.project} eq "fstar"} {
</span> # Subport-specific configuration
subport fstar {
github.setup ${github.author} ${github.project} ${fstar.version} V
<span style='display:block; white-space:pre;background:#ffe0e0;'>- revision 6
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ revision 7
</span>
distname V${version}
checksums rmd160 bec45d793880ecf815bdc3d79cdb58f7f6ba7414 \
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -159,15 +159,13 @@ subport fstar {
</span> subport fstar-devel {
github.setup ${github.author} ${github.project} 469ad10d993d82364993f225ba48004119b7d073
version ${fstar.version}-[string range ${github.version} 0 6]
<span style='display:block; white-space:pre;background:#ffe0e0;'>- revision 0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ revision 1
</span>
checksums rmd160 4dae34cd7b596dc8725e07e1b8d9f928040c093d \
sha256 04d811cccd06cd3354a92aa717e66b03fac1bff2bfbdc8d8ec3d9a1e75df62a4 \
size 7336672
github.tarball_from tarball
<span style='display:block; white-space:pre;background:#ffe0e0;'>- patchfiles-append fstar-devel/patch-examples-fix-tests
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span> post-patch {
# Disable the known-broken kv_parsing test
if {${github.version} ne "469ad10d993d82364993f225ba48004119b7d073"} {
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -181,7 +179,7 @@ subport fstar-devel {
</span>
subport kremlin {
github.setup ${github.author} ${fstar.project} 0.9.6.0 v
<span style='display:block; white-space:pre;background:#ffe0e0;'>- revision 9
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ revision 10
</span>
distname v${version}
worksrcdir kremlin-${version}
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -218,7 +216,7 @@ subport kremlin {
</span> subport kremlin-devel {
github.setup ${github.author} ${fstar.project} dc80e6cc827754952e49793a77896239843cadf0
version ${fstar.version}-[string range ${github.version} 0 6]
<span style='display:block; white-space:pre;background:#ffe0e0;'>- revision 0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ revision 1
</span>
checksums rmd160 84a191e0ca3fb9e5032de25a0210718221fe16b9 \
sha256 f6e1026894cb04d021e58ebe8ffbda273bcfba28c8f9c45c715351ccf7b1ec48 \
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -240,7 +238,7 @@ if {${fstar.project} eq "fstar"} {
</span> build.target ocaml-fstar-ocaml
test.run yes
<span style='display:block; white-space:pre;background:#ffe0e0;'>- test.env KREMLIN_HOME=${kremlin.home}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ test.env KREMLIN_HOME=${kremlin.home}/home
</span> test.dir ${worksrcpath}
test.target all
test.args -C examples \
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -297,9 +295,20 @@ if {${fstar.project} eq "fstar"} {
</span> # Provide a link to our z3 binary
ln -shf ../../z3-fstar/bin/z3 ${destroot}${fstar.home}/bin/z3
<span style='display:block; white-space:pre;background:#ffe0e0;'>- # Provide a "home" symlink for symmetry with the KreMLin port's
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # "home" directory
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ln -shf . ${destroot}${fstar.home}/home
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Provide compatibility symlinks for projects that expect F*'s
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # source layout
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set fstar_compat_home ${destroot}${fstar.home}/home
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ xinstall -d -m 755 ${fstar_compat_home}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ foreach {fstar_src fstar_dest} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ lib/fstar ulib
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ bin bin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ share/fstar/examples examples
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ share/fstar/contrib ucontrib
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ } {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ln -shf \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ../${fstar_src} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ${fstar_compat_home}/${fstar_dest}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span> }
notes "
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -326,7 +335,7 @@ if {${fstar.project} eq "fstar"} {
</span> #
# If we exclude it, we can rely on auto-detection of kremlin.home, which
# allows us to run krml in-place (e.g. for tests)
<span style='display:block; white-space:pre;background:#ffe0e0;'>- build.args FSTAR_HOME=${fstar.home} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ build.args FSTAR_HOME=${fstar.home}/home \
</span> KREMLIN_HOME=${worksrcpath}
test.run yes
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -334,15 +343,9 @@ if {${fstar.project} eq "fstar"} {
</span> -j ${build.jobs}
destroot.args PREFIX=${destroot}${kremlin.home} \
<span style='display:block; white-space:pre;background:#ffe0e0;'>- FSTAR_HOME=${fstar.home} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ FSTAR_HOME=${fstar.home}/home \
</span> KREMLIN_HOME=${worksrcpath}
<span style='display:block; white-space:pre;background:#ffe0e0;'>- post-patch {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # Fix path to the fstar example sources
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- reinplace {s|\$(FSTAR_HOME)/examples|$(FSTAR_HOME)/share/fstar/examples|g} \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- test/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span> post-destroot {
# KreMLin-specific cleanup up the installed files.
fs-traverse {f} ${destroot}${fstar.subport.home} {
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/fstar-devel/patch-examples-fix-tests b/lang/fstar/files/fstar-devel/patch-examples-fix-tests
</span>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 5926c03..0000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/files/fstar-devel/patch-examples-fix-tests
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,189 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples/bug-reports/Makefile.orig 2019-09-04 17:11:24.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/bug-reports/Makefile 2019-09-04 17:15:26.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -2,6 +2,13 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- include ../Makefile.include
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- include $(FSTAR_HOME)/ulib/ml/Makefile.include
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+CACHE_DIR = cache
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+FSTAR_FLAGS = $(OTHERFLAGS) --cache_dir $(CACHE_DIR) \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ --cache_checked_modules --already_cached 'Prims FStar'
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- all: verify iverify not-verify extract
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-diff -ru examples.orig/kv_parsing/Makefile examples/kv_parsing/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples.orig/kv_parsing/Makefile 2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/kv_parsing/Makefile 2019-09-05 11:39:36.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -24,7 +24,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- EnumParsing.fst \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- VectorParsing.fst
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--FSTAR_INCLUDE_PATHS:=--include $(KREMLIN_HOME)/kremlib --include $(KREMLIN_HOME)/kremlib/compat
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+FSTAR_INCLUDE_PATHS:=--include $(KREMLIN_HOME)/lib/kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- OTHERFLAGS+=$(FSTAR_INCLUDE_PATHS) --z3rlimit_factor 4
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-diff -ru examples.orig/low-level/LowCProvider/Makefile examples/low-level/LowCProvider/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples.orig/low-level/LowCProvider/Makefile 2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/low-level/LowCProvider/Makefile 2019-09-05 10:51:49.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -6,9 +6,9 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- MARCH?=x86_64
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KREMLIN_HOME?=../../../../kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--KRML_INCLUDES=$(addprefix -I ,.. $(KREMLIN_HOME)/kremlib $(KREMLIN_HOME)/test)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+KRML_INCLUDES=$(addprefix -I ,.. $(KREMLIN_HOME)/lib/kremlin $(KREMLIN_HOME)/test)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KRML_ARGS=-verbose -ccopt -Wno-error=pointer-sign $(KOPTS)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--KRML=$(KREMLIN_HOME)/krml $(KRML_ARGS) $(KRML_INCLUDES)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+KRML=$(KREMLIN_HOME)/bin/krml $(KRML_ARGS) $(KRML_INCLUDES)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- OCAMLC = ocamlfind c $(INCLUDE) -g -annot
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- OCAMLOPT = ocamlfind opt $(INCLUDE) -g -annot
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-diff -ru examples.orig/low-level/Makefile examples/low-level/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples.orig/low-level/Makefile 2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/low-level/Makefile 2019-09-05 10:51:50.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -10,7 +10,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- CODEGEN_ARGS=--lax --codegen OCaml --no_location_info $(FSTAR_DEFAULT_ARGS)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KREMLIN_HOME?=../../../kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--KREMLIN=$(KREMLIN_HOME)/Kremlin.native
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+KREMLIN=$(KREMLIN_HOME)/bin/krml
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KREMLIN_ARGS=-tmpdir kremlin -cc clang
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- CHACHA_ODIR=chacha
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -185,13 +185,13 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- $(FSTAR) --use_hints crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part6.fst --include crypto
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- $(FSTAR) --use_hints --include crypto crypto/Crypto.Symmetric.Poly1305.Bignum.fst
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--KRML_INCLUDES=$(addprefix -I ,spartan_aes crypto $(KREMLIN_HOME)/kremlib $(KREMLIN_HOME)/test)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+KRML_INCLUDES=$(addprefix -I ,spartan_aes crypto $(KREMLIN_HOME)/lib/kremlin $(KREMLIN_HOME)/test)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ifeq ($(OS),Windows_NT)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KRML_ARGS=-ccopts -maes $(KOPTS)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- else
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KRML_ARGS=-ccopts -maes,-fPIC $(KOPTS)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- endif
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--KRML=$(KREMLIN_HOME)/krml $(KRML_ARGS) $(KRML_INCLUDES)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+KRML=$(KREMLIN_HOME)/bin/krml $(KRML_ARGS) $(KRML_INCLUDES)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- spartan_aes/aes.o:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- make -C spartan_aes
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -205,7 +205,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -no-prefix Crypto.KrmlTest \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -dast \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -drop Crypto.Symmetric.GF128.Spec -drop Crypto.Symmetric.PRF \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-- $(KREMLIN_HOME)/test/../kremlib/testlib.c crypto/test_hacks.c \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ $(KREMLIN_HOME)/lib/kremlin/testlib.c crypto/test_hacks.c \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -tmpdir tmp -add-include '"testlib.h"' -o $@ \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- crypto/spartan/Crypto.Config.fst crypto/real/Flag.fst crypto/Crypto.KrmlTest.fst
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -./krml-test.exe #AR: 04/27: this fails, but the tests don't apparently use it. will raise a bug for this too.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -224,11 +224,11 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # LowCProvider (which does ar ../tmp/*.o) would pick up the wrong main
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- $(KRML) tmp/out.krml -drop Crypto.KrmlTest \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -tmpdir tmp-test-perf -add-include '"testlib.h"' -o $@ \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-- $(KREMLIN_HOME)/kremlib/testlib.c crypto/test_hacks.c \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ $(KREMLIN_HOME)/lib/kremlin/testlib.c crypto/test_hacks.c \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- crypto/test_perf.c spartan_aes/aes.o crypto/spartan_stub.c \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -ldopt -flto \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -ccopts -Ofast,-m64,-march=native,-mtune=native,-funroll-loops,-fomit-frame-pointer,-Wno-int-conversion \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-- -I $(KREMLIN_HOME)/kremlib -I $(KREMLIN_HOME)/test \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ -I $(KREMLIN_HOME)/lib/kremlin -I $(KREMLIN_HOME)/test \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -I $(OPENSSL_HOME)/include -ldopts -L,$(OPENSSL_HOME)/lib,-L,$(OPENSSL_HOME),-lcrypto$(WINSOCK) $(CFLAGS)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- PATH=$(OPENSSL_HOME):"$(PATH)" \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- LD_LIBRARY_PATH=$(OPENSSL_HOME):"$(LD_LIBRARY_PATH)" \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -274,8 +274,8 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- tmp/Crypto_AEAD_Lemmas_Part2.ml \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- tmp/Crypto_AEAD_Lemmas.ml \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- tmp/Crypto_AEAD.ml \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-- $(KREMLIN_HOME)/kremlib/TestLib.ml \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-- $(KREMLIN_HOME)/kremlib/C.ml \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ $(KREMLIN_HOME)/lib/kremlin/TestLib.ml \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ $(KREMLIN_HOME)/lib/kremlin/C.ml \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- tmp/Crypto_KrmlTest.ml
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -320,7 +320,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ocaml-test-extract: ulib
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- mkdir -p tmp
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- $(FSTAR_EXTRACT) --include crypto/hacl/ \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-- --include $(KREMLIN_HOME)/kremlib --include $(KREMLIN_HOME)/test/ \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ --include $(KREMLIN_HOME)/lib/kremlin --include $(KREMLIN_HOME)/test/ \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- --odir tmp crypto/Crypto.KrmlTest.fst
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- echo "let _ = main()" >> tmp/Crypto_KrmlTest.ml
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-diff -ru examples.orig/miniparse/Makefile examples/miniparse/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples.orig/miniparse/Makefile 2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/miniparse/Makefile 2019-09-05 11:11:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -3,7 +3,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # Inspired from: ../tactics/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KREMLIN_HOME?=$(FSTAR_HOME)/../Kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--INCLUDE_PATHS=$(KREMLIN_HOME)/kremlib
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+INCLUDE_PATHS=$(KREMLIN_HOME)/lib/kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- FSTAR_FILES=$(wildcard *.fst) $(wildcard *.fsti)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- all: verify-all
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -19,7 +19,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ifdef KREMLIN_HOME
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- miniparse: $(CACHE_DIR)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-- [ ! -f $(KREMLIN_HOME)/krml ] || [ ! -x $(KREMLIN_HOME)/krml ] || $(KREMLIN_HOME)/krml -tmpdir miniparse -bundle 'MiniParse.\*' -drop 'FStar.Tactics.\*' -drop 'FStar.Reflection.\*' MiniParseExample3.fst -skip-linking
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ [ ! -f $(KREMLIN_HOME)/bin/krml ] || [ ! -x $(KREMLIN_HOME)/bin/krml ] || $(KREMLIN_HOME)/bin/krml -tmpdir miniparse -bundle 'MiniParse.\*' -drop 'FStar.Tactics.\*' -drop 'FStar.Reflection.\*' MiniParseExample3.fst -skip-linking
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- else
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- miniparse:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- endif
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-diff -ru examples.orig/miniparse/bench/Makefile examples/miniparse/bench/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples.orig/miniparse/bench/Makefile 2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/miniparse/bench/Makefile 2019-09-05 10:51:46.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -1,7 +1,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- FSTAR_HOME=../../..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- INCLUDE_PATHS=..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KREMLIN_HOME?=$(FSTAR_HOME)/../Kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--INCLUDE_PATHS=$(KREMLIN_HOME)/kremlib ..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+INCLUDE_PATHS=$(KREMLIN_HOME)/lib/kremlin ..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- EXCLUDED_FSTAR_FILES=MiniStub.fst
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- #Guido: Take SIZE > 1, or the the tactic may run out of goals
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-diff -ru examples.orig/tactics/Makefile examples/tactics/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples.orig/tactics/Makefile 2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/tactics/Makefile 2019-09-05 10:52:08.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -1,6 +1,6 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- FSTAR_HOME=../..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KREMLIN_HOME?=$(FSTAR_HOME)/../Kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--INCLUDE_PATHS=$(KREMLIN_HOME)/kremlib
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+INCLUDE_PATHS=$(KREMLIN_HOME)/lib/kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # Poly files are here for benchmarking, and expected to fail without tactics
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- EXCLUDED_FSTAR_FILES=Launch.fst Test.Math.Lemmas.fst CanonDeep.fst Poly1.fst Poly2.fst StringPrinterTest.fst
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- FSTAR_FILES = $(filter-out $(EXCLUDED_FSTAR_FILES), $(wildcard *.fst))
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -19,7 +19,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ifdef KREMLIN_HOME
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- stringprintertest: $(CACHE_DIR)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-- [ ! -f $(KREMLIN_HOME)/krml ] || [ ! -x $(KREMLIN_HOME)/krml ] || $(KREMLIN_HOME)/krml -tmpdir stringprintertest -bundle 'StringPrinter.\*' -bundle StringPrinterTest.Aux -drop 'FStar.Tactics.\*' -drop 'FStar.Reflection.\*' StringPrinterTest.fst -skip-linking
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ [ ! -f $(KREMLIN_HOME)/bin/krml ] || [ ! -x $(KREMLIN_HOME)/bin/krml ] || $(KREMLIN_HOME)/bin/krml -tmpdir stringprintertest -bundle 'StringPrinter.\*' -bundle StringPrinterTest.Aux -drop 'FStar.Tactics.\*' -drop 'FStar.Reflection.\*' StringPrinterTest.fst -skip-linking
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- else
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- stringprintertest:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- endif
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-diff -ru examples.orig/tactics/bench/Makefile examples/tactics/bench/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples.orig/tactics/bench/Makefile 2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/tactics/bench/Makefile 2019-09-05 10:52:38.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -1,7 +1,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- FSTAR_HOME=../../..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- INCLUDE_PATHS=..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KREMLIN_HOME?=$(FSTAR_HOME)/../Kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--INCLUDE_PATHS=$(KREMLIN_HOME)/kremlib ..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+INCLUDE_PATHS=$(KREMLIN_HOME)/lib/kremlin ..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- EXCLUDED_FSTAR_FILES=PolyStub.fst
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- POLYS=$(foreach FACTOR,1 2 3,\
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples/param/Makefile.orig 2019-11-29 14:59:14.453844000 -0700
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/param/Makefile 2019-11-29 14:59:39.246708000 -0700
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -1,6 +1,6 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- FSTAR_HOME=../..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KREMLIN_HOME?=$(FSTAR_HOME)/../Kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--INCLUDE_PATHS=$(KREMLIN_HOME)/kremlib
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+INCLUDE_PATHS=$(KREMLIN_HOME)/lib/kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- FSTAR_FILES = $(wildcard *.fst)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- all: verify-all
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/fstar-stable/patch-examples-fix-tests b/lang/fstar/files/fstar-stable/patch-examples-fix-tests
</span><span style='display:block; white-space:pre;color:#808080;'>index 2cf451d..bc66fb8 100644
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/files/fstar-stable/patch-examples-fix-tests
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/fstar-stable/patch-examples-fix-tests
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,19 +1,3 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples/bug-reports/Makefile.orig 2019-09-04 17:11:24.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/bug-reports/Makefile 2019-09-04 17:15:26.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -2,6 +2,13 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- include ../Makefile.include
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- include $(FSTAR_HOME)/ulib/ml/Makefile.include
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+CACHE_DIR = cache
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+FSTAR_FLAGS = $(OTHERFLAGS) --cache_dir $(CACHE_DIR) \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ --cache_checked_modules --already_cached 'Prims FStar'
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- all: verify iverify not-verify extract
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span> diff -ru examples.orig/kv_parsing/Makefile examples/kv_parsing/Makefile
--- examples.orig/kv_parsing/Makefile 2019-09-05 10:44:53.000000000 -0600
+++ examples/kv_parsing/Makefile 2019-09-05 11:39:36.000000000 -0600
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -22,158 +6,7 @@ diff -ru examples.orig/kv_parsing/Makefile examples/kv_parsing/Makefile
</span> VectorParsing.fst
-FSTAR_INCLUDE_PATHS:=--include $(KREMLIN_HOME)/kremlib --include $(KREMLIN_HOME)/kremlib/compat
<span style='display:block; white-space:pre;background:#ffe0e0;'>-+FSTAR_INCLUDE_PATHS:=--include $(KREMLIN_HOME)/lib/kremlin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++FSTAR_INCLUDE_PATHS:=--include $(KREMLIN_HOME)/kremlib
</span>
OTHERFLAGS+=$(FSTAR_INCLUDE_PATHS) --z3rlimit_factor 4
<span style='display:block; white-space:pre;background:#ffe0e0;'>-diff -ru examples.orig/low-level/LowCProvider/Makefile examples/low-level/LowCProvider/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples.orig/low-level/LowCProvider/Makefile 2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/low-level/LowCProvider/Makefile 2019-09-05 10:51:49.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -6,9 +6,9 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- MARCH?=x86_64
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KREMLIN_HOME?=../../../../kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--KRML_INCLUDES=$(addprefix -I ,.. $(KREMLIN_HOME)/kremlib $(KREMLIN_HOME)/test)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+KRML_INCLUDES=$(addprefix -I ,.. $(KREMLIN_HOME)/lib/kremlin $(KREMLIN_HOME)/test)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KRML_ARGS=-verbose -ccopt -Wno-error=pointer-sign $(KOPTS)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--KRML=$(KREMLIN_HOME)/krml $(KRML_ARGS) $(KRML_INCLUDES)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+KRML=$(KREMLIN_HOME)/bin/krml $(KRML_ARGS) $(KRML_INCLUDES)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- OCAMLC = ocamlfind c $(INCLUDE) -g -annot
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- OCAMLOPT = ocamlfind opt $(INCLUDE) -g -annot
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-diff -ru examples.orig/low-level/Makefile examples/low-level/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples.orig/low-level/Makefile 2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/low-level/Makefile 2019-09-05 10:51:50.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -10,7 +10,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- CODEGEN_ARGS=--lax --codegen OCaml --no_location_info $(FSTAR_DEFAULT_ARGS)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KREMLIN_HOME?=../../../kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--KREMLIN=$(KREMLIN_HOME)/Kremlin.native
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+KREMLIN=$(KREMLIN_HOME)/bin/krml
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KREMLIN_ARGS=-tmpdir kremlin -cc clang
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- CHACHA_ODIR=chacha
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -185,13 +185,13 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- $(FSTAR) --use_hints crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part6.fst --include crypto
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- $(FSTAR) --use_hints --include crypto crypto/Crypto.Symmetric.Poly1305.Bignum.fst
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--KRML_INCLUDES=$(addprefix -I ,spartan_aes crypto $(KREMLIN_HOME)/kremlib $(KREMLIN_HOME)/test)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+KRML_INCLUDES=$(addprefix -I ,spartan_aes crypto $(KREMLIN_HOME)/lib/kremlin $(KREMLIN_HOME)/test)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ifeq ($(OS),Windows_NT)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KRML_ARGS=-ccopts -maes $(KOPTS)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- else
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KRML_ARGS=-ccopts -maes,-fPIC $(KOPTS)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- endif
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--KRML=$(KREMLIN_HOME)/krml $(KRML_ARGS) $(KRML_INCLUDES)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+KRML=$(KREMLIN_HOME)/bin/krml $(KRML_ARGS) $(KRML_INCLUDES)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- spartan_aes/aes.o:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- make -C spartan_aes
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -205,7 +205,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -no-prefix Crypto.KrmlTest \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -dast \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -drop Crypto.Symmetric.GF128.Spec -drop Crypto.Symmetric.PRF \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-- $(KREMLIN_HOME)/test/../kremlib/testlib.c crypto/test_hacks.c \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ $(KREMLIN_HOME)/lib/kremlin/testlib.c crypto/test_hacks.c \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -tmpdir tmp -add-include '"testlib.h"' -o $@ \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- crypto/spartan/Crypto.Config.fst crypto/real/Flag.fst crypto/Crypto.KrmlTest.fst
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -./krml-test.exe #AR: 04/27: this fails, but the tests don't apparently use it. will raise a bug for this too.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -224,11 +224,11 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # LowCProvider (which does ar ../tmp/*.o) would pick up the wrong main
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- $(KRML) tmp/out.krml -drop Crypto.KrmlTest \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -tmpdir tmp-test-perf -add-include '"testlib.h"' -o $@ \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-- $(KREMLIN_HOME)/kremlib/testlib.c crypto/test_hacks.c \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ $(KREMLIN_HOME)/lib/kremlin/testlib.c crypto/test_hacks.c \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- crypto/test_perf.c spartan_aes/aes.o crypto/spartan_stub.c \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -ldopt -flto \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -ccopts -Ofast,-m64,-march=native,-mtune=native,-funroll-loops,-fomit-frame-pointer,-Wno-int-conversion \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-- -I $(KREMLIN_HOME)/kremlib -I $(KREMLIN_HOME)/test \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ -I $(KREMLIN_HOME)/lib/kremlin -I $(KREMLIN_HOME)/test \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -I $(OPENSSL_HOME)/include -ldopts -L,$(OPENSSL_HOME)/lib,-L,$(OPENSSL_HOME),-lcrypto$(WINSOCK) $(CFLAGS)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- PATH=$(OPENSSL_HOME):"$(PATH)" \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- LD_LIBRARY_PATH=$(OPENSSL_HOME):"$(LD_LIBRARY_PATH)" \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -274,8 +274,8 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- tmp/Crypto_AEAD_Lemmas_Part2.ml \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- tmp/Crypto_AEAD_Lemmas.ml \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- tmp/Crypto_AEAD.ml \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-- $(KREMLIN_HOME)/kremlib/TestLib.ml \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-- $(KREMLIN_HOME)/kremlib/C.ml \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ $(KREMLIN_HOME)/lib/kremlin/TestLib.ml \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ $(KREMLIN_HOME)/lib/kremlin/C.ml \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- tmp/Crypto_KrmlTest.ml
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -320,7 +320,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ocaml-test-extract: ulib
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- mkdir -p tmp
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- $(FSTAR_EXTRACT) --include crypto/hacl/ \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-- --include $(KREMLIN_HOME)/kremlib --include $(KREMLIN_HOME)/test/ \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ --include $(KREMLIN_HOME)/lib/kremlin --include $(KREMLIN_HOME)/test/ \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- --odir tmp crypto/Crypto.KrmlTest.fst
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- echo "let _ = main()" >> tmp/Crypto_KrmlTest.ml
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-diff -ru examples.orig/miniparse/Makefile examples/miniparse/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples.orig/miniparse/Makefile 2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/miniparse/Makefile 2019-09-05 11:11:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -3,7 +3,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # Inspired from: ../tactics/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KREMLIN_HOME?=$(FSTAR_HOME)/../Kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--INCLUDE_PATHS=$(KREMLIN_HOME)/kremlib
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+INCLUDE_PATHS=$(KREMLIN_HOME)/lib/kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- FSTAR_FILES=$(wildcard *.fst) $(wildcard *.fsti)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- all: verify-all
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -19,7 +19,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ifdef KREMLIN_HOME
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- miniparse: $(CACHE_DIR)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-- [ ! -f $(KREMLIN_HOME)/krml ] || [ ! -x $(KREMLIN_HOME)/krml ] || $(KREMLIN_HOME)/krml -tmpdir miniparse -bundle 'MiniParse.\*' -drop 'FStar.Tactics.\*' -drop 'FStar.Reflection.\*' MiniParseExample3.fst -skip-linking
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ [ ! -f $(KREMLIN_HOME)/bin/krml ] || [ ! -x $(KREMLIN_HOME)/bin/krml ] || $(KREMLIN_HOME)/bin/krml -tmpdir miniparse -bundle 'MiniParse.\*' -drop 'FStar.Tactics.\*' -drop 'FStar.Reflection.\*' MiniParseExample3.fst -skip-linking
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- else
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- miniparse:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- endif
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-diff -ru examples.orig/miniparse/bench/Makefile examples/miniparse/bench/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples.orig/miniparse/bench/Makefile 2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/miniparse/bench/Makefile 2019-09-05 10:51:46.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -1,7 +1,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- FSTAR_HOME=../../..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- INCLUDE_PATHS=..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KREMLIN_HOME?=$(FSTAR_HOME)/../Kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--INCLUDE_PATHS=$(KREMLIN_HOME)/kremlib ..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+INCLUDE_PATHS=$(KREMLIN_HOME)/lib/kremlin ..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- EXCLUDED_FSTAR_FILES=MiniStub.fst
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- #Guido: Take SIZE > 1, or the the tactic may run out of goals
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-diff -ru examples.orig/tactics/Makefile examples/tactics/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples.orig/tactics/Makefile 2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/tactics/Makefile 2019-09-05 10:52:08.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -1,6 +1,6 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- FSTAR_HOME=../..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KREMLIN_HOME?=$(FSTAR_HOME)/../Kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--INCLUDE_PATHS=$(KREMLIN_HOME)/kremlib
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+INCLUDE_PATHS=$(KREMLIN_HOME)/lib/kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # Poly files are here for benchmarking, and expected to fail without tactics
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- EXCLUDED_FSTAR_FILES=Launch.fst Test.Math.Lemmas.fst CanonDeep.fst Poly1.fst Poly2.fst StringPrinterTest.fst
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- FSTAR_FILES = $(filter-out $(EXCLUDED_FSTAR_FILES), $(wildcard *.fst))
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -19,7 +19,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ifdef KREMLIN_HOME
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- stringprintertest: $(CACHE_DIR)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-- [ ! -f $(KREMLIN_HOME)/krml ] || [ ! -x $(KREMLIN_HOME)/krml ] || $(KREMLIN_HOME)/krml -tmpdir stringprintertest -bundle 'StringPrinter.\*' -bundle StringPrinterTest.Aux -drop 'FStar.Tactics.\*' -drop 'FStar.Reflection.\*' StringPrinterTest.fst -skip-linking
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+ [ ! -f $(KREMLIN_HOME)/bin/krml ] || [ ! -x $(KREMLIN_HOME)/bin/krml ] || $(KREMLIN_HOME)/bin/krml -tmpdir stringprintertest -bundle 'StringPrinter.\*' -bundle StringPrinterTest.Aux -drop 'FStar.Tactics.\*' -drop 'FStar.Reflection.\*' StringPrinterTest.fst -skip-linking
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- else
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- stringprintertest:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- endif
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-diff -ru examples.orig/tactics/bench/Makefile examples/tactics/bench/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples.orig/tactics/bench/Makefile 2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/tactics/bench/Makefile 2019-09-05 10:52:38.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -1,7 +1,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- FSTAR_HOME=../../..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- INCLUDE_PATHS=..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- KREMLIN_HOME?=$(FSTAR_HOME)/../Kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--INCLUDE_PATHS=$(KREMLIN_HOME)/kremlib ..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+INCLUDE_PATHS=$(KREMLIN_HOME)/lib/kremlin ..
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- EXCLUDED_FSTAR_FILES=PolyStub.fst
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- POLYS=$(foreach FACTOR,1 2 3,\
</span></pre><pre style='margin:0'>
</pre>