From 6b2daed7df72b25e7fcaecb4c0ef05d3f4051c26 Mon Sep 17 00:00:00 2001 From: Bart Jacobs Date: Tue, 5 Dec 2017 10:12:00 +0100 Subject: [PATCH] Add script for building VF build deps on Win32 --- make_vfdeps_win32/Makefile | 228 +++++++++++++++++++++++++ make_vfdeps_win32/download_and_untar | 24 +++ make_vfdeps_win32/download_and_unzip | 24 +++ make_vfdeps_win32/install-cygwin.bat | 22 +++ make_vfdeps_win32/ocaml-Makefile.patch | 8 + make_vfdeps_win32/pkg-config | 3 + 6 files changed, 309 insertions(+) create mode 100644 make_vfdeps_win32/Makefile create mode 100644 make_vfdeps_win32/download_and_untar create mode 100644 make_vfdeps_win32/download_and_unzip create mode 100644 make_vfdeps_win32/install-cygwin.bat create mode 100644 make_vfdeps_win32/ocaml-Makefile.patch create mode 100644 make_vfdeps_win32/pkg-config diff --git a/make_vfdeps_win32/Makefile b/make_vfdeps_win32/Makefile new file mode 100644 index 000000000..c478f4842 --- /dev/null +++ b/make_vfdeps_win32/Makefile @@ -0,0 +1,228 @@ +PREFIX=C:/vfdeps-17.12 +MAKEDIR:=$(shell pwd) +PATH:=$(shell cygpath "$(MAKEDIR)"):$(shell cygpath "$(PREFIX)")/bin:$(PATH) + +all: ocaml findlib num ocamlbuild camlp4 gtk lablgtk z3 + +clean:: + -rm -Rf $(PREFIX) + +# ---- OCaml ---- + +OCAML_VERSION=4.06.0 +OCAML_TGZ=ocaml-$(OCAML_VERSION).tar.gz +OCAML_SRC=ocaml-$(OCAML_VERSION)/config/Makefile.mingw +FLEXDLL_VERSION=0.37 +FLEXDLL_TGZ=flexdll-$(FLEXDLL_VERSION).tar.gz +FLEXDLL_SRC=flexdll-$(FLEXDLL_VERSION)/flexdll.c +OCAML_EXE=$(PREFIX)/bin/ocamlopt.opt.exe + +$(OCAML_TGZ): + curl -Lfo ocaml-$(OCAML_VERSION).tar.gz https://github.com/ocaml/ocaml/archive/$(OCAML_VERSION).tar.gz + +$(OCAML_SRC): $(OCAML_TGZ) + tar xzfm $(OCAML_TGZ) + +$(FLEXDLL_TGZ): + curl -Lfo $(FLEXDLL_TGZ) https://github.com/alainfrisch/flexdll/archive/$(FLEXDLL_VERSION).tar.gz + +$(FLEXDLL_SRC): $(FLEXDLL_TGZ) + tar xzfm $(FLEXDLL_TGZ) + +ocaml-$(OCAML_VERSION)/flexdll/flexdll.c: $(OCAML_SRC) $(FLEXDLL_SRC) + cd ocaml-$(OCAML_VERSION)/flexdll && cp -R ../../flexdll-$(FLEXDLL_VERSION)/* . + +ocaml-$(OCAML_VERSION)/config/Makefile: $(OCAML_SRC) + cd ocaml-$(OCAML_VERSION) && \ + cp config/m-nt.h byterun/caml/m.h && \ + cp config/s-nt.h byterun/caml/s.h && \ + cp config/Makefile.mingw config/Makefile && \ + patch config/Makefile ../ocaml-Makefile.patch + +$(OCAML_EXE): ocaml-$(OCAML_VERSION)/config/Makefile ocaml-$(OCAML_VERSION)/flexdll/flexdll.c + cd ocaml-$(OCAML_VERSION) && \ + make flexdll world opt opt.opt flexlink.opt install + +ocaml: $(OCAML_EXE) +.PHONY: ocaml + +clean:: + -rm -Rf ocaml-$(OCAML_VERSION) + -rm -Rf flexdll-$(FLEXDLL_VERSION) + +# ---- Findlib ---- + +FINDLIB_VERSION=1.7.3 +FINDLIB_EXE=$(PREFIX)/bin/ocamlfind.exe +FINDLIB_TGZ=findlib-$(FINDLIB_VERSION).tar.gz +FINDLIB_SRC=findlib-$(FINDLIB_VERSION)/configure +FINDLIB_CFG=findlib-$(FINDLIB_VERSION)/Makefile.config + +$(FINDLIB_TGZ): + curl -Lfo $(FINDLIB_TGZ) http://download.camlcity.org/download/findlib-$(FINDLIB_VERSION).tar.gz + +$(FINDLIB_SRC): $(FINDLIB_TGZ) + tar xzfm $(FINDLIB_TGZ) + +$(FINDLIB_CFG): $(OCAML_EXE) $(FINDLIB_SRC) + cd findlib-$(FINDLIB_VERSION) && \ + ./configure \ + -bindir $(PREFIX)/bin \ + -mandir $(PREFIX)/man \ + -sitelib $(PREFIX)/lib/ocaml \ + -config $(PREFIX)/etc/findlib.conf + +$(FINDLIB_EXE): $(FINDLIB_CFG) + cd findlib-$(FINDLIB_VERSION) && \ + make all && \ + make opt && \ + make install + +findlib: $(FINDLIB_EXE) +.PHONY: findlib + +clean:: + -rm -Rf findlib-$(FINDLIB_VERSION) + +# ---- Num ---- + +NUM_VERSION=1.1 +NUM_BINARY=$(PREFIX)/lib/ocaml/nums.cmxa +NUM_TGZ=num-$(NUM_VERSION).tar.gz +NUM_SRC=num-$(NUM_VERSION)/Makefile + +$(NUM_TGZ): + curl -Lfo $(NUM_TGZ) https://github.com/ocaml/num/archive/v$(NUM_VERSION).tar.gz + +$(NUM_SRC): $(NUM_TGZ) + tar xzfm $(NUM_TGZ) + +$(NUM_BINARY): $(NUM_SRC) $(FINDLIB_EXE) + cd num-$(NUM_VERSION) && make && make install SO=dll + +num: $(NUM_BINARY) +.PHONY: num + +clean:: + -rm -Rf num-$(NUM_VERSION) + +# ---- ocamlbuild ---- + +OCAMLBUILD_VERSION=0.12.0 +OCAMLBUILD_BINARY=$(PREFIX)/bin/ocamlbuild.exe +OCAMLBUILD_TGZ=ocamlbuild-$(OCAMLBUILD_VERSION).tar.gz +OCAMLBUILD_SRC=ocamlbuild-$(OCAMLBUILD_VERSION)/Makefile + +$(OCAMLBUILD_TGZ): + curl -Lfo $(OCAMLBUILD_TGZ) https://github.com/ocaml/ocamlbuild/archive/$(OCAMLBUILD_VERSION).tar.gz + +$(OCAMLBUILD_SRC): $(OCAMLBUILD_TGZ) + tar xzfm $(OCAMLBUILD_TGZ) + +$(OCAMLBUILD_BINARY): $(FINDLIB_BINARY) $(OCAMLBUILD_SRC) + cd ocamlbuild-$(OCAMLBUILD_VERSION) && \ + make configure && make && make install + +ocamlbuild: $(OCAMLBUILD_BINARY) +.PHONY: ocamlbuild + +clean:: + -rm -Rf ocamlbuild-$(OCAMLBUILD_VERSION) + +# ---- camlp4 ---- + +CAMLP4_VERSION=4.06+1 +CAMLP4_DIR=camlp4-$(subst +,-,$(CAMLP4_VERSION)) +CAMLP4_BINARY=$(PREFIX)/bin/camlp4o.exe +CAMLP4_TGZ=camlp4-$(CAMLP4_VERSION).tar.gz +CAMLP4_SRC=$(CAMLP4_DIR)/configure + +$(CAMLP4_TGZ): + curl -Lfo $(CAMLP4_TGZ) https://github.com/ocaml/camlp4/archive/$(CAMLP4_VERSION).tar.gz + +$(CAMLP4_SRC): $(CAMLP4_TGZ) + tar xzfm $(CAMLP4_TGZ) + +$(CAMLP4_BINARY): $(OCAMLBUILD_BINARY) $(CAMLP4_SRC) + cd $(CAMLP4_DIR) && \ + ./configure && make all && make install + +camlp4: $(CAMLP4_BINARY) +.PHONY: camlp4 + +clean:: + -rm -Rf $(CAMLP4_DIR) + +# ---- GTK ---- + +GTK_BINARY=$(PREFIX)/bin/gtk-demo.exe + +$(GTK_BINARY): + cd $(PREFIX) && \ + for url in \ + ftp://ftp.gnome.org/pub/gnome/binaries/win32/gtk+/2.24/gtk+-bundle_2.24.10-20120208_win32.zip \ + ftp://ftp.gnome.org/pub/gnome/binaries/win32/gtksourceview/2.10/gtksourceview-2.10.0.zip \ + ftp://ftp.gnome.org/pub/gnome/binaries/win32/gtksourceview/2.10/gtksourceview-dev-2.10.0.zip \ + ftp://ftp.gnome.org/pub/gnome/binaries/win32/dependencies/libxml2_2.9.0-1_win32.zip \ + 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 + +gtk: $(GTK_BINARY) +.PHONY: gtk + +# ---- lablgtk ---- + +LABLGTK_VERSION=2.18.6 +LABLGTK_SRC=lablgtk-$(LABLGTK_VERSION)/configure +LABLGTK_CFG=lablgtk-$(LABLGTK_VERSION)/config.make +LABLGTK_BUILD=lablgtk-$(LABLGTK_VERSION)/src/lablgtk2.cmxa +LABLGTK_BINARY=$(PREFIX)/lib/ocaml/lablgtk2/lablgtk2.cmxa + +$(LABLGTK_SRC): + download_and_untar https://forge.ocamlcore.org/frs/download.php/1726/lablgtk-$(LABLGTK_VERSION).tar.gz + +$(LABLGTK_CFG): $(LABLGTK_SRC) $(CAMLP4_BINARY) $(GTK_BINARY) + cd lablgtk-$(LABLGTK_VERSION) && \ + ./configure + +$(LABLGTK_BUILD): $(LABLGTK_CFG) + cd lablgtk-$(LABLGTK_VERSION) && \ + make && make opt + +$(LABLGTK_BINARY): $(LABLGTK_BUILD) + cd lablgtk-$(LABLGTK_VERSION) && make install + +lablgtk: $(LABLGTK_BINARY) +.PHONY: lablgtk + +clean:: + -rm -Rf lablgtk-$(LABLGTK_VERSION) + +# ---- Z3 ---- + +Z3_VERSION=4.5.0 +Z3_BINARY=$(PREFIX)/lib/libz3.dll +Z3_DIR=z3-z3-$(Z3_VERSION) +Z3_SRC=$(Z3_DIR)/scripts/mk_make.py +Z3_CFG=$(Z3_DIR)/build/Makefile +Z3_BUILD=$(Z3_DIR)/build/libz3.dll + +$(Z3_SRC): + download_and_untar https://github.com/Z3Prover/z3/archive/z3-$(Z3_VERSION).tar.gz + +$(Z3_CFG): $(FINDLIB_EXE) $(Z3_SRC) + cd $(Z3_DIR) && CXX=i686-w64-mingw32-g++ CC=i686-w64-mingw32-gcc AR=i686-w64-mingw32-ar python scripts/mk_make.py --ml --prefix=$(PREFIX) + +$(Z3_BUILD): $(Z3_CFG) + cd $(Z3_DIR)/build && make + +$(Z3_BINARY): $(Z3_BUILD) + cd $(Z3_DIR)/build && make install + +z3: $(Z3_BINARY) +.PHONY: z3 + +clean:: + -rm -Rf $(Z3_DIR) diff --git a/make_vfdeps_win32/download_and_untar b/make_vfdeps_win32/download_and_untar new file mode 100644 index 000000000..bd25b6373 --- /dev/null +++ b/make_vfdeps_win32/download_and_untar @@ -0,0 +1,24 @@ +#!/bin/bash + +set -e # Stop as soon as a command fails. +set -x # Print what is being executed. + +dlcache=. + +while [ "$#" != "0" ]; do + case "$1" in + --dlcache) + dlcache=$2 + shift 2 + ;; + *) + url=$1 + shift 1 + ;; + esac +done + +filename=$(basename "$url") +filepath=$dlcache/$filename +if [ ! -f "$filepath" ]; then curl -Lfo "$filepath" "$url"; fi +tar xzfm "$filepath" diff --git a/make_vfdeps_win32/download_and_unzip b/make_vfdeps_win32/download_and_unzip new file mode 100644 index 000000000..733ce689d --- /dev/null +++ b/make_vfdeps_win32/download_and_unzip @@ -0,0 +1,24 @@ +#!/bin/bash + +set -e # Stop as soon as a command fails. +set -x # Print what is being executed. + +dlcache=. + +while [ "$#" != "0" ]; do + case "$1" in + --dlcache) + dlcache=$2 + shift 2 + ;; + *) + url=$1 + shift 1 + ;; + esac +done + +filename=$(basename "$url") +filepath=$dlcache/$filename +if [ ! -f "$filepath" ]; then curl -Lfo "$filepath" "$url"; fi +7z x "$filepath" diff --git a/make_vfdeps_win32/install-cygwin.bat b/make_vfdeps_win32/install-cygwin.bat new file mode 100644 index 000000000..881148a40 --- /dev/null +++ b/make_vfdeps_win32/install-cygwin.bat @@ -0,0 +1,22 @@ +@echo on + + +bitsadmin.exe /transfer "cygwin" https://cygwin.com/setup-x86.exe C:\Bart\setup-cygwin-x86.exe || exit /b + + +C:\Bart\setup-cygwin-x86.exe -B -qnNd -R c:/cygwin -l c:/cygwin/var/cache/setup -s http://ftp.inf.tu-dresden.de/software/windows/cygwin32/ -P python -P p7zip -P curl -P m4 -P make -P mingw64-i686-gcc-g++ -P mingw64-i686-gcc-core -P mingw64-i686-gcc -P patch -P rlwrap -P libreadline6 -P diffutils -P dos2unix -P mingw64-i686-binutils || exit /b + + +@rem Package 'wget' is required as well but is pre-installed on AppVeyor. + + + +@rem Add ",noacl" to prevent cygwin from messing with Windows file permissions + + +echo none /cygdrive cygdrive binary,posix=0,user,noacl 0 0 > c:\cygwin\etc\fstab || exit /b + + + +rem c:\cygwin\bin\bash -lc "cd /cygdrive/c/projects/verifast && bash setup-windows.sh" || exit /b + diff --git a/make_vfdeps_win32/ocaml-Makefile.patch b/make_vfdeps_win32/ocaml-Makefile.patch new file mode 100644 index 000000000..3930d1b35 --- /dev/null +++ b/make_vfdeps_win32/ocaml-Makefile.patch @@ -0,0 +1,8 @@ +20c20 +< PREFIX=C:/ocamlmgw +--- +> PREFIX=C:/vfdeps-17.12 +35c35 +< LIBDIR=$(PREFIX)/lib +--- +> LIBDIR=$(PREFIX)/lib/ocaml diff --git a/make_vfdeps_win32/pkg-config b/make_vfdeps_win32/pkg-config new file mode 100644 index 000000000..aedbf7665 --- /dev/null +++ b/make_vfdeps_win32/pkg-config @@ -0,0 +1,3 @@ +#!/bin/bash +set -o pipefail # A pipe fails if any component fails +/cygdrive/c/vfdeps-17.12/bin/pkg-config $* | dos2unix