diff options
Diffstat (limited to 'dev/build')
32 files changed, 42 insertions, 626 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/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index b202635714..2e934ff0c0 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -444,9 +444,6 @@ function load_overlay_data { else export CI_BRANCH="" export CI_PULL_REQUEST="" - # Used when building 8.8.0 with the latest scripts - export TRAVIS_BRANCH="" - export TRAVIS_PULL_REQUEST="" fi for overlay in /build/user-overlays/*.sh; do @@ -691,7 +688,7 @@ function installer_addon_end { # ------------------------------------------------------------------------------ function coq_set_timeouts_1000 { - find . -type f -name '*.v' -print0 | xargs -0 sed -i 's/timeout\s\+[0-9]\+/timeout 1000/' + find . -type f -name '*.v' -print0 | xargs -0 sed -i 's/timeout\s\+[0-9]\+/timeout 1000/g' } ###################### MODULE BUILD FUNCTIONS ##################### @@ -701,7 +698,7 @@ function coq_set_timeouts_1000 { function make_sed { if build_prep https://ftp.gnu.org/gnu/sed/ sed-4.2.2 tar.gz ; then logn configure ./configure - log1 make + log1 make $MAKE_OPT log2 make install log2 make clean build_post @@ -1107,7 +1104,7 @@ function make_ocamlbuild { make_ocaml if build_prep https://github.com/ocaml/ocamlbuild/archive 0.12.0 tar.gz 1 ocamlbuild-0.12.0; then log2 make configure OCAML_NATIVE=true OCAMLBUILD_PREFIX=$PREFIXOCAML OCAMLBUILD_BINDIR=$PREFIXOCAML/bin OCAMLBUILD_LIBDIR=$PREFIXOCAML/lib - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1634,7 +1631,7 @@ function make_addon_bignums { installer_addon_section bignums "Bignums" "Coq library for fast arbitrary size numbers" "" # To make command lines shorter :-( echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local - log1 make all + log1 make $MAKE_OPT all log2 make install build_post fi @@ -1650,7 +1647,7 @@ function make_addon_equations { # Note: PATH is automatically saved/restored by build_prep / build_post PATH=$COQBIN:$PATH logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1696,7 +1693,7 @@ function make_addon_ltac2 { installer_addon_dependency ltac2 if build_prep_overlay ltac2; then installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactic language" "" - log1 make all + log1 make $MAKE_OPT all log2 make install build_post fi @@ -1709,7 +1706,7 @@ function make_addon_unicoq { if build_prep_overlay unicoq; then installer_addon_section unicoq "Unicoq" "Coq plugin for an enhanced unification algorithm" "" log1 coq_makefile -f Make -o Makefile - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1724,7 +1721,7 @@ function make_addon_mtac2 { if build_prep_overlay mtac2; then installer_addon_section mtac2 "Mtac-2" "Coq plugin for a typed tactic language for Coq." "" log1 coq_makefile -f _CoqProject -o Makefile - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1766,7 +1763,7 @@ function make_addon_menhirlib { echo -R . MenhirLib > _CoqProject ls -1 *.v >> _CoqProject log1 coq_makefile -f _CoqProject -o Makefile.coq - log1 make -f Makefile.coq all + log1 make -f Makefile.coq $MAKE_OPT all logn make-install make -f Makefile.coq install build_post fi @@ -1779,10 +1776,10 @@ function make_addon_compcert { make_menhir make_addon_menhirlib installer_addon_dependency_end - if build_prep_overlay CompCert; then + if build_prep_overlay compcert; then installer_addon_section compcert "CompCert" "ATTENTION: THIS IS NOT OPEN SOURCE! CompCert verified C compiler and Clightgen (required for using VST for your own code)" "off" logn configure ./configure -ignore-coq-version -clightgen -prefix "$PREFIXCOQ" -coqdevdir "$PREFIXCOQ/lib/coq/user-contrib/compcert" x86_32-cygwin - log1 make + log1 make $MAKE_OPT log2 make install logn install-license-1 install -D -T "LICENSE" "$PREFIXCOQ/lib/coq/user-contrib/compcert/LICENSE" logn install-license-2 install -D -T "LICENSE" "$PREFIXCOQ/lib/compcert/LICENSE" @@ -1807,8 +1804,8 @@ function install_addon_vst { install_glob "progs" '*.v' "$VSTDEST/progs/" install_glob "progs" '*.c' "$VSTDEST/progs/" install_glob "progs" '*.h' "$VSTDEST/progs/" - install_glob "veric" '*.v' "$VSTDEST/msl/" - install_glob "veric" '*.vo' "$VSTDEST/msl/" + install_glob "veric" '*.v' "$VSTDEST/veric/" + install_glob "veric" '*.vo' "$VSTDEST/veric/" # Install VST documentation files install_glob "." 'LICENSE' "$VSTDEST" @@ -1821,12 +1818,20 @@ function install_addon_vst { install_glob "." '_CoqProject-export' "$VSTDEST/progs" } +function vst_patch_compcert_refs { + find . -type f -name '*.v' -print0 | xargs -0 sed -E -i \ + -e 's/(Require\s+(Import\s+|Export\s+)*)compcert\./\1VST.compcert./g' \ + -e 's/From compcert Require/From VST.compcert Require/g' +} + function make_addon_vst { installer_addon_dependency vst - if build_prep_overlay VST; then + if build_prep_overlay vst; then installer_addon_section vst "VST" "ATTENTION: SOME INCLUDED COMPCERT PARTS ARE NOT OPEN SOURCE! Verified Software Toolchain for verifying C code" "off" - log1 coq_set_timeouts_1000 - log1 make IGNORECOQVERSION=true $MAKE_OPT + # log1 coq_set_timeouts_1000 + log1 vst_patch_compcert_refs + # The usage of the shell variable ARCH in VST collides with the usage in this shellscript + logn make env -u ARCH make IGNORECOQVERSION=true $MAKE_OPT log1 install_addon_vst build_post fi @@ -1851,9 +1856,9 @@ function make_addon_coquelicot { function make_addon_aactactics { installer_addon_dependency aac - if build_prep_overlay aactactics; then + if build_prep_overlay aac_tactics; then installer_addon_section aac "AAC" "Coq plugin for extensible associative and commutative rewriting" "" - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1894,7 +1899,7 @@ function make_addon_quickchick { installer_addon_dependency_end if build_prep_overlay quickchick; then installer_addon_section quickchick "QuickChick" "Coq plugin for randomized testing and counter example search" "" - log1 make + log1 make $MAKE_OPT log2 make install build_post fi diff --git a/dev/build/windows/patches_coq/VST.patch b/dev/build/windows/patches_coq/VST.patch new file mode 100755 index 0000000000..2c8c46373f --- /dev/null +++ b/dev/build/windows/patches_coq/VST.patch @@ -0,0 +1,15 @@ +diff --git a/Makefile b/Makefile +index 4a119042..fdfac13e 100755 +--- a/Makefile ++++ b/Makefile +@@ -76,8 +76,8 @@ endif + + COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend flocq exportclight $(BACKEND) + +-COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) compcert.$(d)) +-EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) compcert.$(d)) ++COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) VST.compcert.$(d)) ++EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) VST.compcert.$(d)) + + # for SSReflect + ifdef MATHCOMP 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 |