From 552ca5a00e94d977bd7aff922a59ecf7b30784d8 Mon Sep 17 00:00:00 2001 From: Bart Jacobs Date: Tue, 5 Dec 2017 14:17:18 +0100 Subject: [PATCH] Upgrade Windows build The Windows build now uses OCaml 4.06.0 and furthermore is now ready to start using Z3 4.5.0. --- make_vfdeps_win32/Makefile | 5 +- make_vfdeps_win32/pkg-config | 3 +- setup-windows.bat | 1 - setup-windows.sh | 102 ++--------------------------------- src/GNUmakefile | 8 +-- src/linemarks/Makefile | 8 +-- src/win/GNUmakefile | 3 +- src/win/Stopwatch.ml | 16 ++++++ 8 files changed, 30 insertions(+), 116 deletions(-) create mode 100644 src/win/Stopwatch.ml diff --git a/make_vfdeps_win32/Makefile b/make_vfdeps_win32/Makefile index c478f4842..281ddc160 100644 --- a/make_vfdeps_win32/Makefile +++ b/make_vfdeps_win32/Makefile @@ -167,7 +167,10 @@ $(GTK_BINARY): ftp://ftp.gnome.org/pub/gnome/binaries/win32/dependencies/libxml2-dev_2.9.0-1_win32.zip \ ; do \ download_and_unzip --dlcache "$(MAKEDIR)" "$$url" \ - ; done + ; done && \ + mv bin/pkg-config.exe bin/pkg-config.exe_ && \ + cp "$(MAKEDIR)/pkg-config" bin && \ + mv bin/pkg-config.exe_ bin/pkg-config.exe gtk: $(GTK_BINARY) .PHONY: gtk diff --git a/make_vfdeps_win32/pkg-config b/make_vfdeps_win32/pkg-config index aedbf7665..a3cd50ac1 100644 --- a/make_vfdeps_win32/pkg-config +++ b/make_vfdeps_win32/pkg-config @@ -1,3 +1,4 @@ #!/bin/bash set -o pipefail # A pipe fails if any component fails -/cygdrive/c/vfdeps-17.12/bin/pkg-config $* | dos2unix +DIRNAME=`dirname "$0"` +"$DIRNAME/pkg-config.exe" $* | conv --dos2unix diff --git a/setup-windows.bat b/setup-windows.bat index dfd133e19..c00be77c8 100644 --- a/setup-windows.bat +++ b/setup-windows.bat @@ -15,4 +15,3 @@ bitsadmin.exe /transfer "cygwin" https://cygwin.com/setup-x86.exe %TEMP%\setup-c echo none /cygdrive cygdrive binary,posix=0,user,noacl 0 0 > c:\cygwin\etc\fstab || exit /b c:\cygwin\bin\bash -lc "cd /cygdrive/c/projects/verifast && bash setup-windows.sh" || exit /b -copy /y c:\gtk\bin\zlib1.dll c:\projects\verifast\bin diff --git a/setup-windows.sh b/setup-windows.sh index c94da8813..f67374e71 100644 --- a/setup-windows.sh +++ b/setup-windows.sh @@ -1,13 +1,6 @@ #!/bin/bash # Installs OCaml and lablgtk on Windows. Called by setup-windows.bat. -# -# This script depends on (these dependencies are installed by setup-windows.bat): -# - cygwin -# - wget, 7z -# - curl,make,mingw64-i686-gcc-g++,mingw64-i686-gcc-core,mingw64-i686-gcc,patch,rlwrap,libreadline6,diffutils,wget (choosen by ocaml installer) -# - dos2unix -# - mingw64-i686-binutils (for "ar.exe", used by vfide's makefile) dl_and_unzip(){ url="$1" @@ -25,96 +18,7 @@ set -x # Print what is being executed. cd /cygdrive/c -# Ocaml -# -# The .exe OCaml installer needs GUI interaction and is thus not scriptable, -# so we extract the files and set up the config by hand. -# -# If you want to do this by hand, you can instead of executing these commands, -# just launch the .exe and keep clicking "Next". -mkdir -p OCaml -cd OCaml -wget --progress=dot:mega -c http://gallium.inria.fr/~protzenk/caml-installer/ocaml-4.02.3-i686-mingw64-installer4.exe -echo "64cfe42bd15d059cb3ad2916bfa234b555f1d355 *ocaml-4.02.3-i686-mingw64-installer4.exe" | sha1sum -c || exit 1 -7z -y x ocaml-4.02.3-i686-mingw64-installer4.exe bin/ lib/ -chmod +x bin/* -chmod a+rx lib lib/ lib/stublibs lib/stublibs/* -mkdir -p etc -cat << EOF > etc/findlib.conf -destdir="C:\\\\OCaml\\\\lib\\\\site-lib" -path="C:\\\\OCaml\\\\lib\\\\site-lib" -stdlib="C:\\\\OCaml\\\\lib" -ldconf="C:\\\\OCaml\\\\lib\\\\ld.conf" -ocamlc="ocamlc.opt" -ocamlopt="ocamlopt.opt" -ocamldep="ocamldep.opt" -ocamldoc="ocamldoc.opt" -EOF -echo 'C:\OCaml\lib' > lib/ld.conf -echo 'C:\OCaml\lib\stublibs' >> lib/ld.conf -echo 'export PATH="$PATH:/cygdrive/c/OCaml/bin"' >> ~/.bash_profile - export PATH="$PATH:/cygdrive/c/OCaml/bin" -echo "export OCAMLFIND_CONF='C:\OCaml\etc\findlib.conf'" >> ~/.bash_profile - export OCAMLFIND_CONF='C:\OCaml\etc\findlib.conf' -echo "export OCAMLLIB='C:\OCaml\lib'" >> ~/.bash_profile - export OCAMLLIB='C:\OCaml\lib' -cd .. +dl_and_unzip http://www.cs.kuleuven.be/~bartj/verifast/vfdeps-17.12-win32.zip 9046d38717c0de448a2d454e7186443edd342dd6 - -# GTK -mkdir -p gtk -cd gtk -dl_and_unzip \ - ftp://ftp.gnome.org/pub/gnome/binaries/win32/gtk+/2.24/gtk+-bundle_2.24.10-20120208_win32.zip \ - 895072c22f5bfd4ac9054d48d62d6c8b2a487098 -cd .. - -# Gtksourceview -cd gtk -dl_and_unzip \ - ftp://ftp.gnome.org/pub/gnome/binaries/win32/gtksourceview/2.10/gtksourceview-2.10.0.zip \ - 9d04bdeb86ed8358e250394a35e389680b5c8bf5 -dl_and_unzip \ - ftp://ftp.gnome.org/pub/gnome/binaries/win32/gtksourceview/2.10/gtksourceview-dev-2.10.0.zip \ - 2accab71c2c4b6bae91453e5428a7ef37a45fbe3 -dl_and_unzip \ - ftp://ftp.gnome.org/pub/gnome/binaries/win32/dependencies/libxml2_2.9.0-1_win32.zip \ - a7961070b8a954c36041b7cc1948213a5195f043 -dl_and_unzip \ - ftp://ftp.gnome.org/pub/gnome/binaries/win32/dependencies/libxml2-dev_2.9.0-1_win32.zip \ - 6bedf32091e78764c2121db63b6927967c9e4844 -cd .. - -# LablGTK -wget -c http://forge.ocamlcore.org/frs/download.php/1261/lablgtk-2.18.3.tar.gz -echo "c76a7ae9454e89365666cf19728dbb51edb6810e2e57032b3bebd53ccec5946e *lablgtk-2.18.3.tar.gz" | sha256sum -c || exit 1 -tar -xzf lablgtk-2.18.3.tar.gz -mv lablgtk-2.18.0 lablgtk-2.18.3 # Bug in lablgtk-2.18.3.tar.gz: the directory is still called lablgtk-2.18.0 -cd lablgtk-2.18.3 -# Problem: the pkg-config program that ships with Gtk produces CRLF-terminated -# lines. The Cygwin tools choke on this. -# Solution: create a wrapper that transforms the DOS lines to Unix lines using -# Cygwin's "conv --dos2unix" or dos2unix program: -cat << EOF > pkg-config -#!/bin/bash -set -o pipefail # A pipe fails if any component fails -/cygdrive/c/gtk/bin/pkg-config \$* | dos2unix -EOF -chmod +x pkg-config -echo 'export CAMLP4LIB=C:/OCaml/lib/camlp4' >> ~/.bash_profile - export CAMLP4LIB=C:/OCaml/lib/camlp4 -echo 'export PATH="/cygdrive/c/lablgtk-2.18.3:/cygdrive/c/gtk/bin:$PATH"' >> ~/.bash_profile - export PATH="/cygdrive/c/lablgtk-2.18.3:/cygdrive/c/gtk/bin:$PATH" -./configure -make -make opt -#In src/Makefile, after the line -# include $(CONFIG) -#insert the line -# FLINSTALLDIR := $(subst \,/,$(FLINSTALLDIR)) -sed -i 's/include \$(CONFIG)/include \$(CONFIG)\nFLINSTALLDIR := \$(subst \\,\/,\$(FLINSTALLDIR)\)\n/' src/Makefile -make install -cd .. - -# Hack to make "ar" work in makefiles -which ar 2>/dev/null || ln -s $(which i686-w64-mingw32-ar.exe) /usr/bin/ar +echo 'export PATH="$PATH:/cygdrive/c/vfdeps-17.12/bin"' >> ~/.bash_profile + export PATH="$PATH:/cygdrive/c/vfdeps-17.12/bin" diff --git a/src/GNUmakefile b/src/GNUmakefile index 13d061e5f..cc9c2114d 100644 --- a/src/GNUmakefile +++ b/src/GNUmakefile @@ -48,12 +48,8 @@ endif # Lablgtk configuration ifndef WITHOUT_LABLGTK - ifeq ($(OS), Windows_NT) - LABLGTK_FLAGS += -I +site-lib/lablgtk2 lablgtk.cmxa - else - LABLGTK_FLAGS_ += -I +../lablgtk2 -I +lablgtk2 - LABLGTK_FLAGS += ${LABLGTK_FLAGS_} lablgtk.cmxa - endif + LABLGTK_FLAGS_ += -I +../lablgtk2 -I +lablgtk2 + LABLGTK_FLAGS += ${LABLGTK_FLAGS_} lablgtk.cmxa ifdef WITHOUT_GTKSOURCEVIEW GTKSOURCEVIEW_LFLAGS += -I macos GSourceView2.cmx GLineMarks.cmx GTKSOURCEVIEW_DEPS += macos/GSourceView2.cmx macos/GLineMarks.cmx diff --git a/src/linemarks/Makefile b/src/linemarks/Makefile index fd1d25f53..4f3e86488 100644 --- a/src/linemarks/Makefile +++ b/src/linemarks/Makefile @@ -1,20 +1,14 @@ ifeq ($(OS), Windows_NT) DOTEXE=.exe -LABLGTK2=site-lib/lablgtk2 else DOTEXE= -LABLGTK2=lablgtk2 endif hello$(DOTEXE): hello.ml linemarks.cmxa - ${OCAMLOPT} ${OCAMLCFLAGS} -o hello$(DOTEXE) -I +$(LABLGTK2) lablgtk.cmxa lablgtksourceview2.cmxa linemarks.cmxa gtkInit.cmx hello.ml + ${OCAMLOPT} ${OCAMLCFLAGS} -o hello$(DOTEXE) $(LABLGTK_FLAGS) lablgtksourceview2.cmxa linemarks.cmxa gtkInit.cmx hello.ml linemarks.cmxa: liblinemarks.a -ifeq ($(OS), Windows_NT) - ${OCAMLOPT} ${OCAMLCFLAGS} -a -o linemarks.cmxa -I +$(LABLGTK2) GtkLineMarks.mli GtkLineMarks.ml GLineMarks.ml -cclib -L$(shell pwd) -cclib -llinemarks -cclib "`pkg-config --libs gtksourceview-2.0`" -else ${OCAMLOPT} ${OCAMLCFLAGS} -a -o linemarks.cmxa $(LABLGTK_FLAGS) GtkLineMarks.mli GtkLineMarks.ml GLineMarks.ml -cclib -L$(shell pwd) -cclib -llinemarks -cclib "`pkg-config --libs gtksourceview-2.0`" -endif liblinemarks.a: linemarks.o ar r liblinemarks.a linemarks.o ml_GtkLineMarks.o diff --git a/src/win/GNUmakefile b/src/win/GNUmakefile index b8edc41af..859ee3a7e 100644 --- a/src/win/GNUmakefile +++ b/src/win/GNUmakefile @@ -1,5 +1,6 @@ win/Perf.cmxa: win/caml_perf.c win/Perf.mli win/Perf.ml win/Stopwatch.mli win/caml_stopwatch.c - cd win; ocamlopt.opt -a -o Perf.cmxa caml_perf.c Perf.mli Perf.ml Stopwatch.mli caml_stopwatch.c + cd win; ocamlopt.opt -c -opaque Stopwatch.mli Stopwatch.ml + cd win; ocamlopt.opt -a -o Perf.cmxa caml_perf.c Perf.mli Perf.ml caml_stopwatch.c Stopwatch.cmx clean:: rm -f win/*.o win/*.a win/*.cm* diff --git a/src/win/Stopwatch.ml b/src/win/Stopwatch.ml new file mode 100644 index 000000000..34d58d1c6 --- /dev/null +++ b/src/win/Stopwatch.ml @@ -0,0 +1,16 @@ +external getpid: unit -> int32 = "caml_stopwatch_getpid" + +(** Locks this process to processor 1. + * This potentially improves the accuracy of timing results on multicore systems. + * This module uses the RDTSC (read timestamp counter) instruction; these counters might not run in lockstep on the different processors of a system. *) +external lock_process_to_processor_1: unit -> unit = "caml_lock_process_to_processor_1" + +external processor_ticks: unit -> int64 = "caml_stopwatch_processor_ticks" + +(** The type of stopwatches. *) +type t + +external create: unit -> t = "caml_stopwatch_create" +external start: t -> unit = "caml_stopwatch_start" +external stop: t -> unit = "caml_stopwatch_stop" +external ticks: t -> int64 = "caml_stopwatch_ticks"