<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/f6a829fea07788dc62e72a3d27c9e7e4fb73a25c">https://github.com/macports/macports-ports/commit/f6a829fea07788dc62e72a3d27c9e7e4fb73a25c</a></p>
<pre style="white-space: pre; background: #F8F8F8"><span style='display:block; white-space:pre;color:#808000;'>commit f6a829fea07788dc62e72a3d27c9e7e4fb73a25c
</span>Author: Landon Fuller <landonf@macports.org>
AuthorDate: Fri Sep 27 18:00:52 2019 -0600

<span style='display:block; white-space:pre;color:#404040;'>    fstar: new port
</span><span style='display:block; white-space:pre;color:#404040;'>    
</span><span style='display:block; white-space:pre;color:#404040;'>    Includes subports for kremlin, fstar-devel, and kremlin-devel
</span>---
 lang/fstar/Portfile                                | 363 +++++++++++++++++++++
 lang/fstar/files/fstar-select.in                   |   2 +
 .../files/kremlin-devel/patch-fix-make-command     |  26 ++
 .../files/kremlin-devel/patch-test_system_system.h |  10 +
 .../kremlin-0.9.6.0-test-hints.tar.xz              | Bin 0 -> 363308 bytes
 .../kremlin-stable/patch-disable-broken-tests      |  26 ++
 .../files/kremlin-stable/patch-fix-make-command    |  16 +
 .../fstar/files/kremlin-stable/patch-fstar-0.9.7.0 | 207 ++++++++++++
 .../fstar/files/kremlin/patch-clang-driver-options |  36 ++
 lang/fstar/files/patch-examples-fix-tests          | 179 ++++++++++
 lang/fstar/files/patch-fix-get_exec_dir            |  14 +
 lang/fstar/files/patch-no-install-checked          |  11 +
 lang/fstar/files/patch-ocaml4.08                   |  16 +
 lang/fstar/files/patch-z3-path                     |  11 +
 14 files changed, 917 insertions(+)

<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/Portfile b/lang/fstar/Portfile
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 0000000..5e9e92a
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,363 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# -*- coding: utf-8; mode: tcl; tab-width: 4; indent-tabs-mode: nil; c-basic-offset: 4 -*- vim:fenc=utf-8:ft=tcl:et:sw=4:ts=4:sts=4
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+PortSystem              1.0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+PortGroup               github  1.0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+PortGroup               ocaml   1.1
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+PortGroup               select  1.0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+name                    fstar
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+categories              lang devel
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+maintainers             {landonf @landonf}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+homepage                https://fstar-lang.org
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+platforms               darwin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+github.author           FStarLang
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+depends_build           port:ocaml-ocamlbuild
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+depends_lib             port:ocaml-batteries \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        port:ocaml-stdint \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        port:ocaml-zarith \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        port:ocaml-ppx_deriving \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        port:ocaml-ppx_deriving_yojson \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        port:ocaml-process \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        port:ocaml-yojson \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        port:ocaml-fileutils \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        port:ocaml-menhir \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        port:ocaml-pprint
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+use_configure           no
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ocaml.use_findlib       yes
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# Basic configuration options that vary based on the subport (fstar vs kremlin)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# and its release type (stable vs devel).
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+default fstar.stable        {[expr {![string match {*-devel} $subport]}]}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+default fstar.project       {[regsub {(.*?)(-devel)?$} ${subport} {\1}]}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+default fstar.port_suffix   {[expr {${fstar.stable} ? "" : "-devel"}]}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+options fstar.release \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        fstar.version
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+if {${fstar.stable}} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    fstar.version       0.9.7.0-alpha1
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # Strip everything but <major>.<minor>
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    fstar.release       [regsub {^([^\.]+\.[^\.]+).*} ${fstar.version} {\1}]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+} else {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    fstar.version       20190925
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    fstar.release       devel
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+foreach fname {fstar kremlin} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    set S [list subst -novariables]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    options ${fname}.home \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            ${fname}.bin \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            ${fname}.port \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            ${fname}.select_name \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            ${fname}.doc_dirs
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    default ${fname}.home        [{*}$S {${prefix}/libexec/[set fname]-${fstar.release}}]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    default ${fname}.bin         [{*}$S {[set fname]}]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    default ${fname}.port        [{*}$S {[set fname]${fstar.port_suffix}}]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    default ${fname}.select_name {${fstar.project}-${fstar.release}}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# Provide generic alias options for the current subport
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+foreach key {home doc_dirs bin port select_name} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    set var "${fstar.project}.${key}"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    default fstar.subport.${key}    [subst -nocommands {[set ${var}]}]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# Common fstar/fstar-devel configuration
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+if {${fstar.project} eq "fstar"} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    github.project          FStar
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    license                 MIT
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    description             General-purpose functional language aimed at program verification
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    long_description        F* (pronounced F star) is a general-purpose \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            functional programming language with effects aimed at \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            program verification. It puts together the automation \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            of an SMT-backed deductive verification tool with the \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            expressive power of a proof assistant based on \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            dependent types. After verification, F* programs can \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            be extracted to efficient OCaml, F#, C, WASM, or ASM \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            code.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    patchfiles              patch-z3-path \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            patch-examples-fix-tests \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            patch-fix-get_exec_dir
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    post-patch {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        # Always prefer MacPorts' z3 binary (rather than searching PATH)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        reinplace -E "s|@PREFIX@|${prefix}|g" \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            src/basic/FStar.Options.fs \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            src/basic/ml/FStar_Util.ml
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # destroot requires ginstall from coreutils
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    depends_build-append    port:coreutils
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    depends_lib-append      port:z3 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            port:gmp \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            port:ocaml-ulex \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            port:ocaml-migrate-parsetree \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            port:realpath
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    depends_run-append      port:fstar_select
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    fstar.doc_dirs          examples \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            contrib \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            tutorial
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# Common kremlin/kremlin-devel configuration
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+} elseif {${fstar.project} eq "kremlin"} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    github.project          kremlin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    license                 Apache-2
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    description             A tool for extracting low-level F* programs to readable C code
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    long_description        KreMLin is a tool that extracts an F* program to readable C code.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    patchfiles              kremlin/patch-clang-driver-options
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    depends_run-append      port:kremlin_select
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    depends_build-append    port:gsed
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    depends_lib-append      port:${fstar.port} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            port:coreutils \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            port:ocaml-fix \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            port:ocaml-wasm \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            port:ocaml-visitors
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    kremlin.bin             krml
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    kremlin.doc_dirs        examples
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+} else {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    ui_error "Unsupported project: ${fstar.project}"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# Subport-specific configuration
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+subport fstar {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    github.setup        ${github.author} ${github.project} ${fstar.version} V
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    distname            V${version}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    checksums           rmd160  bec45d793880ecf815bdc3d79cdb58f7f6ba7414 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        sha256  baa60f5f8a6c0dd5237a4fc7de5b8e940a3c620d680d255ae0057cf765163618 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        size    7173479
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    patchfiles-append   patch-ocaml4.08
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+subport fstar-devel {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    github.setup        ${github.author} ${github.project} 1edfde5a4cc03ad1fb60d6da7ffdd63815506276
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    version             ${fstar.version}-[string range ${github.version} 0 6]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    checksums           rmd160  74c0f8b563ea0b49fd27d3a0aeeb0c5b6bd174a4 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        sha256  ffff961a141b8242876053181ab73c925ba3a9d510b574f3522668129ae8294e \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        size    7265944
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    github.tarball_from tarball
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    post-patch {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        # Disable the known-broken kv_parsing test
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        if {${github.version} ne "1edfde5a4cc03ad1fb60d6da7ffdd63815506276"} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            ui_error "Please verify that the kv_parsing test is still broken" 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        reinplace -E {s|^kv_parsing.*|\\|g} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            examples/Makefile
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+subport kremlin {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    github.setup        ${github.author} ${fstar.project} 0.9.6.0 v
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    distname            v${version}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    worksrcdir          kremlin-${version}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # Updated z3 hints; can be generated after a valid test run via:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    #   tar -Jcf files/kremlin-0.9.6.0-test-hints.tar.xz -C work kremlin-0.9.6.0/test/.hints
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    distfiles-append    kremlin-stable/kremlin-${version}-test-hints.tar.xz
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    patchfiles-append   kremlin-stable/patch-fstar-0.9.7.0 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        kremlin-stable/patch-fix-make-command
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    github.tarball_from archive
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    checksums           rmd160  b806353b0dbc89ad4e398e14d332b36d9ea2f69a \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        sha256  547d3374e347d4e0b50bda2ed17a78719aa2265a91a2e1828a0e492e82dfb558 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        size    660454
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    depends_lib-append  port:ocaml-ulex
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # Disable known-broken test paths
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    if {${version} ne "0.9.6.0"} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        ui_error "Please verify that full test execution is still broken" 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    } else {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        patchfiles-append kremlin-stable/patch-disable-broken-tests
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    post-patch {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        # Fix path to the fstar executable
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        reinplace {s|fstar\.exe|$(FSTAR_HOME)/bin/fstar|g} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+             test/Makefile
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+subport kremlin-devel {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    github.setup        ${github.author} ${fstar.project} f6299a2aab5ad2b6a66048d22625033def041ad3
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    version             ${fstar.version}-[string range ${github.version} 0 6]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    checksums           rmd160  f2d10d648b606c3b93dcd324bbf5caad2d9199e3 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        sha256  f8ad6f4f2020d62df36f7a846f7d38c4b785137d9beaf9ba113cca5b6d460e8b \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        size    739183
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    patchfiles-append   kremlin-devel/patch-fix-make-command \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        kremlin-devel/patch-test_system_system.h
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    depends_lib-append  port:ocaml-sedlex
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    depends_test-append port:ocaml-ctypes
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# Apply shared fstar/fstar-devel subport configuration
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+if {${fstar.project} eq "fstar"} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    ocaml.package_dir   ${fstar.home}/bin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    build.args          PREFIX=${fstar.home}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    build.target        ocaml-fstar-ocaml
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    test.run            yes
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    test.env            KREMLIN_HOME=${kremlin.home}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    test.dir            ${worksrcpath}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    test.target         all
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    test.args           -C examples \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        -j ${build.jobs}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    #
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # XXX TODO:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    #
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # A number of F* test cases actually depend on KreMLin (while KreMLin depends
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # on F*).
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    #
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # We need to find a way to break this circular dependency, either by disabling
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # the given tests (and running them in KreMLin's test target?), or actually
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # building KreMLin as part of F*, or ... (?).
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    #
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # Current (as of this writing) list of examples in fstar-devel that depend on KreMLin:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    #   - csl
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    #   - kv_parsing
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    #   - low-level
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    #   - miniparse
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    #   - tactics
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    #   - typeclasses
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    #
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    depends_test        port:${kremlin.port}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    destroot.dir        ${worksrcpath}/src/ocaml-output
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    destroot.args       PREFIX=${destroot}${fstar.home}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    build {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        foreach {dir ftargets} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            src     {ocaml-fstar-ocaml}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            ulib    {install-fstarlib install-fstar-tactics all}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        } {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            build.dir       ${worksrcpath}/${dir}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            build.target    {*}${ftargets}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            do-build
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    post-destroot {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        # Remove intermediate build directories
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        foreach dir {ml tactics_ml} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            delete ${destroot}${fstar.home}/lib/fstar/${dir}/_build
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        # Drop the '.exe' file extension inserted by the build system
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        move \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            ${destroot}${fstar.home}/bin/${fstar.bin}.exe \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            ${destroot}${fstar.home}/bin/${fstar.bin}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        # Provide an fstar.exe -> fstar compatibility symlink
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        ln -shf fstar ${destroot}${fstar.home}/bin/${fstar.bin}.exe
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# Apply shared kremlin/kremlin-devel subport configuration
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+} elseif {${fstar.project} eq "kremlin"} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # If we specify PREFIX=${kremlin.home} in our build.args, a fixed path to
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # kremlin.home is hard-coded by kremlin's build system in AutoConfig.ml.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    #
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # If we exclude it, we can rely on auto-detection of kremlin.home, which
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # allows us to run krml in-place (e.g. for tests)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    build.args              FSTAR_HOME=${fstar.home} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            KREMLIN_HOME=${worksrcpath}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    test.run                yes
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    test.args               {*}${build.args} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            -j ${build.jobs}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    destroot.args           PREFIX=${destroot}${kremlin.home} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            FSTAR_HOME=${fstar.home} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            KREMLIN_HOME=${worksrcpath}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    post-patch {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        # Fix path to the fstar example sources
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        reinplace {s|\$(FSTAR_HOME)/examples|$(FSTAR_HOME)/share/fstar/examples|g} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            test/Makefile
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+#
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# Configure and register the subport's select file
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+#
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+select.group    ${fstar.project}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+select.file     ${workpath}/${fstar.project}-macports-select/${fstar.subport.select_name}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+post-patch {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    file mkdir [file dirname ${select.file}]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    copy -- ${filespath}/fstar-select.in \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        ${select.file}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    foreach {fstar_key fstar_var} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        @FSTAR_PROJECT@     fstar.project
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        @FSTAR_RELEASE@     fstar.release
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        @FSTAR_BIN@         fstar.subport.bin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    } {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        reinplace "s|${fstar_key}|[set ${fstar_var}]|g" \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            ${select.file}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+#
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# Common destroot cleanup
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+#
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+post-destroot {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # Clean up the installed files.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    fs-traverse {f} ${destroot}${fstar.subport.home} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        switch -glob -- "[file tail $f] [file type $f]" {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            {*.checked file} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                # Bump the mtime of all *.checked files by 1 second.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                #
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                # This ensures that fstar/kremlin GNU make dependencies
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                # don't try to regenerate read-only *.checked files if they
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                # have an mtime identical to their corresponding fst/fsti
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                # input (yes, that happens)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                set mtime [file mtime $f]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                file mtime $f [expr {$mtime + 1}]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            {.gitignore file} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                # Delete .gitignore files
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                delete $f
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # Add versioned documentation symlinks to share/doc/
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    xinstall -d 755 ${destroot}${prefix}/share/doc/${fstar.project}-${fstar.release}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    foreach doc_dir ${fstar.subport.doc_dirs} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        ln -sf \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            ${fstar.subport.home}/share/${fstar.project}/${doc_dir} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            ${destroot}${prefix}/share/doc/${fstar.project}-${fstar.release}/${doc_dir}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # Add a versioned symlink to bin/
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    ln -sf \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        ${fstar.subport.home}/bin/${fstar.subport.bin} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        ${destroot}${prefix}/bin/${fstar.subport.bin}-${fstar.release} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/fstar-select.in b/lang/fstar/files/fstar-select.in
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 0000000..5c671f3
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/fstar-select.in
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,2 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+libexec/@FSTAR_PROJECT@-@FSTAR_RELEASE@/bin/@FSTAR_BIN@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+share/doc/@FSTAR_PROJECT@-@FSTAR_RELEASE@
</span>\ No newline at end of file
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/kremlin-devel/patch-fix-make-command b/lang/fstar/files/kremlin-devel/patch-fix-make-command
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 0000000..64954d6
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/kremlin-devel/patch-fix-make-command
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,26 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- Makefile.orig  2019-09-13 13:05:28.664142000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ Makefile       2019-09-13 13:05:48.070466000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -42,19 +42,19 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ clean:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   rm -rf krml _build Tests.$(FLAVOR) Kremlin.$(FLAVOR)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  make -C test clean
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  make -C kremlib clean
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  $(MAKE) -C test clean
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  $(MAKE) -C kremlib clean
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ test: all
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   ./Tests.native
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  +make -C test
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  +$(MAKE) -C test
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Auto-detection
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ pre:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   @which fstar.exe >/dev/null 2>&1 || [ -x $(FSTAR_HOME)/bin/fstar.exe ] || \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     { echo "Didn't find fstar.exe in the path or in FSTAR_HOME (which is: $(FSTAR_HOME))"; exit 1; }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   @ocamlfind query fstarlib >/dev/null 2>&1 || [ -f $(FSTAR_HOME)/bin/fstarlib/fstarlib.cmxa ] || \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-    { echo "Didn't find fstarlib via ocamlfind or in FSTAR_HOME (which is: $(FSTAR_HOME)); run make -C $(FSTAR_HOME)/ulib/ml"; exit 1; }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++    { echo "Didn't find fstarlib via ocamlfind or in FSTAR_HOME (which is: $(FSTAR_HOME)); run $(MAKE) -C $(FSTAR_HOME)/ulib/ml"; exit 1; }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ install: all
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   @if [ x"$(PREFIX)" = x ]; then echo "please define PREFIX"; exit 1; fi
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/kremlin-devel/patch-test_system_system.h b/lang/fstar/files/kremlin-devel/patch-test_system_system.h
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 0000000..fa14205
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/kremlin-devel/patch-test_system_system.h
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,10 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- test/hello-system/system.h.orig        2019-09-13 13:13:26.492859000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ test/hello-system/system.h     2019-09-13 13:13:37.963118000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -3,6 +3,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include <winsock2.h>
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include <ws2tcpip.h>
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #else
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++#include <sys/socket.h>
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include <netdb.h>
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #endif
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/kremlin-stable/kremlin-0.9.6.0-test-hints.tar.xz b/lang/fstar/files/kremlin-stable/kremlin-0.9.6.0-test-hints.tar.xz
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 0000000..313a06a
</span>Binary files /dev/null and b/lang/fstar/files/kremlin-stable/kremlin-0.9.6.0-test-hints.tar.xz differ
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/kremlin-stable/patch-disable-broken-tests b/lang/fstar/files/kremlin-stable/patch-disable-broken-tests
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 0000000..e786c6c
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/kremlin-stable/patch-disable-broken-tests
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,26 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- test/Makefile.orig     2019-09-06 21:47:25.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ test/Makefile  2019-09-06 22:00:45.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -21,7 +21,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   LinkedList1.test LinkedList2.test LinkedList3.test LinkedList4.test \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   NoExtract.test InlineNoExtract.test ../book/RingBuffer.test \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   ../book/Introduction.test
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-CUSTOM            = count-uu
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++CUSTOM            =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ WASM_FILES        = \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   WasmTrap.wasm-test Wasm1.wasm-test Wasm2.wasm-test Wasm3.wasm-test Wasm4.wasm-test
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ NEGATIVE  = false
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -75,12 +75,11 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   touch $@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ $(OUTPUT_DIR)/%.exe: $(ALL_KRML_FILES) | $(KRML_BIN)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  $(KRML) $(EXTRA) -tmpdir $(subst .exe,.out,$@) -no-prefix $(notdir $*) \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-    -o $@ $(filter %.krml,$^) -bundle $(subst _,.,$*)=WindowsHack,\*
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  @echo "\033[01;31m✘\033[00m: $<"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ .SECONDEXPANSION:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ %.test: $(OUTPUT_DIR)/$$(notdir $$(subst .,_,$$*)).exe
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  @$^ && echo "\033[01;32m✔\033[00m [TEST,$*]" || (echo "\033[01;31m✘\033[00m [TEST,$*]" && false)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  @echo "\033[01;31m✘\033[00m [TEST,$*]"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Various flags to be passed to some targets...
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ $(OUTPUT_DIR)/Structs2.exe: EXTRA = -wasm -d force-c -drop C,TestLib wasm-stubs.c
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/kremlin-stable/patch-fix-make-command b/lang/fstar/files/kremlin-stable/patch-fix-make-command
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 0000000..ecd3372
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/kremlin-stable/patch-fix-make-command
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,16 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- Makefile.orig  2019-09-13 12:46:52.602303000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ Makefile       2019-09-13 12:47:08.615444000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -33,11 +33,11 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ clean:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   rm -rf krml _build Tests.$(FLAVOR) Kremlin.$(FLAVOR)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  make -C test clean
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  $(MAKE) -C test clean
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ test: all
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   ./Tests.native
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  +make -C test
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  +$(MAKE) -C test
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Auto-detection
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ pre:
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/kremlin-stable/patch-fstar-0.9.7.0 b/lang/fstar/files/kremlin-stable/patch-fstar-0.9.7.0
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 0000000..c181809
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/kremlin-stable/patch-fstar-0.9.7.0
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,207 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+diff -ru include/kremlin/fstar_bytes.h.orig include/kremlin/fstar_bytes.h
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- include/kremlin/fstar_bytes.h  2019-08-30 16:45:01.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ include/kremlin/fstar_bytes.h  2019-08-30 16:47:20.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -76,6 +76,13 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   return b;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++typedef struct K___uint8_t_uint8_t_s
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++{
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  uint8_t fst;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  uint8_t snd;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++K___uint8_t_uint8_t;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ static inline FStar_Bytes_bytes FStar_Bytes_twobytes_(K___uint8_t_uint8_t *v) {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   char *data = KRML_HOST_MALLOC(2);
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   CHECK(data);
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -145,6 +152,13 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   return FStar_Bytes_utf8_encode(str);
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++typedef struct K___FStar_Bytes_bytes_FStar_Bytes_bytes_s
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++{
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  FStar_Bytes_bytes fst;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  FStar_Bytes_bytes snd;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++K___FStar_Bytes_bytes_FStar_Bytes_bytes;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ static inline void
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ FStar_Bytes_split_(FStar_Bytes_bytes bs, FStar_UInt32_t i, K___FStar_Bytes_bytes_FStar_Bytes_bytes *dst) {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   dst->fst = FStar_Bytes_slice(bs, 0, i);
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -371,6 +385,18 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   return NULL;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++#define FStar_Pervasives_Native_None 0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++#define FStar_Pervasives_Native_Some 1
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++typedef uint8_t FStar_Pervasives_Native_option__Prims_string_tags;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++typedef struct FStar_Pervasives_Native_option__Prims_string_s
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++{
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  FStar_Pervasives_Native_option__Prims_string_tags tag;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  Prims_string v;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++FStar_Pervasives_Native_option__Prims_string;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ static inline void
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ FStar_Bytes_iutf8_opt_(FStar_Bytes_bytes b, FStar_Pervasives_Native_option__Prims_string *ret) {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   char *str = KRML_HOST_MALLOC(b.length + 1);
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+diff -ru kremlib/TestLib.fsti.orig kremlib/TestLib.fsti
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- kremlib/TestLib.fsti.orig      2019-08-30 17:29:18.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ kremlib/TestLib.fsti   2019-08-30 17:29:21.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -43,7 +43,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+       /\ is_eternal_region (frameOf b)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+       /\ HyperStack.modifies (Set.singleton (frameOf b)) h0 h1
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+       /\ HyperStack.modifies_ref (frameOf b) (Set.empty) h0 h1
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-      /\ (FStar.HyperStack.(Map.domain h0.h == Map.domain h1.h)))
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++      /\ (FStar.HyperStack.(Map.domain (FStar.HyperStack.get_hmap h0) == Map.domain (FStar.HyperStack.get_hmap h1))))
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ (** Prints: "got error code %d" where %d is the first argument *)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ val perr: FStar.UInt32.t -> Stack unit
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- book/LowStar.fst.orig  2019-08-30 17:41:49.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ book/LowStar.fst       2019-08-30 17:55:20.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -602,8 +602,8 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ /// ``ST.equal_domains`` predicate.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let equal_domains (m0 m1: HS.mem) =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  m0.HS.tip == m1.HS.tip /\
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  Set.equal (Map.domain m0.HS.h) (Map.domain m1.HS.h) /\
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  (HS.get_tip m0) == (HS.get_tip m1) /\
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  Set.equal (Map.domain (HS.get_hmap m0)) (Map.domain (HS.get_hmap m1)) /\
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   ST.same_refs_in_all_regions m0 m1
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ /// The ``equal_domains`` predicate states that a function in the ``Stack`` effect:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -625,14 +625,14 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ /// .. note::
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ///
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-///    The following examples use the ``[@ fail ]`` F* attribute. Remember that
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++///    The following examples use the ``[@ expect_failure ]`` F* attribute. Remember that
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ///    this tutorial is a valid F* file, which we put under continuous
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ///    integration and version control. This attribute merely indicates to F*
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ///    that the failure is intentional.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ///
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ /// Based on the knowledge above, consider the following failing function.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-[@ fail ]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++[@ expect_failure ]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let g (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   let b = Buffer.create 0ul 8ul in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   ()
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -653,7 +653,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ///
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ /// We can attempt to fix ``g`` by adding a call to ``push_frame``.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-[@ fail ]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++[@ expect_failure ]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let g2 (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   push_frame ();
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   let b = Buffer.create 0ul 8ul in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -702,7 +702,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let test_st_get (): St unit =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   push_frame ();
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   let m = ST.get () in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  assert (Monotonic.HyperStack.is_stack_region m.HS.tip);
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  assert (Monotonic.HyperStack.is_stack_region (HS.get_tip m));
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   pop_frame ()
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ /// These are the basic building blocks of our memory model. Verifying on top of
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -867,7 +867,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ /// Just like in C, one can only free the base pointer, i.e. this is an error:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-[@ fail ]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++[@ expect_failure ]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let test_sub_error (): St unit =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   let b = Buffer.rcreate_mm HS.root 0UL 8ul in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   let b_l = Buffer.sub b 0ul 4ul in // idx = 0; length = 4
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- test/ML16.fst.orig     2019-08-30 17:57:28.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ test/ML16.fst  2019-08-30 17:57:47.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -20,7 +20,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let test2 (_: unit):
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   StackInline (Buffer.buffer Int32.t)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  (requires (fun h0 -> is_stack_region h0.tip))
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  (requires (fun h0 -> is_stack_region (FStar.HyperStack.get_tip h0)))
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   (ensures (fun h0 b h1 -> live h1 b /\ Buffer.length b = 2))
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   let b = Buffer.create 0l 2ul in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- test/StringLit.fst.orig        2019-08-30 17:58:58.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ test/StringLit.fst     2019-08-30 17:59:36.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -5,10 +5,10 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ open FStar.HyperStack.ST
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let test (x:string): Stack string (fun _ -> true) (fun _ _ _ -> true) =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  FStar.String.strcat "hello " x
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  strcat "hello " x
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let cat (x y:string): Stack string (fun _ -> true) (fun _ _ _ -> true) =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  FStar.String.strcat x y
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  strcat x y
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let main () =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   // C strings, modeled as zero-terminated, not relying on GC
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- runtime/WasmSupport.fst.orig   2019-08-30 18:12:21.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ runtime/WasmSupport.fst        2019-08-30 18:13:19.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -30,6 +30,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ (* TODO: all of these functions are copy-pastes from whatever is written in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+  * kremlib.h. They OUGHT TO BE implement in F*! *)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++#set-options "--lax"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let eq_mask64 (x y: U64.t) =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   let open FStar.UInt64 in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   let x = lognot (logxor x y) in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- test/Inline.fst.orig   2019-08-30 18:13:52.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ test/Inline.fst        2019-08-30 18:14:16.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -8,7 +8,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ module I32 = FStar.Int32
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let alloc_and_init (i: Int32.t): StackInline (Buffer.buffer Int32.t)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  (requires (fun h0 -> FStar.Int.size (I32.v i) 16 /\ is_stack_region h0.tip))
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  (requires (fun h0 -> FStar.Int.size (I32.v i) 16 /\ is_stack_region (FStar.HyperStack.get_tip h0)))
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     // JP: why do I have to manually write the hypothesis above?
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   (ensures (fun h0 b h1 ->
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     let open FStar.Buffer in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- test/DataTypes.fst.orig        2019-08-30 18:18:21.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ test/DataTypes.fst     2019-08-30 18:18:38.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -4,10 +4,12 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ open FStar.HyperStack.ST
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ open FStar.Ghost
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++noeq
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ type t =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   | A: a:UInt32.t -> b:UInt64.t -> t
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   | B: c:UInt8.t -> d:UInt8.t -> e:erased UInt8.t -> t
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++noeq
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ type u =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   | C: f:UInt32.t -> g:UInt64.t -> u
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   | D: h:t -> i:unit -> u
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- test/Makefile  2019-08-30 22:09:45.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ test/Makefile  2019-08-30 22:42:02.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -62,8 +62,10 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ $(HINTS_DIR):
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   mkdir -p $@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++$(CACHE_DIR)/FStar.ModifiesGen.fst.checked: FSTAR+=--z3rlimit_factor 4
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ $(CACHE_DIR)/%.checked: | .depend $(HINTS_DIR)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  $(FSTAR) --hint_file $(HINTS_DIR)/$*.hints $<
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  $(FSTAR) --z3cliopt 'timeout=600000' --smtencoding.valid_intro true --smtencoding.valid_elim true --hint_file $(HINTS_DIR)/$*.hints $< && \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   touch $@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ $(OUTPUT_DIR)/%.krml: | .depend
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -72,9 +74,9 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     $(notdir $(subst .checked,,$<))
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   touch $@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-$(OUTPUT_DIR)/%.exe: $(OUTPUT_DIR)/FStar_UInt128.krml | $(KRML_BIN)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++$(OUTPUT_DIR)/%.exe: $(ALL_KRML_FILES) | $(KRML_BIN)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   $(KRML) $(EXTRA) -tmpdir $(subst .exe,.out,$@) -no-prefix $(notdir $*) \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-    -o $@ $^
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++    -o $@ $(filter %.krml,$^) -bundle $(subst _,.,$*)=WindowsHack,\*
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ .SECONDEXPANSION:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ %.test: $(OUTPUT_DIR)/$$(notdir $$(subst .,_,$$*)).exe
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/kremlin/patch-clang-driver-options b/lang/fstar/files/kremlin/patch-clang-driver-options
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 0000000..9fbf711
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/kremlin/patch-clang-driver-options
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,36 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- src/Options.ml.orig    2019-08-20 08:05:43.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ src/Options.ml 2019-09-09 11:04:27.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -24,7 +24,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let verbose = ref false
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let silent = ref false
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let exe_name = ref ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-let cc = ref "gcc"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++let cc = ref "clang"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let m32 = ref false
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let fsopts: string list ref = ref []
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let ccopts: string list ref = ref []
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -72,16 +72,21 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     "-ccopts";
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     "-Wall,-Werror,-Wno-unused-variable," ^
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     "-Wno-unknown-warning-option,-Wno-unused-but-set-variable," ^
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-    "-g,-fwrapv,-fstack-check,-D_BSD_SOURCE,-D_DEFAULT_SOURCE" ^
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++    "-g,-fwrapv,-fstack-check" ^
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     (if Sys.os_type = "Win32" then ",-D__USE_MINGW_ANSI_STDIO" else "") ^
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     (if !parentheses then "" else ",-Wno-parentheses")
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   |] in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   let gcc_options = Array.append gcc_like_options
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-    [| "-ccopt"; if !c89_std then "-std=c89" else "-std=c11" |]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++    [| "-ccopt"; if !c89_std then "-std=c89" else "-std=c11" |] in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  let clang_options = Array.append gcc_options
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  (* '-Winfinite-recursion' is triggered by the use of 'C.portable_exit'
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++   * in a recursive function; we need to disable this
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++   * warning until KreMLin adds support for the _Noreturn attribute *)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++    [| "-ccopt"; "-Wno-error=infinite-recursion" |]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   [
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     "gcc", gcc_options;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-    "clang", gcc_options;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++    "clang", clang_options;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     "g++", gcc_like_options;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     "compcert", [|
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+       "-warn-error"; "@6@8";
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/patch-examples-fix-tests b/lang/fstar/files/patch-examples-fix-tests
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 0000000..2cf451d
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/patch-examples-fix-tests
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,179 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- examples/bug-reports/Makefile.orig     2019-09-04 17:11:24.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ examples/bug-reports/Makefile  2019-09-04 17:15:26.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -2,6 +2,13 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ include ../Makefile.include
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ include $(FSTAR_HOME)/ulib/ml/Makefile.include
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++CACHE_DIR = cache
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++FSTAR_FLAGS = $(OTHERFLAGS) --cache_dir $(CACHE_DIR) \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  --cache_checked_modules --already_cached 'Prims FStar'
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ all: verify iverify not-verify extract
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+diff -ru examples.orig/kv_parsing/Makefile examples/kv_parsing/Makefile
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- examples.orig/kv_parsing/Makefile      2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ examples/kv_parsing/Makefile   2019-09-05 11:39:36.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -24,7 +24,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            EnumParsing.fst \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            VectorParsing.fst
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-FSTAR_INCLUDE_PATHS:=--include $(KREMLIN_HOME)/kremlib --include $(KREMLIN_HOME)/kremlib/compat
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++FSTAR_INCLUDE_PATHS:=--include $(KREMLIN_HOME)/lib/kremlin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ OTHERFLAGS+=$(FSTAR_INCLUDE_PATHS) --z3rlimit_factor 4
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+diff -ru examples.orig/low-level/LowCProvider/Makefile examples/low-level/LowCProvider/Makefile
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- examples.orig/low-level/LowCProvider/Makefile  2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ examples/low-level/LowCProvider/Makefile       2019-09-05 10:51:49.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -6,9 +6,9 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ MARCH?=x86_64
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ KREMLIN_HOME?=../../../../kremlin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-KRML_INCLUDES=$(addprefix -I ,.. $(KREMLIN_HOME)/kremlib $(KREMLIN_HOME)/test)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++KRML_INCLUDES=$(addprefix -I ,.. $(KREMLIN_HOME)/lib/kremlin $(KREMLIN_HOME)/test)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ KRML_ARGS=-verbose -ccopt -Wno-error=pointer-sign $(KOPTS)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-KRML=$(KREMLIN_HOME)/krml $(KRML_ARGS) $(KRML_INCLUDES)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++KRML=$(KREMLIN_HOME)/bin/krml $(KRML_ARGS) $(KRML_INCLUDES)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ OCAMLC = ocamlfind c $(INCLUDE) -g -annot
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ OCAMLOPT = ocamlfind opt $(INCLUDE) -g -annot
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+diff -ru examples.orig/low-level/Makefile examples/low-level/Makefile
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- examples.orig/low-level/Makefile       2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ examples/low-level/Makefile    2019-09-05 10:51:50.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -10,7 +10,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ CODEGEN_ARGS=--lax --codegen OCaml --no_location_info $(FSTAR_DEFAULT_ARGS)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ KREMLIN_HOME?=../../../kremlin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-KREMLIN=$(KREMLIN_HOME)/Kremlin.native
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++KREMLIN=$(KREMLIN_HOME)/bin/krml
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ KREMLIN_ARGS=-tmpdir kremlin -cc clang
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ CHACHA_ODIR=chacha
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -185,13 +185,13 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   $(FSTAR) --use_hints crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part6.fst --include crypto
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   $(FSTAR) --use_hints --include crypto crypto/Crypto.Symmetric.Poly1305.Bignum.fst
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-KRML_INCLUDES=$(addprefix -I ,spartan_aes crypto $(KREMLIN_HOME)/kremlib $(KREMLIN_HOME)/test)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++KRML_INCLUDES=$(addprefix -I ,spartan_aes crypto $(KREMLIN_HOME)/lib/kremlin $(KREMLIN_HOME)/test)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ifeq ($(OS),Windows_NT)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   KRML_ARGS=-ccopts -maes $(KOPTS)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ else
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   KRML_ARGS=-ccopts -maes,-fPIC $(KOPTS)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ endif
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-KRML=$(KREMLIN_HOME)/krml $(KRML_ARGS) $(KRML_INCLUDES) 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++KRML=$(KREMLIN_HOME)/bin/krml $(KRML_ARGS) $(KRML_INCLUDES) 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ spartan_aes/aes.o:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   make -C spartan_aes
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -205,7 +205,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                 -no-prefix Crypto.KrmlTest \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+           -dast \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+           -drop Crypto.Symmetric.GF128.Spec -drop Crypto.Symmetric.PRF \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-                $(KREMLIN_HOME)/test/../kremlib/testlib.c crypto/test_hacks.c \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++                $(KREMLIN_HOME)/lib/kremlin/testlib.c crypto/test_hacks.c \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                 -tmpdir tmp -add-include '"testlib.h"' -o $@ \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                 crypto/spartan/Crypto.Config.fst crypto/real/Flag.fst crypto/Crypto.KrmlTest.fst
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   -./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:#e0ffe0;'>+@@ -224,11 +224,11 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   # LowCProvider (which does ar ../tmp/*.o) would pick up the wrong main
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   $(KRML) tmp/out.krml -drop Crypto.KrmlTest \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                   -tmpdir tmp-test-perf -add-include '"testlib.h"' -o $@ \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-                  $(KREMLIN_HOME)/kremlib/testlib.c crypto/test_hacks.c \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++                  $(KREMLIN_HOME)/lib/kremlin/testlib.c crypto/test_hacks.c \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                   crypto/test_perf.c spartan_aes/aes.o crypto/spartan_stub.c \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                   -ldopt -flto \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                   -ccopts -Ofast,-m64,-march=native,-mtune=native,-funroll-loops,-fomit-frame-pointer,-Wno-int-conversion \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-                  -I $(KREMLIN_HOME)/kremlib -I $(KREMLIN_HOME)/test \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++                  -I $(KREMLIN_HOME)/lib/kremlin -I $(KREMLIN_HOME)/test \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                   -I $(OPENSSL_HOME)/include -ldopts -L,$(OPENSSL_HOME)/lib,-L,$(OPENSSL_HOME),-lcrypto$(WINSOCK) $(CFLAGS)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   PATH=$(OPENSSL_HOME):"$(PATH)" \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     LD_LIBRARY_PATH=$(OPENSSL_HOME):"$(LD_LIBRARY_PATH)" \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -274,8 +274,8 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+           tmp/Crypto_AEAD_Lemmas_Part2.ml \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+           tmp/Crypto_AEAD_Lemmas.ml \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+           tmp/Crypto_AEAD.ml \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-          $(KREMLIN_HOME)/kremlib/TestLib.ml \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-          $(KREMLIN_HOME)/kremlib/C.ml \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++          $(KREMLIN_HOME)/lib/kremlin/TestLib.ml \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++          $(KREMLIN_HOME)/lib/kremlin/C.ml \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+           tmp/Crypto_KrmlTest.ml
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -320,7 +320,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ocaml-test-extract: ulib
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   mkdir -p tmp
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   $(FSTAR_EXTRACT) --include crypto/hacl/ \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-          --include $(KREMLIN_HOME)/kremlib --include $(KREMLIN_HOME)/test/ \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++          --include $(KREMLIN_HOME)/lib/kremlin --include $(KREMLIN_HOME)/test/ \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+           --odir tmp crypto/Crypto.KrmlTest.fst
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   echo "let _ = main()" >> tmp/Crypto_KrmlTest.ml
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+diff -ru examples.orig/miniparse/Makefile examples/miniparse/Makefile
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- examples.orig/miniparse/Makefile       2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ examples/miniparse/Makefile    2019-09-05 11:11:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -3,7 +3,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Inspired from: ../tactics/Makefile
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ KREMLIN_HOME?=$(FSTAR_HOME)/../Kremlin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-INCLUDE_PATHS=$(KREMLIN_HOME)/kremlib
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++INCLUDE_PATHS=$(KREMLIN_HOME)/lib/kremlin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ FSTAR_FILES=$(wildcard *.fst) $(wildcard *.fsti)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ all: verify-all
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -19,7 +19,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ifdef KREMLIN_HOME
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ miniparse: $(CACHE_DIR)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-   [ ! -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:#e0ffe0;'>++   [ ! -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:#e0ffe0;'>+ else
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ miniparse:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ endif
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+diff -ru examples.orig/miniparse/bench/Makefile examples/miniparse/bench/Makefile
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- examples.orig/miniparse/bench/Makefile 2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ examples/miniparse/bench/Makefile      2019-09-05 10:51:46.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -1,7 +1,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ FSTAR_HOME=../../..
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ INCLUDE_PATHS=..
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ KREMLIN_HOME?=$(FSTAR_HOME)/../Kremlin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-INCLUDE_PATHS=$(KREMLIN_HOME)/kremlib ..
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++INCLUDE_PATHS=$(KREMLIN_HOME)/lib/kremlin ..
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ EXCLUDED_FSTAR_FILES=MiniStub.fst
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #Guido: Take SIZE > 1, or the the tactic may run out of goals
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+diff -ru examples.orig/tactics/Makefile examples/tactics/Makefile
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- examples.orig/tactics/Makefile 2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ examples/tactics/Makefile      2019-09-05 10:52:08.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -1,6 +1,6 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ FSTAR_HOME=../..
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ KREMLIN_HOME?=$(FSTAR_HOME)/../Kremlin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-INCLUDE_PATHS=$(KREMLIN_HOME)/kremlib
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++INCLUDE_PATHS=$(KREMLIN_HOME)/lib/kremlin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Poly files are here for benchmarking, and expected to fail without tactics
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 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:#e0ffe0;'>+ FSTAR_FILES = $(filter-out $(EXCLUDED_FSTAR_FILES), $(wildcard *.fst))
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -19,7 +19,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ifdef KREMLIN_HOME
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ stringprintertest: $(CACHE_DIR)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-   [ ! -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:#e0ffe0;'>++   [ ! -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:#e0ffe0;'>+ else
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ stringprintertest:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ endif
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+diff -ru examples.orig/tactics/bench/Makefile examples/tactics/bench/Makefile
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- examples.orig/tactics/bench/Makefile   2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ examples/tactics/bench/Makefile        2019-09-05 10:52:38.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -1,7 +1,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ FSTAR_HOME=../../..
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ INCLUDE_PATHS=..
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ KREMLIN_HOME?=$(FSTAR_HOME)/../Kremlin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-INCLUDE_PATHS=$(KREMLIN_HOME)/kremlib ..
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++INCLUDE_PATHS=$(KREMLIN_HOME)/lib/kremlin ..
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ EXCLUDED_FSTAR_FILES=PolyStub.fst
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ POLYS=$(foreach FACTOR,1 2 3,\
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/patch-fix-get_exec_dir b/lang/fstar/files/patch-fix-get_exec_dir
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 0000000..276b158
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/patch-fix-get_exec_dir
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,14 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- src/basic/ml/FStar_Util.ml.orig        2019-09-19 13:38:15.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ src/basic/ml/FStar_Util.ml     2019-09-19 13:38:23.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -841,7 +841,10 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let decr r = FStar_ST.(Z.(write r (read r - one)))
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let geq (i:int) (j:int) = i >= j
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-let get_exec_dir () = Filename.dirname (Sys.executable_name)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++let get_exec_dir () =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  (*  Unfortunately, OCaml does not expose realpath(3) *)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  let bin_path = String.trim (List.hd (Process.read_stdout "@PREFIX@/bin/realpath" [| Sys.executable_name |])) in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  Filename.dirname (bin_path)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let expand_environment_variable x = try Some (Sys.getenv x) with Not_found -> None
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let physical_equality (x:'a) (y:'a) = x == y
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/patch-no-install-checked b/lang/fstar/files/patch-no-install-checked
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 0000000..d4578c2
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/patch-no-install-checked
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,11 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- src/ocaml-output/Makefile.orig 2019-08-30 21:34:00.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ src/ocaml-output/Makefile      2019-08-30 21:34:24.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -182,7 +182,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # permissions and creating directories on the fly as needed.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # (JP: the package version of this command is based on git but for OPAM
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #  installs we cannot assume the user has git installed.)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-install_dir = cd ../../$(1) && find . -type f -exec $(INSTALL_EXEC) -m 644 -D {} $(PREFIX)/$(2)/{} \;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++install_dir = cd ../../$(1) && find . -type f ! -name '*.checked' -exec $(INSTALL_EXEC) -m 644 -D {} $(PREFIX)/$(2)/{} \;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # install the standard library binary files
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ install_fstarlib = $(INSTALL_EXEC) -m 755 -D ../../$(1)/$(2) $(PREFIX)/lib/fstar/$(2)
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/patch-ocaml4.08 b/lang/fstar/files/patch-ocaml4.08
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 0000000..4eacdcc
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/patch-ocaml4.08
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,16 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- src/tactics/ml/FStar_Tactics_Load.ml.orig      2019-08-26 21:44:29.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ src/tactics/ml/FStar_Tactics_Load.ml   2019-08-26 21:47:46.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -15,9 +15,11 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     | Unsafe_file -> "Unsafe_file"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     | Linking_error _ -> "Linking_error"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     | Corrupted_interface _ -> "Corrupted_interface"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-    | File_not_found _ -> "File_not_found"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-    | Cannot_open_dll _ -> "Cannot_open_dll"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++    | Cannot_open_dynamic_library _ -> "Cannot_open_dynamic_library"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++    | Library's_module_initializers_failed _ -> "Library's_module_initializers_failed"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     | Inconsistent_implementation _ -> "Inconsistent_implementation"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++    | Module_already_loaded _ -> "Module_already_loaded"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++    | Private_library_cannot_implement_interface _ -> "Private_library_cannot_implement_interface"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     in s ^ ": " ^ Dynlink.error_message e
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let find_taclib () =
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/patch-z3-path b/lang/fstar/files/patch-z3-path
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 0000000..2a60fe0
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/patch-z3-path
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,11 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- src/basic/FStar.Options.fs.orig        2019-08-28 18:32:49.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ src/basic/FStar.Options.fs     2019-08-28 18:33:08.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -1559,7 +1559,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                                       | _ -> false
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let warn_default_effects         () = get_warn_default_effects        ()
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let z3_exe                       () = match get_smt () with
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-                                    | None -> Platform.exe "z3"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++                                    | None -> Platform.exe "@PREFIX@/bin/z3"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                                     | Some s -> s
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let z3_cliopt                    () = get_z3cliopt                    ()
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let z3_refresh                   () = get_z3refresh                   ()
</span></pre><pre style='margin:0'>

</pre>