diff options
| author | Emilio Jesus Gallego Arias | 2018-12-15 01:51:13 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-25 20:41:04 +0100 |
| commit | 63aaca037f37ce7f026a23ca0fdf33fb12bbeb63 (patch) | |
| tree | 6245ca4d10ca92b66aa5c392c8fa442109fca749 | |
| parent | 599696d804eb7c40661615a49c5d729e7d6ff373 (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.
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 |
