aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-12-15 01:51:13 +0100
committerEmilio Jesus Gallego Arias2018-12-25 20:41:04 +0100
commit63aaca037f37ce7f026a23ca0fdf33fb12bbeb63 (patch)
tree6245ca4d10ca92b66aa5c392c8fa442109fca749
parent599696d804eb7c40661615a49c5d729e7d6ff373 (diff)
[windows] Cleanup cruft from `dev/build/windows`
The amount of cruft we are carrying there is high enough as to even difficult navigation. More cleanup should be performed, but this is a first step.
-rw-r--r--dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat28
-rw-r--r--dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat28
-rw-r--r--dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat28
-rw-r--r--dev/build/windows/MakeCoq_85pl3_installer.bat26
-rw-r--r--dev/build/windows/MakeCoq_85pl3_installer_32.bat26
-rw-r--r--dev/build/windows/MakeCoq_86_abs_ocaml.bat10
-rw-r--r--dev/build/windows/MakeCoq_86_installer.bat8
-rw-r--r--dev/build/windows/MakeCoq_86_installer_32.bat8
-rw-r--r--dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat10
-rw-r--r--dev/build/windows/MakeCoq_86beta1_installer.bat8
-rw-r--r--dev/build/windows/MakeCoq_86beta1_installer_32.bat8
-rw-r--r--dev/build/windows/MakeCoq_86git_abs_ocaml.bat28
-rw-r--r--dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat29
-rw-r--r--dev/build/windows/MakeCoq_86git_installer.bat26
-rw-r--r--dev/build/windows/MakeCoq_86git_installer2.bat8
-rw-r--r--dev/build/windows/MakeCoq_86git_installer_32.bat26
-rwxr-xr-xdev/build/windows/MakeCoq_86git_installer_cyglocal.bat27
-rw-r--r--dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat10
-rw-r--r--dev/build/windows/MakeCoq_86rc1_installer.bat8
-rw-r--r--dev/build/windows/MakeCoq_86rc1_installer_32.bat8
-rwxr-xr-xdev/build/windows/MakeCoq_88git_installer.bat27
-rw-r--r--dev/build/windows/ReadMe.txt39
-rw-r--r--dev/build/windows/patches_coq/camlp4-4.02+6.patch11
-rw-r--r--dev/build/windows/patches_coq/coq-8.4pl2.patch11
-rw-r--r--dev/build/windows/patches_coq/coq-8.4pl6.patch13
-rw-r--r--dev/build/windows/patches_coq/flexdll-0.34.patch14
-rw-r--r--dev/build/windows/patches_coq/glib-2.46.0.patch30
-rw-r--r--dev/build/windows/patches_coq/lablgtk-2.18.3.patch101
-rw-r--r--[-rwxr-xr-x]dev/build/windows/patches_coq/sed-4.2.2-3.src.patch0
-rw-r--r--[-rwxr-xr-x]dev/build/windows/patches_coq/sed-4.2.2.patch0
30 files changed, 0 insertions, 604 deletions
diff --git a/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat b/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat
deleted file mode 100644
index 9dbce1920f..0000000000
--- a/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat
+++ /dev/null
@@ -1,28 +0,0 @@
-@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.4pl6 ^
- -destcyg="%ROOTPATH%\cygwin_coq64_84pl6_abs" ^
- -destcoq="%ROOTPATH%\coq64_84pl6_abs"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_84pl6_abs_ocaml.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat b/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat
deleted file mode 100644
index 7faf3e9ce1..0000000000
--- a/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat
+++ /dev/null
@@ -1,28 +0,0 @@
-@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.5pl2 ^
- -destcyg="%ROOTPATH%\cygwin_coq64_85pl2_abs" ^
- -destcoq="%ROOTPATH%\coq64_85pl2_abs"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_85pl2_abs_ocaml.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat b/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat
deleted file mode 100644
index b719b14c53..0000000000
--- a/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat
+++ /dev/null
@@ -1,28 +0,0 @@
-@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.5pl3 ^
- -destcyg="%ROOTPATH%\cygwin_coq64_85pl3_abs" ^
- -destcoq="%ROOTPATH%\coq64_85pl3_abs"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_85pl3_abs_ocaml.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_85pl3_installer.bat b/dev/build/windows/MakeCoq_85pl3_installer.bat
deleted file mode 100644
index a9f4e2da2e..0000000000
--- a/dev/build/windows/MakeCoq_85pl3_installer.bat
+++ /dev/null
@@ -1,26 +0,0 @@
-@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=8.5pl3 ^
- -destcyg="%ROOTPATH%\cygwin_coq64_85pl3_inst" ^
- -destcoq="%ROOTPATH%\coq64_85pl3_inst"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_85pl3_installer.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_85pl3_installer_32.bat b/dev/build/windows/MakeCoq_85pl3_installer_32.bat
deleted file mode 100644
index ef593cc63a..0000000000
--- a/dev/build/windows/MakeCoq_85pl3_installer_32.bat
+++ /dev/null
@@ -1,26 +0,0 @@
-@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=32 ^
- -installer=Y ^
- -coqver=8.5pl3 ^
- -destcyg="%ROOTPATH%\cygwin_coq32_85pl3_inst" ^
- -destcoq="%ROOTPATH%\coq32_85pl3_inst"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_85pl3_installer_32.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_86_abs_ocaml.bat b/dev/build/windows/MakeCoq_86_abs_ocaml.bat
deleted file mode 100644
index 50483c4d4a..0000000000
--- a/dev/build/windows/MakeCoq_86_abs_ocaml.bat
+++ /dev/null
@@ -1,10 +0,0 @@
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.6 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86_abs ^
- -destcoq=%ROOTPATH%\coq64_86_abs
diff --git a/dev/build/windows/MakeCoq_86_installer.bat b/dev/build/windows/MakeCoq_86_installer.bat
deleted file mode 100644
index 263520ff14..0000000000
--- a/dev/build/windows/MakeCoq_86_installer.bat
+++ /dev/null
@@ -1,8 +0,0 @@
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=8.6 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86_inst ^
- -destcoq=%ROOTPATH%\coq64_86_inst
diff --git a/dev/build/windows/MakeCoq_86_installer_32.bat b/dev/build/windows/MakeCoq_86_installer_32.bat
deleted file mode 100644
index 14921dd7c3..0000000000
--- a/dev/build/windows/MakeCoq_86_installer_32.bat
+++ /dev/null
@@ -1,8 +0,0 @@
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=32 ^
- -installer=Y ^
- -coqver=8.6 ^
- -destcyg=%ROOTPATH%\cygwin_coq32_86_inst ^
- -destcoq=%ROOTPATH%\coq32_86_inst
diff --git a/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat b/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat
deleted file mode 100644
index 914c332f46..0000000000
--- a/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat
+++ /dev/null
@@ -1,10 +0,0 @@
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.6beta1 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86beta1_abs ^
- -destcoq=%ROOTPATH%\coq64_86beta1_abs
diff --git a/dev/build/windows/MakeCoq_86beta1_installer.bat b/dev/build/windows/MakeCoq_86beta1_installer.bat
deleted file mode 100644
index 76a5bb35ac..0000000000
--- a/dev/build/windows/MakeCoq_86beta1_installer.bat
+++ /dev/null
@@ -1,8 +0,0 @@
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=8.6beta1 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86beta1_inst ^
- -destcoq=%ROOTPATH%\coq64_86beta1_inst
diff --git a/dev/build/windows/MakeCoq_86beta1_installer_32.bat b/dev/build/windows/MakeCoq_86beta1_installer_32.bat
deleted file mode 100644
index f53232b651..0000000000
--- a/dev/build/windows/MakeCoq_86beta1_installer_32.bat
+++ /dev/null
@@ -1,8 +0,0 @@
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=32 ^
- -installer=Y ^
- -coqver=8.6beta1 ^
- -destcyg=%ROOTPATH%\cygwin_coq32_86beta1_inst ^
- -destcoq=%ROOTPATH%\coq32_86beta1_inst
diff --git a/dev/build/windows/MakeCoq_86git_abs_ocaml.bat b/dev/build/windows/MakeCoq_86git_abs_ocaml.bat
deleted file mode 100644
index 99a1f156b0..0000000000
--- a/dev/build/windows/MakeCoq_86git_abs_ocaml.bat
+++ /dev/null
@@ -1,28 +0,0 @@
-@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=git-v8.6 ^
- -destcyg="%ROOTPATH%\cygwin_coq64_86git_abs" ^
- -destcoq="%ROOTPATH%\coq64_86git_abs"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_86git_abs_ocaml.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat b/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat
deleted file mode 100644
index 896d1cd633..0000000000
--- a/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat
+++ /dev/null
@@ -1,29 +0,0 @@
-@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -gtksrc=Y ^
- -coqver=git-v8.6 ^
- -destcyg="%ROOTPATH%\cygwin_coq64_86git_abs_gtksrc" ^
- -destcoq="%ROOTPATH%\coq64_86git_abs_gtksrc"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_86git_abs_ocaml_gtksrc.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_86git_installer.bat b/dev/build/windows/MakeCoq_86git_installer.bat
deleted file mode 100644
index c4823103f1..0000000000
--- a/dev/build/windows/MakeCoq_86git_installer.bat
+++ /dev/null
@@ -1,26 +0,0 @@
-@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=git-v8.6 ^
- -destcyg="%ROOTPATH%\cygwin_coq64_86git_inst" ^
- -destcoq="%ROOTPATH%\coq64_86git_inst"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_86git_installer.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_86git_installer2.bat b/dev/build/windows/MakeCoq_86git_installer2.bat
deleted file mode 100644
index d184f0e30e..0000000000
--- a/dev/build/windows/MakeCoq_86git_installer2.bat
+++ /dev/null
@@ -1,8 +0,0 @@
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=git-v8.6 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86git_inst2 ^
- -destcoq=%ROOTPATH%\coq64_86git_inst2
diff --git a/dev/build/windows/MakeCoq_86git_installer_32.bat b/dev/build/windows/MakeCoq_86git_installer_32.bat
deleted file mode 100644
index 19146c96c9..0000000000
--- a/dev/build/windows/MakeCoq_86git_installer_32.bat
+++ /dev/null
@@ -1,26 +0,0 @@
-@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=32 ^
- -installer=Y ^
- -coqver=git-v8.6 ^
- -destcyg="%ROOTPATH%\cygwin_coq32_86git_inst" ^
- -destcoq="%ROOTPATH%\coq32_86git_inst"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_86git_installer_32.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_86git_installer_cyglocal.bat b/dev/build/windows/MakeCoq_86git_installer_cyglocal.bat
deleted file mode 100755
index cf6cafaa02..0000000000
--- a/dev/build/windows/MakeCoq_86git_installer_cyglocal.bat
+++ /dev/null
@@ -1,27 +0,0 @@
-@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=git-v8.6 ^
- -cyglocal=Y ^
- -destcyg="%ROOTPATH%\cygwin_coq64_86git_inst_cyglocal" ^
- -destcoq="%ROOTPATH%\coq64_86git_inst_cyglocal"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_86git_installer_cyglocal.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat b/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat
deleted file mode 100644
index c0669f01d2..0000000000
--- a/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat
+++ /dev/null
@@ -1,10 +0,0 @@
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.6rc1 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86rc1_abs ^
- -destcoq=%ROOTPATH%\coq64_86rc1_abs
diff --git a/dev/build/windows/MakeCoq_86rc1_installer.bat b/dev/build/windows/MakeCoq_86rc1_installer.bat
deleted file mode 100644
index 66234ebbde..0000000000
--- a/dev/build/windows/MakeCoq_86rc1_installer.bat
+++ /dev/null
@@ -1,8 +0,0 @@
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=8.6rc1 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86rc1_inst ^
- -destcoq=%ROOTPATH%\coq64_86rc1_inst
diff --git a/dev/build/windows/MakeCoq_86rc1_installer_32.bat b/dev/build/windows/MakeCoq_86rc1_installer_32.bat
deleted file mode 100644
index 96f43e16a5..0000000000
--- a/dev/build/windows/MakeCoq_86rc1_installer_32.bat
+++ /dev/null
@@ -1,8 +0,0 @@
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=32 ^
- -installer=Y ^
- -coqver=8.6rc1 ^
- -destcyg=%ROOTPATH%\cygwin_coq32_86rc1_inst ^
- -destcoq=%ROOTPATH%\coq32_86rc1_inst
diff --git a/dev/build/windows/MakeCoq_88git_installer.bat b/dev/build/windows/MakeCoq_88git_installer.bat
deleted file mode 100755
index b016fb3891..0000000000
--- a/dev/build/windows/MakeCoq_88git_installer.bat
+++ /dev/null
@@ -1,27 +0,0 @@
-@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=git-v8.8 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_88_inst ^
- -destcoq=%ROOTPATH%\coq64_88_inst ^
- -addon=bignums
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_88git_installer.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt
index 93851aeb8d..a392115ea4 100644
--- a/dev/build/windows/ReadMe.txt
+++ b/dev/build/windows/ReadMe.txt
@@ -369,8 +369,6 @@ Text files patched by the installer:
Text files containing the install folder path after install:
-./bin/mkcamlp5:LIB=D:/bin/coq64_buildtest_reloc_ocaml20/libocaml/camlp5
-./bin/mkcamlp5.opt:LIB=D:/bin/coq64_buildtest_reloc_ocaml20/libocaml/camlp5
./libocaml/Makefile.config:PREFIX=D:/bin/coq64_buildtest_reloc_ocaml20
./libocaml/Makefile.config:LIBDIR=D:/bin/coq64_buildtest_reloc_ocaml20/libocaml
./libocaml/site-lib/findlib/Makefile.config:OCAML_CORE_BIN=/cygdrive/d/bin/coq64_buildtest_reloc_ocaml20/bin
@@ -382,8 +380,6 @@ Text files containing the install folder path after install:
./libocaml/topfind: Topdirs.dir_load Format.err_formatter "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib_top.cma";
./libocaml/topfind:(* #load "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib.cma";; *)
./libocaml/topfind:(* #load "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib_top.cma";; *)
-./man/man1/camlp5.1:These files are installed in the directory D:/bin/coq64_buildtest_reloc_ocaml20/libocaml/camlp5.
-./man/man1/camlp5.1:D:/bin/coq64_buildtest_reloc_ocaml20/libocaml/camlp5
Binary files containing the build folder path after install:
@@ -398,26 +394,6 @@ Binary file ./libocaml/ocamldoc/odoc_info.cma matches
Binary files containing the install folder path after install:
$ find . -type f -exec grep "coq64_buildtest_reloc_ocaml20" {} /dev/null \;
-Binary file ./bin/camlp4.exe matches
-Binary file ./bin/camlp4boot.exe matches
-Binary file ./bin/camlp4o.exe matches
-Binary file ./bin/camlp4o.opt.exe matches
-Binary file ./bin/camlp4of.exe matches
-Binary file ./bin/camlp4of.opt.exe matches
-Binary file ./bin/camlp4oof.exe matches
-Binary file ./bin/camlp4oof.opt.exe matches
-Binary file ./bin/camlp4orf.exe matches
-Binary file ./bin/camlp4orf.opt.exe matches
-Binary file ./bin/camlp4r.exe matches
-Binary file ./bin/camlp4r.opt.exe matches
-Binary file ./bin/camlp4rf.exe matches
-Binary file ./bin/camlp4rf.opt.exe matches
-Binary file ./bin/camlp5.exe matches
-Binary file ./bin/camlp5o.exe matches
-Binary file ./bin/camlp5o.opt matches
-Binary file ./bin/camlp5r.exe matches
-Binary file ./bin/camlp5r.opt matches
-Binary file ./bin/camlp5sch.exe matches
Binary file ./bin/coqc.exe matches
Binary file ./bin/coqchk.exe matches
Binary file ./bin/coqdep.exe matches
@@ -428,11 +404,7 @@ Binary file ./bin/coqtop.exe matches
Binary file ./bin/coqworkmgr.exe matches
Binary file ./bin/coq_makefile.exe matches
Binary file ./bin/menhir matches
-Binary file ./bin/mkcamlp4.exe matches
Binary file ./bin/ocaml.exe matches
-Binary file ./bin/ocamlbuild.byte.exe matches
-Binary file ./bin/ocamlbuild.exe matches
-Binary file ./bin/ocamlbuild.native.exe matches
Binary file ./bin/ocamlc.exe matches
Binary file ./bin/ocamlc.opt.exe matches
Binary file ./bin/ocamldebug.exe matches
@@ -455,17 +427,6 @@ Binary file ./lib/ide/ide_win32_stubs.o matches
Binary file ./lib/lib/clib.a matches
Binary file ./lib/lib/clib.cma matches
Binary file ./lib/libcoqrun.a matches
-Binary file ./libocaml/camlp4/camlp4fulllib.a matches
-Binary file ./libocaml/camlp4/camlp4fulllib.cma matches
-Binary file ./libocaml/camlp4/camlp4lib.a matches
-Binary file ./libocaml/camlp4/camlp4lib.cma matches
-Binary file ./libocaml/camlp4/camlp4o.cma matches
-Binary file ./libocaml/camlp4/camlp4of.cma matches
-Binary file ./libocaml/camlp4/camlp4oof.cma matches
-Binary file ./libocaml/camlp4/camlp4orf.cma matches
-Binary file ./libocaml/camlp4/camlp4r.cma matches
-Binary file ./libocaml/camlp4/camlp4rf.cma matches
-Binary file ./libocaml/camlp5/odyl.cma matches
Binary file ./libocaml/compiler-libs/ocamlcommon.a matches
Binary file ./libocaml/compiler-libs/ocamlcommon.cma matches
Binary file ./libocaml/dynlink.cma matches
diff --git a/dev/build/windows/patches_coq/camlp4-4.02+6.patch b/dev/build/windows/patches_coq/camlp4-4.02+6.patch
deleted file mode 100644
index 0cdb4a929b..0000000000
--- a/dev/build/windows/patches_coq/camlp4-4.02+6.patch
+++ /dev/null
@@ -1,11 +0,0 @@
---- camlp4-4.02-6.orig/myocamlbuild.ml 2015-06-17 13:37:36.000000000 +0200
-+++ camlp4-4.02+6/myocamlbuild.ml 2016-10-13 13:57:35.512213600 +0200
-@@ -86,7 +86,7 @@
- let dep = "camlp4"/"boot"/exe in
- let cmd =
- let ( / ) = Filename.concat in
-- "camlp4"/"boot"/exe
-+ String.escaped (String.escaped ("camlp4"/"boot"/exe))
- in
- (Some dep, cmd)
- in
diff --git a/dev/build/windows/patches_coq/coq-8.4pl2.patch b/dev/build/windows/patches_coq/coq-8.4pl2.patch
deleted file mode 100644
index 45a66d0bfa..0000000000
--- a/dev/build/windows/patches_coq/coq-8.4pl2.patch
+++ /dev/null
@@ -1,11 +0,0 @@
---- configure 2014-04-14 22:28:39.174177924 +0200
-+++ configure 2014-04-14 22:29:23.253025166 +0200
-@@ -335,7 +335,7 @@
- MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3`
- MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1`
- MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2`
-- if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then
-+ if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ] || [ "$MAKEVERSIONMAJOR" -ge 4 ] ; then
- echo "You have GNU Make $MAKEVERSION. Good!"
- else
- OK="no" \ No newline at end of file
diff --git a/dev/build/windows/patches_coq/coq-8.4pl6.patch b/dev/build/windows/patches_coq/coq-8.4pl6.patch
deleted file mode 100644
index c3b7f8574e..0000000000
--- a/dev/build/windows/patches_coq/coq-8.4pl6.patch
+++ /dev/null
@@ -1,13 +0,0 @@
-coq-8.4pl6.orig
---- coq-8.4pl6.orig/configure 2015-04-09 15:59:35.000000000 +0200
-+++ coq-8.4pl6//configure 2016-11-09 13:29:42.235319800 +0100
-@@ -309,9 +309,6 @@
- # executable extension
-
- case "$ARCH,$CYGWIN" in
-- win32,yes)
-- EXE=".exe"
-- DLLEXT=".so";;
- win32,*)
- EXE=".exe"
- DLLEXT=".dll";;
diff --git a/dev/build/windows/patches_coq/flexdll-0.34.patch b/dev/build/windows/patches_coq/flexdll-0.34.patch
deleted file mode 100644
index 16389baca3..0000000000
--- a/dev/build/windows/patches_coq/flexdll-0.34.patch
+++ /dev/null
@@ -1,14 +0,0 @@
-reloc.ml
---- orig.flexdll-0.34/reloc.ml 2015-01-22 17:30:07.000000000 +0100
-+++ flexdll-0.34/reloc.ml 2016-10-12 11:59:16.885829700 +0200
-@@ -117,8 +117,8 @@
-
- let new_cmdline () =
- let rf = match !toolchain with
-- | `MSVC | `MSVC64 | `LIGHTLD -> true
-- | `MINGW | `MINGW64 | `GNAT | `CYGWIN | `CYGWIN64 -> false
-+ | `MSVC | `MSVC64 | `LIGHTLD | `MINGW | `MINGW64 -> true
-+ | `GNAT | `CYGWIN | `CYGWIN64 -> false
- in
- {
- may_use_response_file = rf;
diff --git a/dev/build/windows/patches_coq/glib-2.46.0.patch b/dev/build/windows/patches_coq/glib-2.46.0.patch
deleted file mode 100644
index 9082460bf0..0000000000
--- a/dev/build/windows/patches_coq/glib-2.46.0.patch
+++ /dev/null
@@ -1,30 +0,0 @@
-diff -u -r glib-2.46.0/gio/glocalfile.c glib-2.46.0.patched/gio/glocalfile.c
---- glib-2.46.0/gio/glocalfile.c 2015-08-27 05:32:26.000000000 +0200
-+++ glib-2.46.0.patched/gio/glocalfile.c 2016-01-27 13:08:30.059736400 +0100
-@@ -2682,7 +2682,10 @@
- (!g_path_is_absolute (filename) || len > g_path_skip_root (filename) - filename))
- wfilename[len] = '\0';
-
-- retval = _wstat32i64 (wfilename, &buf);
-+ // MSoegtrop: _wstat32i64 is the wrong function for GLocalFileStat = struct _stati64
-+ // The correct function is _wstati64, see https://msdn.microsoft.com/en-us/library/14h5k7ff.aspx
-+ // Also _wstat32i64 is a VC function, not a windows SDK function, see https://msdn.microsoft.com/en-us/library/aa273365(v=vs.60).aspx
-+ retval = _wstati64 (wfilename, &buf);
- save_errno = errno;
-
- g_free (wfilename);
-diff -u -r glib-2.46.0/glib/gstdio.c glib-2.46.0.patched/glib/gstdio.c
---- glib-2.46.0/glib/gstdio.c 2015-02-26 13:57:09.000000000 +0100
-+++ glib-2.46.0.patched/glib/gstdio.c 2016-01-27 13:31:12.708987700 +0100
-@@ -493,7 +493,10 @@
- (!g_path_is_absolute (filename) || len > g_path_skip_root (filename) - filename))
- wfilename[len] = '\0';
-
-- retval = _wstat (wfilename, buf);
-+ // MSoegtrop: _wstat32i64 is the wrong function for GLocalFileStat = struct _stati64
-+ // The correct function is _wstati64, see https://msdn.microsoft.com/en-us/library/14h5k7ff.aspx
-+ // Also _wstat32i64 is a VC function, not a windows SDK function, see https://msdn.microsoft.com/en-us/library/aa273365(v=vs.60).aspx
-+ retval = _wstati64 (wfilename, buf);
- save_errno = errno;
-
- g_free (wfilename);
diff --git a/dev/build/windows/patches_coq/lablgtk-2.18.3.patch b/dev/build/windows/patches_coq/lablgtk-2.18.3.patch
deleted file mode 100644
index 23c303135d..0000000000
--- a/dev/build/windows/patches_coq/lablgtk-2.18.3.patch
+++ /dev/null
@@ -1,101 +0,0 @@
-diff/patch file created on Wed, Apr 25, 2018 11:08:05 AM with:
-difftar-folder.sh ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz lablgtk-2.18.3 1
-TARFILE= ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz
-FOLDER= lablgtk-2.18.3
-TARSTRIP= 1
-TARPREFIX= lablgtk-2.18.3/
-ORIGFOLDER= lablgtk-2.18.3.orig
---- lablgtk-2.18.3.orig/configure 2014-10-29 08:51:05.000000000 +0100
-+++ lablgtk-2.18.3/configure 2018-04-25 10:58:54.454501600 +0200
-@@ -2667,7 +2667,7 @@
- fi
-
-
--if test "`$OCAMLFIND printconf stdlib`" != "`$CAMLC -where`"; then
-+if test "`$OCAMLFIND printconf stdlib | tr '\\' '/'`" != "`$CAMLC -where | tr '\\' '/'`"; then
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Ignoring ocamlfind" >&5
- $as_echo "$as_me: WARNING: Ignoring ocamlfind" >&2;}
- OCAMLFIND=no
---- lablgtk-2.18.3.orig/src/glib.mli 2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3/src/glib.mli 2018-04-25 10:58:54.493555500 +0200
-@@ -75,6 +75,7 @@
- type condition = [ `ERR | `HUP | `IN | `NVAL | `OUT | `PRI]
- type id
- val channel_of_descr : Unix.file_descr -> channel
-+ val channel_of_descr_socket : Unix.file_descr -> channel
- val add_watch :
- cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
- val remove : id -> unit
---- lablgtk-2.18.3.orig/src/glib.ml 2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3/src/glib.ml 2018-04-25 10:58:54.479543500 +0200
-@@ -72,6 +72,8 @@
- type id
- external channel_of_descr : Unix.file_descr -> channel
- = "ml_g_io_channel_unix_new"
-+ external channel_of_descr_socket : Unix.file_descr -> channel
-+ = "ml_g_io_channel_unix_new_socket"
- external remove : id -> unit = "ml_g_source_remove"
- external add_watch :
- cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
---- lablgtk-2.18.3.orig/src/Makefile 2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3/src/Makefile 2018-04-25 10:58:54.506522500 +0200
-@@ -461,9 +461,9 @@
- do rm -f "$(BINDIR)"/$$f; done
-
- lablgtk.cma liblablgtk2$(XA): $(COBJS) $(MLOBJS)
-- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
-+ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
- lablgtk.cmxa: $(COBJS) $(MLOBJS:.cmo=.cmx)
-- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
-+ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
- lablgtk.cmxs: DYNLINKLIBS=$(GTK_LIBS)
-
- lablgtkgl.cma liblablgtkgl2$(XA): $(GLCOBJS) $(GLMLOBJS)
---- lablgtk-2.18.3.orig/src/ml_glib.c 2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3/src/ml_glib.c 2018-04-25 10:58:54.539535600 +0200
-@@ -25,6 +25,8 @@
- #include <string.h>
- #include <locale.h>
- #ifdef _WIN32
-+/* to kill a #warning: include winsock2.h before windows.h */
-+#include <winsock2.h>
- #include "win32.h"
- #include <wtypes.h>
- #include <io.h>
-@@ -38,6 +40,11 @@
- #include <caml/callback.h>
- #include <caml/threads.h>
-
-+#ifdef _WIN32
-+/* for Socket_val */
-+#include <caml/unixsupport.h>
-+#endif
-+
- #include "wrappers.h"
- #include "ml_glib.h"
- #include "glib_tags.h"
-@@ -325,14 +332,23 @@
-
- #ifndef _WIN32
- ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref)
-+CAMLprim value ml_g_io_channel_unix_new_socket (value arg1) {
-+ return Val_GIOChannel_noref (g_io_channel_unix_new (Int_val (arg1)));
-+}
-
- #else
- CAMLprim value ml_g_io_channel_unix_new(value wh)
- {
- return Val_GIOChannel_noref
-- (g_io_channel_unix_new
-+ (g_io_channel_win32_new_fd
- (_open_osfhandle((long)*(HANDLE*)Data_custom_val(wh), O_BINARY)));
- }
-+
-+CAMLprim value ml_g_io_channel_unix_new_socket(value wh)
-+{
-+ return Val_GIOChannel_noref
-+ (g_io_channel_win32_new_socket(Socket_val(wh)));
-+}
- #endif
-
- static gboolean ml_g_io_channel_watch(GIOChannel *s, GIOCondition c,
diff --git a/dev/build/windows/patches_coq/sed-4.2.2-3.src.patch b/dev/build/windows/patches_coq/sed-4.2.2-3.src.patch
index d210a04153..d210a04153 100755..100644
--- a/dev/build/windows/patches_coq/sed-4.2.2-3.src.patch
+++ b/dev/build/windows/patches_coq/sed-4.2.2-3.src.patch
diff --git a/dev/build/windows/patches_coq/sed-4.2.2.patch b/dev/build/windows/patches_coq/sed-4.2.2.patch
index c7ccd53c7f..c7ccd53c7f 100755..100644
--- a/dev/build/windows/patches_coq/sed-4.2.2.patch
+++ b/dev/build/windows/patches_coq/sed-4.2.2.patch