<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/04bcb0dba808ca74e882bc3a41bb34ece312a728">https://github.com/macports/macports-ports/commit/04bcb0dba808ca74e882bc3a41bb34ece312a728</a></p>
<pre style="white-space: pre; background: #F8F8F8"><span style='display:block; white-space:pre;color:#808000;'>commit 04bcb0dba808ca74e882bc3a41bb34ece312a728
</span>Author: Landon Fuller <landonf@macports.org>
AuthorDate: Thu Sep 2 12:43:54 2021 -0600

<span style='display:block; white-space:pre;color:#404040;'>    fstar|kremlin: update to 2021.09.02|2021.08.24, drop *-devel and *_select ports, and update dependents.
</span>---
 devel/everparse/Portfile                           |  10 +-
 lang/fstar/Portfile                                | 493 ++++++++-------------
 lang/fstar/files/fstar-select.in                   |   3 -
 .../files/fstar-stable/patch-examples-fix-tests    |  12 -
 .../files/fstar-stable/patch-fix-get_exec_dir      |  14 -
 lang/fstar/files/fstar-stable/patch-ocaml4.08      |  16 -
 .../{fstar-devel => fstar}/patch-fix-get_exec_dir  |   0
 .../patch-tests_machine__integers_Makefile         |   0
 lang/fstar/files/{ => fstar}/patch-z3-path         |   0
 .../kremlin-0.9.6.0-test-hints.tar.xz              | Bin 363308 -> 0 bytes
 .../kremlin-stable/patch-clang-driver-options      |  36 --
 .../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 ---------
 .../files/kremlin-stable/patch-fstar-discover-path |  90 ----
 .../patch-clang-driver-options                     |   0
 .../patch-fstar-discover-path                      |   0
 .../patch-fstar-driver-no-lax                      |   0
 .../patch-kremlib-march-native                     |   0
 .../patch-test_system_system.h                     |   0
 lang/fstar/files/patch-no-install-checked          |  11 -
 ocaml/ocaml-hacl-star/Portfile                     |   9 +-
 sysutils/fstar_select/Portfile                     |  63 ---
 sysutils/fstar_select/files/base.in                |   3 -
 sysutils/fstar_select/files/none                   |   3 -
 25 files changed, 193 insertions(+), 819 deletions(-)

<span style='display:block; white-space:pre;color:#808080;'>diff --git a/devel/everparse/Portfile b/devel/everparse/Portfile
</span><span style='display:block; white-space:pre;color:#808080;'>index 56e81c627c6..de14c784581 100644
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/devel/everparse/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/devel/everparse/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -6,7 +6,7 @@ PortGroup github    1.0
</span> name                everparse
 github.setup        project-everest everparse d61b5afa052aff422c146e3db297d257802c043d
 version             20210727-[string range ${github.version} 0 6]
<span style='display:block; white-space:pre;background:#ffe0e0;'>-revision            0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+revision            1
</span> 
 categories          devel
 platforms           darwin
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -21,8 +21,8 @@ checksums           rmd160  369d843747ec78391e9ba4762c5e0044792b67fe \
</span>                     sha256  44df578f65e07df5c3c125707dd6c2417c8c5f9f2b26b2527f3e51adca63b0e3 \
                     size    863604
 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-depends_lib         port:fstar-devel \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                    port:kremlin-devel \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+depends_lib         port:fstar \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                    port:kremlin \
</span>                     port:ocaml-hacl-star
 
 depends_build       port:ocaml \
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -39,8 +39,8 @@ options             lowparse.home \
</span>                     fstar.home \
                     kremlin.home
 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-default fstar.home      {${prefix}/libexec/fstar-devel}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-default kremlin.home    {${prefix}/libexec/kremlin-devel}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+default fstar.home      {${prefix}/libexec/fstar}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+default kremlin.home    {${prefix}/libexec/kremlin}
</span> default lowparse.home   {${prefix}/libexec/${subport}}
 
 pre-patch {
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/Portfile b/lang/fstar/Portfile
</span><span style='display:block; white-space:pre;color:#808080;'>index 4d1006c2cc7..a3316303781 100644
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -2,8 +2,6 @@
</span> 
 PortSystem              1.0
 PortGroup               github  1.0
<span style='display:block; white-space:pre;background:#ffe0e0;'>-PortGroup               ocaml   1.1
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-PortGroup               select  1.0
</span> 
 name                    fstar
 categories              lang devel
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -12,71 +10,58 @@ maintainers             {landonf @landonf}
</span> homepage                https://fstar-lang.org
 platforms               darwin
 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-github.author           FStarLang
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-depends_build           port:ocaml-ocamlbuild \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        port:gmake
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-# Requires gmake 3.82+
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-build.cmd               ${prefix}/bin/gmake
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-depends_lib             port:ocaml-batteries \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        port:ocaml-stdint \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        port:ocaml-zarith \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        port:ocaml-ppx_deriving \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        port:ocaml-ppx_deriving_yojson \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        port:ocaml-process \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        port:ocaml-yojson \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        port:ocaml-fileutils \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        port:ocaml-menhir \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        port:ocaml-pprint
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-use_configure           no
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-ocaml.use_findlib       yes
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-# Basic configuration options that vary based on the subport (fstar vs kremlin)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-# and its release type (stable vs devel).
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-default fstar.stable        {[expr {![string match {*-devel} $subport]}]}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-default fstar.project       {[regsub {(.*?)(-devel)?$} ${subport} {\1}]}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-default fstar.port_suffix   {[expr {${fstar.stable} ? "" : "-devel"}]}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-options fstar.release \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        fstar.version
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-if {${fstar.stable}} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    fstar.version       0.9.7.0-alpha1
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    # Strip everything but <major>.<minor>
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    fstar.release       [regsub {^([^\.]+\.[^\.]+).*} ${fstar.version} {\1}]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-} else {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    fstar.version       20210824
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    fstar.release       devel
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+if {${subport} eq "fstar" || ${subport} eq "kremlin"} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    PortGroup               ocaml 1.1
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-foreach fname {fstar kremlin} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    set S [list subst -novariables]
</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;'>+                            port:gmake
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-    options ${fname}.home \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            ${fname}.bin \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            ${fname}.port \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            ${fname}.select_name \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            ${fname}.doc_dirs
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # Requires gmake 3.82+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    build.cmd               ${prefix}/bin/gmake
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-    default ${fname}.home        [{*}$S {${prefix}/libexec/[set fname]-${fstar.release}}]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    default ${fname}.bin         [{*}$S {[set fname]}]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    default ${fname}.port        [{*}$S {[set fname]${fstar.port_suffix}}]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    default ${fname}.select_name {${fstar.project}-${fstar.release}}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-}
</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;'>+    # Common configuration options that vary based on the subport (fstar vs kremlin)
</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:#ffe0e0;'>-# Provide generic alias options for the current subport
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-foreach key {home doc_dirs bin port select_name} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    set var "${fstar.project}.${key}"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    default fstar.subport.${key}    [subst -nocommands {[set ${var}]}]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        default ${fname}.home        [{*}$S {${prefix}/libexec/[set fname]}]
</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]}]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        default ${fname}.select_name {${subport}}
</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 "${subport}.${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:#ffe0e0;'>-# Common fstar/fstar-devel configuration
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-if {${fstar.project} eq "fstar"} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    github.project          FStar
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+subport fstar {    
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    github.setup            FStarLang FStar 356fb200d7e6a1d2ccc689073752400227160ba9
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    version                 2021.09.02
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    epoch                   1
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span>     license                 MIT
     description             General-purpose functional language aimed at program verification
     long_description        F* (pronounced F star) is a general-purpose \
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -88,205 +73,47 @@ if {${fstar.project} eq "fstar"} {
</span>                             be extracted to efficient OCaml, F#, C, WASM, or ASM \
                             code.
 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-    patchfiles              patch-z3-path
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    post-patch {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        # Fix up the z3 path in the generated code, too.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        #
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        # A patch file would be more of a headache here, as the autogenerated variable names
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        # result in the patches not applying cleanly across updates.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        reinplace {s|FStar_Platform.exe "z3"|FStar_String.op_Hat fstar_bin_directory (FStar_Platform.exe "/z3")|g} \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            src/ocaml-output/FStar_Options.ml
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        # Provide required link to z3 binary
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        ln -shf ${prefix}/libexec/z3-fstar/bin/z3 \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            ${worksrcpath}/bin/z3
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    checksums               rmd160  250761afdfbd099094a01d740789fb0c7d069855 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            sha256  391c4334c68c7cc13c9e01df83504569c6a07a7bb2ee62223d4237cac74f2363 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            size    8187909
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    github.tarball_from     archive
</span> 
     # destroot requires ginstall from coreutils
     depends_build-append    port:coreutils
<span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span>     depends_lib-append      port:z3-fstar \
                             port:gmp \
<span style='display:block; white-space:pre;background:#ffe0e0;'>-                            port:realpath
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    depends_run-append      port:fstar_select
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            port:realpath \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            port:ocaml-sedlex \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            port:ocaml-ppxlib
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    patchfiles              fstar/patch-z3-path \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            fstar/patch-fix-get_exec_dir \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            fstar/patch-tests_machine__integers_Makefile
</span> 
     fstar.doc_dirs          examples \
                             contrib \
                             tutorial
 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-# Common kremlin/kremlin-devel configuration
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-} elseif {${fstar.project} eq "kremlin"} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    github.project          kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    license                 Apache-2
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    description             A tool for extracting low-level F* programs to readable C code
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    long_description        KreMLin is a tool that extracts an F* program to readable C code.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    compiler.c_standard     2011
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    depends_run-append      port:kremlin_select
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    depends_build-append    port:gsed
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    depends_lib-append      port:${fstar.port} \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                            port:coreutils \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                            port:ocaml-fix \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                            port:ocaml-wasm \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                            port:ocaml-visitors
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    kremlin.bin             krml
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    kremlin.doc_dirs        examples
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    options                 kremlin.cc \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                            kremlin.ccpath
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    kremlin.ccpath          {${configure.compiler}}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    # XXX TODO: We really need a ${configure.compiler.family}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    if {[string match *clang* ${configure.compiler}]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        kremlin.cc clang
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    } elseif {[string match *gcc* ${configure.compiler}]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        kremlin.cc gcc
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    } else {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        # Assume GCC-like behavior
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        kremlin.cc gcc
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-} else {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    ui_error "Unsupported project: ${fstar.project}"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-# Subport-specific configuration
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-subport fstar {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    github.setup        ${github.author} ${github.project} ${fstar.version} V
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    revision            7
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    distname            V${version}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    checksums           rmd160  bec45d793880ecf815bdc3d79cdb58f7f6ba7414 \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        sha256  baa60f5f8a6c0dd5237a4fc7de5b8e940a3c620d680d255ae0057cf765163618 \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        size    7173479
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    patchfiles-append   fstar-stable/patch-ocaml4.08 \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        fstar-stable/patch-examples-fix-tests \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        fstar-stable/patch-fix-get_exec_dir
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    depends_lib-append  port:ocaml-ulex \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        port:ocaml-migrate-parsetree
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    build.args          PREFIX=${fstar.home}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    post-patch {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        # Fix-up paths to MacPorts' binaries
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        reinplace -E "s|@PREFIX@|${prefix}|g" \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            src/basic/ml/FStar_Util.ml
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    build {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        foreach {dir ftargets} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            src     {ocaml-fstar-ocaml}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            ulib    {install-fstarlib install-fstar-tactics all}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        } {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            build.dir       ${worksrcpath}/${dir}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            build.target    {*}${ftargets}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            do-build
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    destroot.dir        ${worksrcpath}/src/ocaml-output
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-subport fstar-devel {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    github.setup        ${github.author} ${github.project} b95d1ac83a18945266d3401acc0dcb3ce438108b
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    version             ${fstar.version}-[string range ${github.version} 0 6]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    revision            0
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    checksums           rmd160  5a9425b3267e68dd3151e43d737e29f0cd492992 \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        sha256  8c47e48d3b4ee97d2f0c672205af754087eca5d70be7776bbc7a81b58a318b8a \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        size    8168870
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    github.tarball_from archive
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    patchfiles-append   fstar-devel/patch-fix-get_exec_dir \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        fstar-devel/patch-tests_machine__integers_Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    depends_lib-append  port:ocaml-sedlex \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        port:ocaml-ppxlib
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    ocaml.package_dir   ${fstar.home}/bin
</span> 
     post-patch {
         # Fix-up paths to MacPorts' binaries
         reinplace -E "s|@PREFIX@|${prefix}|g" \
             src/basic/ml/FStar_Compiler_Util.ml
<span style='display:block; white-space:pre;background:#ffe0e0;'>-    }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-subport kremlin {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    github.setup        ${github.author} ${fstar.project} 0.9.6.0 v
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    revision            10
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-    distname            v${version}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    worksrcdir          kremlin-${version}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    # Updated z3 hints; can be generated after a valid test run via:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    #   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:#ffe0e0;'>-    distfiles-append    kremlin-stable/kremlin-${version}-test-hints.tar.xz
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    patchfiles-append   kremlin-stable/patch-clang-driver-options \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        kremlin-stable/patch-fstar-0.9.7.0 \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        kremlin-stable/patch-fstar-discover-path \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        kremlin-stable/patch-fix-make-command
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    github.tarball_from archive
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    checksums           rmd160  b806353b0dbc89ad4e398e14d332b36d9ea2f69a \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        sha256  547d3374e347d4e0b50bda2ed17a78719aa2265a91a2e1828a0e492e82dfb558 \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        size    660454
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    depends_lib-append  port:ocaml-ulex
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    # Disable known-broken test paths
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    if {${version} ne "0.9.6.0"} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        ui_error "Please verify that full test execution is still broken" 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    } else {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        patchfiles-append kremlin-stable/patch-disable-broken-tests
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        # Fix up the z3 path in the generated code, too.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        #
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        # A patch file would be more of a headache here, as the autogenerated variable names
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        # result in the patches not applying cleanly across updates.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        reinplace {s|FStar_Platform.exe "z3"|FStar_String.op_Hat fstar_bin_directory (FStar_Platform.exe "/z3")|g} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            src/ocaml-output/FStar_Options.ml
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-    post-patch {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        # Fix path to the fstar executable
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        reinplace {s|fstar\.exe|$(FSTAR_HOME)/bin/fstar|g} \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-             test/Makefile
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        # Provide required link to z3 binary
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        ln -shf ${prefix}/libexec/z3-fstar/bin/z3 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            ${worksrcpath}/bin/z3
</span>     }
<span style='display:block; white-space:pre;background:#ffe0e0;'>-}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-subport kremlin-devel {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    github.setup        ${github.author} ${fstar.project} 8d03c65f95fbc79b4f1fcfab1dc4c8f4f985d6d9
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    version             20210709-[string range ${github.version} 0 6]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    revision            0
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    checksums           rmd160  ae7b00b1c118ac9abed39ffcc2ef41427a61f630 \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        sha256  af26f369566fdcb0154f533dcd01d48c08bedb65551c04ce16fdf42dc3c41562 \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        size    895674
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    github.tarball_from archive
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    patchfiles-append   kremlin-devel/patch-clang-driver-options \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        kremlin-devel/patch-fstar-discover-path \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        kremlin-devel/patch-fstar-driver-no-lax \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        kremlin-devel/patch-kremlib-march-native \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        kremlin-devel/patch-test_system_system.h
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    depends_lib-append  port:ocaml-sedlex
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    depends_test-append port:ocaml-ctypes
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-# Apply shared fstar/fstar-devel subport configuration
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-if {${fstar.project} eq "fstar"} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    ocaml.package_dir   ${fstar.home}/bin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    test.run            yes
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    test.env            FSTAR_HOME=${worksrcpath} \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        KREMLIN_HOME=${kremlin.home}/home
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    test.dir            ${worksrcpath}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    test.target         all
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    test.args           -C examples \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        -j ${build.jobs}
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-    #
</span>     # XXX TODO:
     #
     # A number of F* test cases actually depend on KreMLin (while KreMLin depends
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -303,10 +130,16 @@ if {${fstar.project} eq "fstar"} {
</span>     #   - miniparse
     #   - tactics
     #   - typeclasses
<span style='display:block; white-space:pre;background:#ffe0e0;'>-    #
</span>     depends_test        port:${kremlin.port}
<span style='display:block; white-space:pre;background:#ffe0e0;'>-    destroot.args       PREFIX=${destroot}${fstar.home}
</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            FSTAR_HOME=${worksrcpath} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        KREMLIN_HOME=${kremlin.home}/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;'>+    destroot.args       PREFIX=${destroot}${fstar.home}
</span>     post-destroot {
         # Remove intermediate build directories
         foreach dir {ml tactics_ml} {
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -341,24 +174,66 @@ if {${fstar.project} eq "fstar"} {
</span>     }
 
     notes "
<span style='display:block; white-space:pre;background:#ffe0e0;'>-    To select fstar-${fstar.release} as your default F* toolchain, please run:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-      sudo port select fstar ${subport}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    To use your default F* toolchain with most standard Makefile-based F* projects,
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    To use this F* toolchain with most standard Makefile-based F* projects,
</span>     pass FSTAR_HOME to the build as either an environmental variable,
     or make(1) parameter:
 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-      FSTAR_HOME=\"${prefix}/libexec/fstar/home\"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    Alternatively, you may use fstar-${fstar.release} explicitly:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span>       FSTAR_HOME=\"${fstar.home}/home\"
 
     "
<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            FStarLang kremlin 3e502374c9afd018dcd062556eb02203dfad1923
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    version                 2021.08.24
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    epoch                   1
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</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;'>+    checksums               rmd160  38dd175b306f8a070e930c69e8eb956b52f20c9c \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            sha256  f5e9e3ad7a9bc48ba11669fe35da1da420f1776e51935234e0d49f597b319330 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            size    895587
</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;'>+    compiler.c_standard     2011
</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;'>+                            port:ocaml-sedlex
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</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;'>+    patchfiles              kremlin/patch-clang-driver-options \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            kremlin/patch-fstar-discover-path \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            kremlin/patch-fstar-driver-no-lax \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            kremlin/patch-kremlib-march-native \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            kremlin/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;'>+    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;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    options                 kremlin.cc \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                            kremlin.ccpath
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    kremlin.ccpath          {${configure.compiler}}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # XXX TODO: We really need a ${configure.compiler.family}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    if {[string match *clang* ${configure.compiler}]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        kremlin.cc clang
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    } elseif {[string match *gcc* ${configure.compiler}]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        kremlin.cc gcc
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    } else {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        # Assume GCC-like behavior
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        kremlin.cc gcc
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    }
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-# Apply shared kremlin/kremlin-devel subport configuration
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-} elseif {${fstar.project} eq "kremlin"} {
</span>     # If we specify PREFIX=${kremlin.home} in our build.args, a fixed path to
     # kremlin.home is hard-coded by kremlin's build system in AutoConfig.ml.
     #
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -428,79 +303,77 @@ if {${fstar.project} eq "fstar"} {
</span>     }
 
     notes "
<span style='display:block; white-space:pre;background:#ffe0e0;'>-    To select kremlin-${fstar.release} as your default KreMLin toolchain, please run:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-      sudo port select kremlin ${subport}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    To use your default KreMLin toolchain with most standard Makefile-based F*/KreMLin projects,
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    To use this KreMLin toolchain with most standard Makefile-based F*/KreMLin projects,
</span>     pass KREMLIN_HOME to the build as either an environmental variable,
     or make(1) parameter:
 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-      KREMLIN_HOME=\"${prefix}/libexec/kremlin/home\"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    Alternatively, you may use kremlin-${fstar.release} explicitly:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span>       KREMLIN_HOME=\"${kremlin.home}/home\"
 
     "
 }
 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-#
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-# Configure and register the subport's select file
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-#
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-select.group    ${fstar.project}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-select.file     ${workpath}/${fstar.project}-macports-select/${fstar.subport.select_name}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-post-patch {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    file mkdir [file dirname ${select.file}]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    copy -- ${filespath}/fstar-select.in \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        ${select.file}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    foreach {fstar_key fstar_var} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        @FSTAR_PROJECT@     fstar.project
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        @FSTAR_RELEASE@     fstar.release
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        @FSTAR_BIN@         fstar.subport.bin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    } {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        reinplace "s|${fstar_key}|[set ${fstar_var}]|g" \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            ${select.file}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+subport fstar-devel {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    PortGroup           obsolete 1.0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    version             20210824-b95d1ac
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    revision            1
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    replaced_by         fstar
</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;'>+    PortGroup           obsolete 1.0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    version             20210824-b95d1ac
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    revision            1
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    replaced_by         fstar
</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_select {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    PortGroup           obsolete 1.0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    version             1.3
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    revision            1
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span> 
<span style='display:block; white-space:pre;background:#e0ffe0;'>+subport kremlin_select {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    PortGroup           obsolete 1.0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    version             1.3
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    revision            1
</span> }
 
 #
 # Common destroot cleanup
 #
<span style='display:block; white-space:pre;background:#ffe0e0;'>-post-destroot {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    # Clean up the installed files.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    fs-traverse {f} ${destroot}${fstar.subport.home} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        switch -glob -- "[file tail $f] [file type $f]" {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            {*.checked file} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                # Bump the mtime of all *.checked files by 1 second.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                #
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                # This ensures that fstar/kremlin GNU make dependencies
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                # don't try to regenerate read-only *.checked files if they
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                # have an mtime identical to their corresponding fst/fsti
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                # input (yes, that happens)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                set mtime [file mtime $f]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                file mtime $f [expr {$mtime + 1}]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            {.gitignore file} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                # Delete .gitignore files
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                delete $f
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+if {${subport} eq "fstar" || ${subport} eq "kremlin"} {
</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:#ffe0e0;'>-    }
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-    # Add versioned documentation symlinks to share/doc/
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    xinstall -d -m 755 ${destroot}${prefix}/share/doc/${fstar.project}-${fstar.release}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    foreach doc_dir ${fstar.subport.doc_dirs} {
</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 -m 755 ${destroot}${prefix}/share/doc/${subport}
</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/${subport}/${doc_dir} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                ${destroot}${prefix}/share/doc/${subport}/${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>         ln -sf \
<span style='display:block; white-space:pre;background:#ffe0e0;'>-            ${fstar.subport.home}/share/${fstar.project}/${doc_dir} \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            ${destroot}${prefix}/share/doc/${fstar.project}-${fstar.release}/${doc_dir}
</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}
</span>     }
<span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    # Add a versioned symlink to bin/
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    ln -sf \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        ${fstar.subport.home}/bin/${fstar.subport.bin} \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        ${destroot}${prefix}/bin/${fstar.subport.bin}-${fstar.release} \
</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>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 31939107d85..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/files/fstar-select.in
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,3 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-libexec/@FSTAR_PROJECT@-@FSTAR_RELEASE@/bin/@FSTAR_BIN@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-share/doc/@FSTAR_PROJECT@-@FSTAR_RELEASE@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-libexec/@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/fstar-stable/patch-examples-fix-tests b/lang/fstar/files/fstar-stable/patch-examples-fix-tests
</span>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index bc66fb8907c..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/files/fstar-stable/patch-examples-fix-tests
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,12 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-diff -ru examples.orig/kv_parsing/Makefile examples/kv_parsing/Makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- examples.orig/kv_parsing/Makefile      2019-09-05 10:44:53.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ examples/kv_parsing/Makefile   2019-09-05 11:39:36.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -24,7 +24,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            EnumParsing.fst \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            VectorParsing.fst
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--FSTAR_INCLUDE_PATHS:=--include $(KREMLIN_HOME)/kremlib --include $(KREMLIN_HOME)/kremlib/compat
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+FSTAR_INCLUDE_PATHS:=--include $(KREMLIN_HOME)/kremlib
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- OTHERFLAGS+=$(FSTAR_INCLUDE_PATHS) --z3rlimit_factor 4
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/fstar-stable/patch-fix-get_exec_dir b/lang/fstar/files/fstar-stable/patch-fix-get_exec_dir
</span>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 276b1583bf7..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/files/fstar-stable/patch-fix-get_exec_dir
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,14 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- src/basic/ml/FStar_Util.ml.orig        2019-09-19 13:38:15.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ src/basic/ml/FStar_Util.ml     2019-09-19 13:38:23.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -841,7 +841,10 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let decr r = FStar_ST.(Z.(write r (read r - one)))
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let geq (i:int) (j:int) = i >= j
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--let get_exec_dir () = Filename.dirname (Sys.executable_name)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+let get_exec_dir () =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  (*  Unfortunately, OCaml does not expose realpath(3) *)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  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:#ffe0e0;'>-+  Filename.dirname (bin_path)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let expand_environment_variable x = try Some (Sys.getenv x) with Not_found -> None
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 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/fstar-stable/patch-ocaml4.08 b/lang/fstar/files/fstar-stable/patch-ocaml4.08
</span>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 4eacdccebfd..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/files/fstar-stable/patch-ocaml4.08
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,16 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- 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:#ffe0e0;'>-+++ src/tactics/ml/FStar_Tactics_Load.ml   2019-08-26 21:47:46.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -15,9 +15,11 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     | Unsafe_file -> "Unsafe_file"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     | Linking_error _ -> "Linking_error"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     | Corrupted_interface _ -> "Corrupted_interface"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--    | File_not_found _ -> "File_not_found"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--    | Cannot_open_dll _ -> "Cannot_open_dll"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    | Cannot_open_dynamic_library _ -> "Cannot_open_dynamic_library"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    | Library's_module_initializers_failed _ -> "Library's_module_initializers_failed"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     | Inconsistent_implementation _ -> "Inconsistent_implementation"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    | Module_already_loaded _ -> "Module_already_loaded"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    | Private_library_cannot_implement_interface _ -> "Private_library_cannot_implement_interface"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     in s ^ ": " ^ Dynlink.error_message e
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let find_taclib () =
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/fstar-devel/patch-fix-get_exec_dir b/lang/fstar/files/fstar/patch-fix-get_exec_dir
</span>similarity index 100%
rename from lang/fstar/files/fstar-devel/patch-fix-get_exec_dir
rename to lang/fstar/files/fstar/patch-fix-get_exec_dir
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/fstar-devel/patch-tests_machine__integers_Makefile b/lang/fstar/files/fstar/patch-tests_machine__integers_Makefile
</span>similarity index 100%
rename from lang/fstar/files/fstar-devel/patch-tests_machine__integers_Makefile
rename to lang/fstar/files/fstar/patch-tests_machine__integers_Makefile
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/patch-z3-path b/lang/fstar/files/fstar/patch-z3-path
</span>similarity index 100%
rename from lang/fstar/files/patch-z3-path
rename to lang/fstar/files/fstar/patch-z3-path
<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>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 313a06a5981..00000000000
</span>Binary files a/lang/fstar/files/kremlin-stable/kremlin-0.9.6.0-test-hints.tar.xz and /dev/null differ
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/kremlin-stable/patch-clang-driver-options b/lang/fstar/files/kremlin-stable/patch-clang-driver-options
</span>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 9fbf7111b83..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/files/kremlin-stable/patch-clang-driver-options
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,36 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- src/Options.ml.orig    2019-08-20 08:05:43.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ src/Options.ml 2019-09-09 11:04:27.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -24,7 +24,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let verbose = ref false
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let silent = ref false
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let exe_name = ref ""
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--let cc = ref "gcc"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+let cc = ref "clang"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let m32 = ref false
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let fsopts: string list ref = ref []
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let ccopts: string list ref = ref []
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -72,16 +72,21 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     "-ccopts";
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     "-Wall,-Werror,-Wno-unused-variable," ^
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     "-Wno-unknown-warning-option,-Wno-unused-but-set-variable," ^
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--    "-g,-fwrapv,-fstack-check,-D_BSD_SOURCE,-D_DEFAULT_SOURCE" ^
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    "-g,-fwrapv,-fstack-check" ^
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     (if Sys.os_type = "Win32" then ",-D__USE_MINGW_ANSI_STDIO" else "") ^
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     (if !parentheses then "" else ",-Wno-parentheses")
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   |] in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   let gcc_options = Array.append gcc_like_options
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--    [| "-ccopt"; if !c89_std then "-std=c89" else "-std=c11" |]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    [| "-ccopt"; if !c89_std then "-std=c89" else "-std=c11" |] in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  let clang_options = Array.append gcc_options
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  (* '-Winfinite-recursion' is triggered by the use of 'C.portable_exit'
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+   * in a recursive function; we need to disable this
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+   * warning until KreMLin adds support for the _Noreturn attribute *)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    [| "-ccopt"; "-Wno-error=infinite-recursion" |]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   [
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     "gcc", gcc_options;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--    "clang", gcc_options;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    "clang", clang_options;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     "g++", gcc_like_options;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     "compcert", [|
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-       "-warn-error"; "@6@8";
</span><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>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index e786c6c8228..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/files/kremlin-stable/patch-disable-broken-tests
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,26 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- test/Makefile.orig     2019-09-06 21:47:25.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ test/Makefile  2019-09-06 22:00:45.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -21,7 +21,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   LinkedList1.test LinkedList2.test LinkedList3.test LinkedList4.test \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   NoExtract.test InlineNoExtract.test ../book/RingBuffer.test \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   ../book/Introduction.test
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--CUSTOM            = count-uu
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+CUSTOM            =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- WASM_FILES        = \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   WasmTrap.wasm-test Wasm1.wasm-test Wasm2.wasm-test Wasm3.wasm-test Wasm4.wasm-test
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- NEGATIVE  = false
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -75,12 +75,11 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   touch $@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- $(OUTPUT_DIR)/%.exe: $(ALL_KRML_FILES) | $(KRML_BIN)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--  $(KRML) $(EXTRA) -tmpdir $(subst .exe,.out,$@) -no-prefix $(notdir $*) \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--    -o $@ $(filter %.krml,$^) -bundle $(subst _,.,$*)=WindowsHack,\*
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  @echo "\033[01;31m✘\033[00m: $<"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- .SECONDEXPANSION:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- %.test: $(OUTPUT_DIR)/$$(notdir $$(subst .,_,$$*)).exe
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--  @$^ && echo "\033[01;32m✔\033[00m [TEST,$*]" || (echo "\033[01;31m✘\033[00m [TEST,$*]" && false)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  @echo "\033[01;31m✘\033[00m [TEST,$*]"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # Various flags to be passed to some targets...
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- $(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>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index ecd33724f36..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/files/kremlin-stable/patch-fix-make-command
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,16 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- Makefile.orig  2019-09-13 12:46:52.602303000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ Makefile       2019-09-13 12:47:08.615444000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -33,11 +33,11 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- clean:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   rm -rf krml _build Tests.$(FLAVOR) Kremlin.$(FLAVOR)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--  make -C test clean
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  $(MAKE) -C test clean
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- test: all
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   ./Tests.native
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--  +make -C test
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  +$(MAKE) -C test
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # Auto-detection
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 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>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index c1818091c3f..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/files/kremlin-stable/patch-fstar-0.9.7.0
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,207 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-diff -ru include/kremlin/fstar_bytes.h.orig include/kremlin/fstar_bytes.h
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- include/kremlin/fstar_bytes.h  2019-08-30 16:45:01.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ include/kremlin/fstar_bytes.h  2019-08-30 16:47:20.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -76,6 +76,13 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   return b;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+typedef struct K___uint8_t_uint8_t_s
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+{
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  uint8_t fst;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  uint8_t snd;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+K___uint8_t_uint8_t;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- static inline FStar_Bytes_bytes FStar_Bytes_twobytes_(K___uint8_t_uint8_t *v) {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   char *data = KRML_HOST_MALLOC(2);
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   CHECK(data);
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -145,6 +152,13 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   return FStar_Bytes_utf8_encode(str);
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+typedef struct K___FStar_Bytes_bytes_FStar_Bytes_bytes_s
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+{
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  FStar_Bytes_bytes fst;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  FStar_Bytes_bytes snd;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+K___FStar_Bytes_bytes_FStar_Bytes_bytes;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- static inline void
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 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:#ffe0e0;'>-   dst->fst = FStar_Bytes_slice(bs, 0, i);
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -371,6 +385,18 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   return NULL;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+#define FStar_Pervasives_Native_None 0
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+#define FStar_Pervasives_Native_Some 1
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+typedef uint8_t FStar_Pervasives_Native_option__Prims_string_tags;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+typedef struct FStar_Pervasives_Native_option__Prims_string_s
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+{
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  FStar_Pervasives_Native_option__Prims_string_tags tag;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  Prims_string v;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+FStar_Pervasives_Native_option__Prims_string;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- static inline void
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- FStar_Bytes_iutf8_opt_(FStar_Bytes_bytes b, FStar_Pervasives_Native_option__Prims_string *ret) {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   char *str = KRML_HOST_MALLOC(b.length + 1);
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-diff -ru kremlib/TestLib.fsti.orig kremlib/TestLib.fsti
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- kremlib/TestLib.fsti.orig      2019-08-30 17:29:18.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ kremlib/TestLib.fsti   2019-08-30 17:29:21.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -43,7 +43,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-       /\ is_eternal_region (frameOf b)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-       /\ HyperStack.modifies (Set.singleton (frameOf b)) h0 h1
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-       /\ HyperStack.modifies_ref (frameOf b) (Set.empty) h0 h1
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--      /\ (FStar.HyperStack.(Map.domain h0.h == Map.domain h1.h)))
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+      /\ (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:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- (** Prints: "got error code %d" where %d is the first argument *)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- val perr: FStar.UInt32.t -> Stack unit
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- book/LowStar.fst.orig  2019-08-30 17:41:49.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ book/LowStar.fst       2019-08-30 17:55:20.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -602,8 +602,8 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- /// ``ST.equal_domains`` predicate.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let equal_domains (m0 m1: HS.mem) =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--  m0.HS.tip == m1.HS.tip /\
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--  Set.equal (Map.domain m0.HS.h) (Map.domain m1.HS.h) /\
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  (HS.get_tip m0) == (HS.get_tip m1) /\
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  Set.equal (Map.domain (HS.get_hmap m0)) (Map.domain (HS.get_hmap m1)) /\
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   ST.same_refs_in_all_regions m0 m1
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- /// The ``equal_domains`` predicate states that a function in the ``Stack`` effect:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -625,14 +625,14 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- /// .. note::
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ///
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--///    The following examples use the ``[@ fail ]`` F* attribute. Remember that
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+///    The following examples use the ``[@ expect_failure ]`` F* attribute. Remember that
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ///    this tutorial is a valid F* file, which we put under continuous
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ///    integration and version control. This attribute merely indicates to F*
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ///    that the failure is intentional.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ///
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- /// Based on the knowledge above, consider the following failing function.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--[@ fail ]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+[@ expect_failure ]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let g (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   let b = Buffer.create 0ul 8ul in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   ()
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -653,7 +653,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ///
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- /// We can attempt to fix ``g`` by adding a call to ``push_frame``.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--[@ fail ]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+[@ expect_failure ]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let g2 (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   push_frame ();
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   let b = Buffer.create 0ul 8ul in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -702,7 +702,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let test_st_get (): St unit =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   push_frame ();
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   let m = ST.get () in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--  assert (Monotonic.HyperStack.is_stack_region m.HS.tip);
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  assert (Monotonic.HyperStack.is_stack_region (HS.get_tip m));
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   pop_frame ()
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- /// These are the basic building blocks of our memory model. Verifying on top of
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -867,7 +867,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- /// 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:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--[@ fail ]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+[@ expect_failure ]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let test_sub_error (): St unit =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   let b = Buffer.rcreate_mm HS.root 0UL 8ul in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   let b_l = Buffer.sub b 0ul 4ul in // idx = 0; length = 4
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- test/ML16.fst.orig     2019-08-30 17:57:28.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ test/ML16.fst  2019-08-30 17:57:47.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -20,7 +20,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let test2 (_: unit):
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   StackInline (Buffer.buffer Int32.t)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--  (requires (fun h0 -> is_stack_region h0.tip))
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  (requires (fun h0 -> is_stack_region (FStar.HyperStack.get_tip h0)))
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   (ensures (fun h0 b h1 -> live h1 b /\ Buffer.length b = 2))
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   let b = Buffer.create 0l 2ul in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- test/StringLit.fst.orig        2019-08-30 17:58:58.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ test/StringLit.fst     2019-08-30 17:59:36.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -5,10 +5,10 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- open FStar.HyperStack.ST
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let test (x:string): Stack string (fun _ -> true) (fun _ _ _ -> true) =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--  FStar.String.strcat "hello " x
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  strcat "hello " x
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let cat (x y:string): Stack string (fun _ -> true) (fun _ _ _ -> true) =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--  FStar.String.strcat x y
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  strcat x y
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let main () =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   // C strings, modeled as zero-terminated, not relying on GC
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- runtime/WasmSupport.fst.orig   2019-08-30 18:12:21.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ runtime/WasmSupport.fst        2019-08-30 18:13:19.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -30,6 +30,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- (* TODO: all of these functions are copy-pastes from whatever is written in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-  * kremlib.h. They OUGHT TO BE implement in F*! *)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+#set-options "--lax"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let eq_mask64 (x y: U64.t) =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   let open FStar.UInt64 in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   let x = lognot (logxor x y) in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- test/Inline.fst.orig   2019-08-30 18:13:52.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ test/Inline.fst        2019-08-30 18:14:16.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -8,7 +8,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- module I32 = FStar.Int32
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let alloc_and_init (i: Int32.t): StackInline (Buffer.buffer Int32.t)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--  (requires (fun h0 -> FStar.Int.size (I32.v i) 16 /\ is_stack_region h0.tip))
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  (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:#ffe0e0;'>-     // JP: why do I have to manually write the hypothesis above?
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   (ensures (fun h0 b h1 ->
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     let open FStar.Buffer in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- test/DataTypes.fst.orig        2019-08-30 18:18:21.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ test/DataTypes.fst     2019-08-30 18:18:38.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -4,10 +4,12 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- open FStar.HyperStack.ST
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- open FStar.Ghost
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+noeq
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- type t =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   | A: a:UInt32.t -> b:UInt64.t -> t
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   | B: c:UInt8.t -> d:UInt8.t -> e:erased UInt8.t -> t
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+noeq
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- type u =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   | C: f:UInt32.t -> g:UInt64.t -> u
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   | D: h:t -> i:unit -> u
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- test/Makefile  2019-08-30 22:09:45.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ test/Makefile  2019-08-30 22:42:02.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -62,8 +62,10 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- $(HINTS_DIR):
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   mkdir -p $@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+$(CACHE_DIR)/FStar.ModifiesGen.fst.checked: FSTAR+=--z3rlimit_factor 4
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- $(CACHE_DIR)/%.checked: | .depend $(HINTS_DIR)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--  $(FSTAR) --hint_file $(HINTS_DIR)/$*.hints $<
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  $(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:#ffe0e0;'>-   touch $@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- $(OUTPUT_DIR)/%.krml: | .depend
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -72,9 +74,9 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     $(notdir $(subst .checked,,$<))
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   touch $@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--$(OUTPUT_DIR)/%.exe: $(OUTPUT_DIR)/FStar_UInt128.krml | $(KRML_BIN)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+$(OUTPUT_DIR)/%.exe: $(ALL_KRML_FILES) | $(KRML_BIN)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   $(KRML) $(EXTRA) -tmpdir $(subst .exe,.out,$@) -no-prefix $(notdir $*) \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--    -o $@ $^
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    -o $@ $(filter %.krml,$^) -bundle $(subst _,.,$*)=WindowsHack,\*
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- .SECONDEXPANSION:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- %.test: $(OUTPUT_DIR)/$$(notdir $$(subst .,_,$$*)).exe
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/kremlin-stable/patch-fstar-discover-path b/lang/fstar/files/kremlin-stable/patch-fstar-discover-path
</span>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 21838d2c851..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/files/kremlin-stable/patch-fstar-discover-path
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,90 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- src/Driver.ml  2019-10-28 15:51:04.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ src/Driver.ml  2019-10-28 15:52:24.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -49,6 +49,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let fstar_options = ref []
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- (** By [detect_kremlin] *)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+let bin_dir = ref ""
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let kremlib_dir = ref ""
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let runtime_dir = ref ""
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let include_dir = ref ""
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -121,6 +122,16 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- let detect_kremlin () =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   detect_base_tools_if ();
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  let real_krml =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    let me = Sys.argv.(0) in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    if Sys.os_type = "Win32" && not (Filename.is_relative me) then
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+      me
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    else
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+      try read_one_line !readlink [| "-f"; read_one_line "which" [| me |] |]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+      with _ -> fatal_error "Could not compute full krml path"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  bin_dir := Filename.dirname (real_krml);
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   if AutoConfig.kremlib_dir <> "" then begin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     kremlib_dir := AutoConfig.kremlib_dir;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     runtime_dir := AutoConfig.runtime_dir;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -130,19 +141,11 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     KPrint.bprintf "%sKreMLin called via:%s %s\n" Ansi.underline Ansi.reset Sys.argv.(0);
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--    let real_krml =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--      let me = Sys.argv.(0) in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--      if Sys.os_type = "Win32" && not (Filename.is_relative me) then
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--        me
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--      else
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--        try read_one_line !readlink [| "-f"; read_one_line "which" [| me |] |]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--        with _ -> fatal_error "Could not compute full krml path"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--    in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     (* ../_build/src/Kremlin.native *)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     KPrint.bprintf "%sthe Kremlin executable is:%s %s\n" Ansi.underline Ansi.reset real_krml;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     let krml_home =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--      try read_one_line !readlink [| "-f"; d real_krml ^^ ".." ^^ ".." |]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+      try read_one_line !readlink [| "-f"; d real_krml ^^ ".." |]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-       with _ -> fatal_error "Could not compute krml_home"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     KPrint.bprintf "%sKreMLin home is:%s %s\n" Ansi.underline Ansi.reset krml_home;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -154,10 +157,18 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-       Sys.chdir cwd
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     end;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--    kremlib_dir := krml_home ^^ "kremlib";
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--    runtime_dir := krml_home ^^ "runtime";
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--    include_dir := krml_home ^^ "include";
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--    misc_dir := krml_home ^^ "misc"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    if try Sys.is_directory (krml_home ^^ "kremlib") with Sys_error _ -> false; then begin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+      KPrint.bprintf "Detected source layout in KreMLin home\n";
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+      kremlib_dir := krml_home ^^ "kremlib";
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+      runtime_dir := krml_home ^^ "runtime";
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+      include_dir := krml_home ^^ "include";
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+      misc_dir := krml_home ^^ "misc"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    end else begin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+      kremlib_dir := krml_home ^^ "lib" ^^ "kremlin";
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+      runtime_dir := !kremlib_dir ^^ "runtime";
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+      include_dir := krml_home ^^ "include";
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+      misc_dir := krml_home ^^ "share" ^^ "kremlin" ^^ "misc"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    end;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   end;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -188,11 +199,15 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     fstar_home := r;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     fstar := r ^^ "bin" ^^ "fstar.exe"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   with Not_found -> try
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--    fstar := read_one_line "which" [| "fstar.exe" |];
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    let real_fstar =
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+      try read_one_line !readlink [| "-f"; !bin_dir ^^ "fstar" |]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+      with _ -> fatal_error "Could not compute full fstar path"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    in
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    fstar := real_fstar;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-     fstar_home := d (d !fstar);
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--    KPrint.bprintf "FSTAR_HOME is %s (via fstar.exe in PATH)\n" !fstar_home
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    KPrint.bprintf "FSTAR_HOME is %s\n" !fstar_home
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   with _ ->
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--    fatal_error "Did not find fstar.exe in PATH and FSTAR_HOME is not set"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+    fatal_error "Did not find fstar in %s and FSTAR_HOME is not set" !bin_dir
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   end;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   if KString.exists !fstar_home "opam"; then begin
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/kremlin-devel/patch-clang-driver-options b/lang/fstar/files/kremlin/patch-clang-driver-options
</span>similarity index 100%
rename from lang/fstar/files/kremlin-devel/patch-clang-driver-options
rename to lang/fstar/files/kremlin/patch-clang-driver-options
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/kremlin-devel/patch-fstar-discover-path b/lang/fstar/files/kremlin/patch-fstar-discover-path
</span>similarity index 100%
rename from lang/fstar/files/kremlin-devel/patch-fstar-discover-path
rename to lang/fstar/files/kremlin/patch-fstar-discover-path
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/kremlin-devel/patch-fstar-driver-no-lax b/lang/fstar/files/kremlin/patch-fstar-driver-no-lax
</span>similarity index 100%
rename from lang/fstar/files/kremlin-devel/patch-fstar-driver-no-lax
rename to lang/fstar/files/kremlin/patch-fstar-driver-no-lax
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/kremlin-devel/patch-kremlib-march-native b/lang/fstar/files/kremlin/patch-kremlib-march-native
</span>similarity index 100%
rename from lang/fstar/files/kremlin-devel/patch-kremlib-march-native
rename to lang/fstar/files/kremlin/patch-kremlib-march-native
<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/patch-test_system_system.h
</span>similarity index 100%
rename from lang/fstar/files/kremlin-devel/patch-test_system_system.h
rename to lang/fstar/files/kremlin/patch-test_system_system.h
<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>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index d4578c26b4a..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/files/patch-no-install-checked
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,11 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- src/ocaml-output/Makefile.orig 2019-08-30 21:34:00.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ src/ocaml-output/Makefile      2019-08-30 21:34:24.000000000 -0600
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -182,7 +182,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # permissions and creating directories on the fly as needed.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # (JP: the package version of this command is based on git but for OPAM
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- #  installs we cannot assume the user has git installed.)
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--install_dir = cd ../../$(1) && find . -type f -exec $(INSTALL_EXEC) -m 644 -D {} $(PREFIX)/$(2)/{} \;
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+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:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # install the standard library binary files
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 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/ocaml/ocaml-hacl-star/Portfile b/ocaml/ocaml-hacl-star/Portfile
</span><span style='display:block; white-space:pre;color:#808080;'>index db7e10afde3..a092dfd9d99 100644
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/ocaml/ocaml-hacl-star/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/ocaml/ocaml-hacl-star/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -7,6 +7,7 @@ PortGroup ocaml     1.1
</span> name                ocaml-hacl-star
 github.setup        project-everest hacl-star 4b197eb54b41056e6c051f0162cf57a50ad5b380
 version             20210824-[string range ${github.version} 0 6]
<span style='display:block; white-space:pre;background:#e0ffe0;'>+revision            1
</span> 
 categories          ocaml devel security
 maintainers         {landonf @landonf} openmaintainer
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -57,8 +58,8 @@ depends_build       port:gmake \
</span>                     port:gtime \
                     port:gsed
 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-depends_lib         port:fstar-devel \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                    port:kremlin-devel
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+depends_lib         port:fstar \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                    port:kremlin
</span> 
 # Required to build the ocaml-hacl-star bindings
 subport ocaml-hacl-star-raw {
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -69,8 +70,8 @@ subport ocaml-hacl-star-raw {
</span> 
     # Common make arguments
     hacl-star.make_args HACL_HOME="${worksrcpath}" \
<span style='display:block; white-space:pre;background:#ffe0e0;'>-                        FSTAR_HOME="${prefix}/libexec/fstar-devel/home" \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                        KREMLIN_HOME="${prefix}/libexec/kremlin-devel/home" \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        FSTAR_HOME="${prefix}/libexec/fstar/home" \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                        KREMLIN_HOME="${prefix}/libexec/kremlin/home" \
</span>                         VALE_HOME="${worksrcpath}/${vale.distname}" \
                         OPENSSL_HOME="${prefix}/lib"
 
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/sysutils/fstar_select/Portfile b/sysutils/fstar_select/Portfile
</span>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 360f6524f88..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/sysutils/fstar_select/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,63 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-# -*- 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:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-PortSystem          1.0
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-PortGroup           select 1.0
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-name                fstar_select
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-version             1.3
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-categories          sysutils lang
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-platforms           darwin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-maintainers         {landonf @landonf} openmaintainer
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-license             BSD
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-supported_archs     noarch
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-description         common files for selecting default fstar version
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-long_description \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    fstar_select installs files that allow 'port select' to switch the \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    default F* compiler. It creates unsuffixed symlinks in the \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    MacPorts prefix that point to the selected version.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-homepage            https://fstar-lang.org
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-distfiles
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-use_configure       no
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-options fstar.project \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        fstar.bin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-fstar.project       fstar
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-fstar.bin           fstar
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-subport kremlin_select {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    description         common files for selecting default kremlin version
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    long_description \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        kremlin_select installs files that allow 'port select' to switch the \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        default KreMLin compiler. It creates unsuffixed symlinks in the \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        MacPorts prefix that point to the selected version.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    fstar.project   kremlin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    fstar.bin       krml
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-build {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    file mkdir ${worksrcpath}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    copy -- ${filespath}/base.in \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        ${worksrcpath}/base
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    foreach {fstar_key fstar_var} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        @FSTAR_PROJECT@     fstar.project
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        @FSTAR_BIN@         fstar.bin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    } {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        reinplace "s|${fstar_key}|[set ${fstar_var}]|g" \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-            ${worksrcpath}/base
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-destroot {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    select::install ${fstar.project} ${worksrcpath}/base
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    select::install ${fstar.project} ${filespath}/none
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-livecheck.type      none
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/sysutils/fstar_select/files/base.in b/sysutils/fstar_select/files/base.in
</span>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 313e7111fe5..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/sysutils/fstar_select/files/base.in
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,3 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-bin/@FSTAR_BIN@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-share/doc/@FSTAR_PROJECT@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-libexec/@FSTAR_PROJECT@
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/sysutils/fstar_select/files/none b/sysutils/fstar_select/files/none
</span>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index fc9c24676eb..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/sysutils/fstar_select/files/none
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,3 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--
</span></pre><pre style='margin:0'>

</pre>