<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/e2a643d8fbf8885fb25eac0ec9f831c09628c4cb">https://github.com/macports/macports-ports/commit/e2a643d8fbf8885fb25eac0ec9f831c09628c4cb</a></p>
<pre style="white-space: pre; background: #F8F8F8">The following commit(s) were added to refs/heads/master by this push:
<span style='display:block; white-space:pre;color:#404040;'> new e2a643d kremlin(-devel): Add automatic discovery of fstar, and provide 'runtime' and 'include' compatibility symlinks
</span>e2a643d is described below
<span style='display:block; white-space:pre;color:#808000;'>commit e2a643d8fbf8885fb25eac0ec9f831c09628c4cb
</span>Author: Landon Fuller <landonf@macports.org>
AuthorDate: Fri Oct 25 12:38:40 2019 -0600
<span style='display:block; white-space:pre;color:#404040;'> kremlin(-devel): Add automatic discovery of fstar, and provide 'runtime' and 'include' compatibility symlinks
</span>---
lang/fstar/Portfile | 12 +++++--
.../files/kremlin-devel/patch-fstar-discover-path | 39 ++++++++++++++++++++++
.../files/kremlin-stable/patch-fstar-discover-path | 38 +++++++++++++++++++++
3 files changed, 86 insertions(+), 3 deletions(-)
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/Portfile b/lang/fstar/Portfile
</span><span style='display:block; white-space:pre;color:#808080;'>index 89fa43d..b4a7a7e 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;'>@@ -179,7 +179,7 @@ subport fstar-devel {
</span>
subport kremlin {
github.setup ${github.author} ${fstar.project} 0.9.6.0 v
<span style='display:block; white-space:pre;background:#ffe0e0;'>- revision 6
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ revision 7
</span>
distname v${version}
worksrcdir kremlin-${version}
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -188,6 +188,7 @@ subport kremlin {
</span> # tar -Jcf files/kremlin-0.9.6.0-test-hints.tar.xz -C work kremlin-0.9.6.0/test/.hints
distfiles-append kremlin-stable/kremlin-${version}-test-hints.tar.xz
patchfiles-append kremlin-stable/patch-fstar-0.9.7.0 \
<span style='display:block; white-space:pre;background:#e0ffe0;'>+ kremlin-stable/patch-fstar-discover-path \
</span> kremlin-stable/patch-fix-make-command
github.tarball_from archive
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -215,13 +216,14 @@ subport kremlin {
</span> subport kremlin-devel {
github.setup ${github.author} ${fstar.project} e324b7e63e24d0822e753051b9dc7f7ab294bc00
version ${fstar.version}-[string range ${github.version} 0 6]
<span style='display:block; white-space:pre;background:#ffe0e0;'>- revision 1
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ revision 2
</span>
checksums rmd160 b02e8630d700b8065bd83f3938bf5806d74e4d22 \
sha256 be69d4ae8d7f0f38675addc29bf4dae4879805dfe94abba41b3d81a6e2829999 \
size 739359
patchfiles-append kremlin-devel/patch-fix-make-command \
<span style='display:block; white-space:pre;background:#e0ffe0;'>+ kremlin-devel/patch-fstar-discover-path \
</span> kremlin-devel/patch-test_system_system.h
depends_lib-append port:ocaml-sedlex
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -340,19 +342,23 @@ if {${fstar.project} eq "fstar"} {
</span> }
post-destroot {
<span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Provide a link to our fstar binary
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ln -shf ${fstar.home}/bin/${fstar.bin} ${destroot}${kremlin.home}/bin/${fstar.bin}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span> # Provide compatibility symlinks for projects that expect KreMLin's
# source layout
set kremlin_compat_home ${destroot}${kremlin.home}/home
xinstall -d -m 755 ${kremlin_compat_home}
foreach {kremlin_src kremlin_dest} {
lib/kremlin kremlib
<span style='display:block; white-space:pre;background:#e0ffe0;'>+ lib/kremlin/runtime runtime
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ include include
</span> bin/krml krml
share/kremlin/misc misc
} {
ln -shf \
../${kremlin_src} \
${kremlin_compat_home}/${kremlin_dest}
<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/kremlin-devel/patch-fstar-discover-path b/lang/fstar/files/kremlin-devel/patch-fstar-discover-path
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 0000000..ce56033
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/kremlin-devel/patch-fstar-discover-path
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,39 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- src/Driver.ml.orig 2019-10-25 11:40:03.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ src/Driver.ml 2019-10-25 12:08:59.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -52,6 +52,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let fstar_options = ref []
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ (** By [detect_kremlin] *)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++let bin_dir = ref ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let kremlib_dir = ref ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let runtime_dir = ref ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let include_dir = ref ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -145,6 +146,8 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let detect_kremlin () =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ detect_base_tools_if ();
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ bin_dir := Filename.dirname (Sys.executable_name);
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if AutoConfig.kremlib_dir <> "" then begin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ kremlib_dir := AutoConfig.kremlib_dir;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ runtime_dir := AutoConfig.runtime_dir;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -221,12 +224,16 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ fstar_home := r;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ fstar := r ^^ "bin" ^^ "fstar.exe"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ with Not_found -> try
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+- fstar := read_one_line "which" [| "fstar.exe" |];
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ let real_fstar =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ try read_one_line !readlink [| "-f"; !bin_dir ^^ "fstar" |]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ with _ -> fatal_error "Could not compute full fstar path"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ fstar := real_fstar;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ fstar_home := d (d !fstar);
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if not !Options.silent then
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+- KPrint.bprintf "FSTAR_HOME is %s (via fstar.exe in PATH)\n" !fstar_home
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ KPrint.bprintf "FSTAR_HOME is %s\n" !fstar_home
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ with _ ->
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+- fatal_error "Did not find fstar.exe in PATH and FSTAR_HOME is not set"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ 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:#e0ffe0;'>+ end;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 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-stable/patch-fstar-discover-path b/lang/fstar/files/kremlin-stable/patch-fstar-discover-path
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 0000000..b12dec6
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/kremlin-stable/patch-fstar-discover-path
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,38 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- src/Driver.ml.orig 2018-05-17 14:40:16.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ src/Driver.ml 2019-10-25 12:26:07.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -49,6 +49,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let fstar_options = ref []
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ (** By [detect_kremlin] *)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++let bin_dir = ref ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let kremlib_dir = ref ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let runtime_dir = ref ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let include_dir = ref ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -121,6 +122,8 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ let detect_kremlin () =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ detect_base_tools_if ();
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ bin_dir := Filename.dirname (Sys.executable_name);
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if AutoConfig.kremlib_dir <> "" then begin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ kremlib_dir := AutoConfig.kremlib_dir;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ runtime_dir := AutoConfig.runtime_dir;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -188,11 +191,15 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ fstar_home := r;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ fstar := r ^^ "bin" ^^ "fstar.exe"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ with Not_found -> try
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+- fstar := read_one_line "which" [| "fstar.exe" |];
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ let real_fstar =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ try read_one_line !readlink [| "-f"; !bin_dir ^^ "fstar" |]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ with _ -> fatal_error "Could not compute full fstar path"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ fstar := real_fstar;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ fstar_home := d (d !fstar);
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+- KPrint.bprintf "FSTAR_HOME is %s (via fstar.exe in PATH)\n" !fstar_home
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ KPrint.bprintf "FSTAR_HOME is %s\n" !fstar_home
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ with _ ->
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+- fatal_error "Did not find fstar.exe in PATH and FSTAR_HOME is not set"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ 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:#e0ffe0;'>+ end;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if KString.exists !fstar_home "opam"; then begin
</span></pre><pre style='margin:0'>
</pre>