diff options
Diffstat (limited to 'dev')
64 files changed, 495 insertions, 767 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 diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 6663fbecf8..10b4f9b044 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -16,14 +16,12 @@ We are currently running tests on the following platforms: `./configure`. It should allow complying with this discipline without pain. -- Travis CI is used to test the compilation of Coq and run the test-suite on - macOS. - - AppVeyor is used to test the compilation of Coq and run the test-suite on Windows. - Azure Pipelines is used to test the compilation of Coq and run the - test-suite on Windows. It is expected to replace appveyor eventually. + test-suite on Windows and on macOS. It is expected to replace + appveyor eventually. You can anticipate the results of most of these tests prior to submitting your PR by running GitLab CI on your private branches. To do so follow these steps: diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index 470d07b27d..f26e0904bc 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -3,14 +3,15 @@ set -e -x APPVEYOR_OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c +NJOBS=2 wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz tar -xf opam64.tar.xz bash opam64/install.sh -opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing +opam init default -j $NJOBS -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing eval "$(opam env)" -opam install -y num ocamlfind ounit +opam install -j $NJOBS -y num ocamlfind ounit # Full regular Coq Build -cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte # && make -C test-suite all INTERACTIVE= # && make validate +cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make -j $NJOBS && make byte -j $NJOBS && make -j $NJOBS -C test-suite all INTERACTIVE= # && make validate diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index e0f4f50fa9..8dee465cf4 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -150,11 +150,11 @@ : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## -# formal-topology +# fiat_crypto_legacy ######################################################################## -: "${formal_topology_CI_REF:=ci}" -: "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology}" -: "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}" +: "${fiat_crypto_legacy_CI_REF:=sp2019latest}" +: "${fiat_crypto_legacy_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" +: "${fiat_crypto_legacy_CI_ARCHIVEURL:=${fiat_crypto_legacy_CI_GITURL}/archive}" ######################################################################## # coq_dpdgraph @@ -240,13 +240,6 @@ : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" ######################################################################## -# plugin_tutorial -######################################################################## -: "${plugin_tutorial_CI_REF:=master}" -: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}" -: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}" - -######################################################################## # menhirlib ######################################################################## : "${menhirlib_CI_REF:=master}" @@ -273,3 +266,26 @@ : "${relation_algebra_CI_REF:=master}" : "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}" : "${relation_algebra_CI_ARCHIVEURL:=${relation_algebra_CI_GITURL}/archive}" + +######################################################################## +# StructTact + InfSeqExt + Cheerios + Verdi + Verdi Raft +######################################################################## +: "${struct_tact_CI_REF:=master}" +: "${struct_tact_CI_GITURL:=https://github.com/uwplse/StructTact}" +: "${struct_tact_CI_ARCHIVEURL:=${struct_tact_CI_GITURL}/archive}" + +: "${inf_seq_ext_CI_REF:=master}" +: "${inf_seq_ext_CI_GITURL:=https://github.com/DistributedComponents/InfSeqExt}" +: "${inf_seq_ext_CI_ARCHIVEURL:=${inf_seq_ext_CI_GITURL}/archive}" + +: "${cheerios_CI_REF:=master}" +: "${cheerios_CI_GITURL:=https://github.com/uwplse/cheerios}" +: "${cheerios_CI_ARCHIVEURL:=${cheerios_CI_GITURL}/archive}" + +: "${verdi_CI_REF:=master}" +: "${verdi_CI_GITURL:=https://github.com/uwplse/verdi}" +: "${verdi_CI_ARCHIVEURL:=${verdi_CI_GITURL}/archive}" + +: "${verdi_raft_CI_REF:=master}" +: "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}" +: "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}" diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh index 6bf3138346..2af4b58201 100755 --- a/dev/ci/ci-fiat-crypto-legacy.sh +++ b/dev/ci/ci-fiat-crypto-legacy.sh @@ -4,11 +4,11 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" FORCE_GIT=1 -git_download fiat_crypto +git_download fiat_crypto_legacy fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display" fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display" -( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ +( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \ ./etc/ci/remove_autogenerated.sh && \ make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 7e8013be9b..bba17314f7 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -10,5 +10,9 @@ git_download fiat_crypto # building the executables. # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 +fiat_crypto_CI_TARGETS1="c-files printlite lite" +fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem" + ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ - ulimit -s 32768 && make new-pipeline c-files ) + ulimit -s 32768 && \ + make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} ) diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh deleted file mode 100755 index 8be5a06ed2..0000000000 --- a/dev/ci/ci-formal-topology.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download formal_topology - -( cd "${CI_BUILD_DIR}/formal_topology" && make ) diff --git a/dev/ci/ci-plugin_tutorial.sh b/dev/ci/ci-plugin_tutorial.sh deleted file mode 100755 index 6c26a71a21..0000000000 --- a/dev/ci/ci-plugin_tutorial.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download plugin_tutorial - -( cd "${CI_BUILD_DIR}/plugin_tutorial" && \ - pushd tuto0 && make && popd && \ - pushd tuto1 && make && popd && \ - pushd tuto2 && make && popd && \ - pushd tuto3 && make && popd ) diff --git a/dev/ci/ci-verdi-raft.sh b/dev/ci/ci-verdi-raft.sh new file mode 100755 index 0000000000..3bcd52c464 --- /dev/null +++ b/dev/ci/ci-verdi-raft.sh @@ -0,0 +1,24 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download struct_tact + +( cd "${CI_BUILD_DIR}/struct_tact" && ./configure && make && make install ) + +git_download inf_seq_ext + +( cd "${CI_BUILD_DIR}/inf_seq_ext" && ./configure && make && make install ) + +git_download cheerios + +( cd "${CI_BUILD_DIR}/cheerios" && ./configure && make && make install ) + +git_download verdi + +( cd "${CI_BUILD_DIR}/verdi" && ./configure && make && make install ) + +git_download verdi_raft + +( cd "${CI_BUILD_DIR}/verdi_raft" && ./configure && make ) diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh index 12a70176c2..9ca8f76054 100755 --- a/dev/ci/ci-wrapper.sh +++ b/dev/ci/ci-wrapper.sh @@ -6,13 +6,6 @@ set -eo pipefail -function travis_fold { - if [ -n "${TRAVIS}" ]; - then - echo "travis_fold:$1:$2" - fi -} - CI_NAME="$1" CI_SCRIPT="ci-${CI_NAME}.sh" @@ -22,6 +15,5 @@ cd "${DIR}/../.." export TIMED=1 "${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log -travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...' +echo 'Aggregating timing log...' python ./tools/make-one-time-file.py time-of-build.log -travis_fold 'end' 'coq.test.timing' diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index 386a3de204..5f819f31f9 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -26,12 +26,12 @@ if %ARCH% == 64 ( SET CYGROOT=C:\ci\cygwin%ARCH%
SET DESTCOQ=C:\ci\coq%ARCH%
+SET CYGCACHE=C:\ci\cache\cgwin
CALL :MakeUniqueFolder %CYGROOT% CYGROOT
CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
-SET CYGCACHE=%CYGROOT%\var\cache\setup
SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
SET COQREGTESTING=Y
@@ -49,10 +49,9 @@ IF "%WINDOWS%" == "enabled_all_addons" ( -addon=compcert ^
-addon=extlib ^
-addon=quickchick ^
- -addon=coquelicot
- REM addons with build issues
- REM -addon=vst ^
- REM -addon=aactactics ^
+ -addon=coquelicot ^
+ -addon=vst ^
+ -addon=aactactics
) ELSE (
SET "EXTRA_ADDONS= "
)
diff --git a/dev/ci/nix/CoLoR.nix b/dev/ci/nix/CoLoR.nix index 4c5cfd83da..3fcf177aec 100644 --- a/dev/ci/nix/CoLoR.nix +++ b/dev/ci/nix/CoLoR.nix @@ -1,5 +1,5 @@ { bignums }: { - buildInputs = [ bignums ]; + coqBuildInputs = [ bignums ]; } diff --git a/dev/ci/nix/Corn.nix b/dev/ci/nix/Corn.nix index 18c7750279..0d22a6b91b 100644 --- a/dev/ci/nix/Corn.nix +++ b/dev/ci/nix/Corn.nix @@ -1,5 +1,5 @@ { bignums, math-classes }: { - buildInputs = [ bignums math-classes ]; + coqBuildInputs = [ bignums math-classes ]; } diff --git a/dev/ci/nix/GeoCoq.nix b/dev/ci/nix/GeoCoq.nix index a86fb2c44a..45d688285e 100644 --- a/dev/ci/nix/GeoCoq.nix +++ b/dev/ci/nix/GeoCoq.nix @@ -1,5 +1,5 @@ { mathcomp }: { - buildInputs = [ mathcomp ]; + coqBuildInputs = [ mathcomp ]; configure = "./configure.sh"; } diff --git a/dev/ci/nix/README.md b/dev/ci/nix/README.md index 1685b084e9..6f32abef95 100644 --- a/dev/ci/nix/README.md +++ b/dev/ci/nix/README.md @@ -17,3 +17,10 @@ build-system of that project: `configure`, `make`, and `clean`. Therefore, after changing the working directory to the root of the sources of that project, the contents of these variables can be evaluated to respectively set-up, build, and clean the project. + +## Variant: nocoq + +The dependencies of the third-party developments are split into `buildInputs` +and `coqBuildInputs`. The second list gathers the Coq libraries. In case you +only want the non-coq dependencies (because you want to use Coq from your `PATH`), +set the environment variable `NOCOQ` to some non-empty value. diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index 4acfae48e4..277e9ee08f 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -2,7 +2,8 @@ , branch , wd , project ? "xyz" -, bn ? "release" +, withCoq ? true +, bn ? "master" }: with pkgs; @@ -16,6 +17,11 @@ let mathcomp = coqPackages.mathcomp.overrideAttrs (o: { name = "coq-git-mathcomp-git"; src = fetchTarball https://github.com/math-comp/math-comp/archive/master.tar.gz; }); in +let ssreflect = coqPackages.ssreflect.overrideAttrs (o: { + inherit (mathcomp) src; + }); in +let coq-ext-lib = coqPackages.coq-ext-lib; in +let simple-io = coqPackages.simple-io; in let bignums = coqPackages.bignums.overrideAttrs (o: if bn == "release" then {} else if bn == "master" then { src = fetchTarball https://github.com/coq/bignums/archive/master.tar.gz; } else @@ -28,9 +34,17 @@ let math-classes = src = fetchTarball "https://github.com/coq-community/math-classes/archive/master.tar.gz"; }); in -let unicoq = callPackage ./unicoq.nix { inherit coq; }; in +let corn = (coqPackages.corn.override { inherit coq bignums math-classes; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/coq-community/corn/archive/master.tar.gz"; + }); in + +let unicoq = callPackage ./unicoq { inherit coq; }; in -let callPackage = newScope { inherit coq mathcomp bignums coqprime math-classes unicoq; }; in +let callPackage = newScope { inherit coq + bignums coq-ext-lib coqprime corn math-classes + mathcomp simple-io ssreflect unicoq; +}; in # Environments for building CI libraries with this Coq let projects = { @@ -45,12 +59,14 @@ let projects = { fiat_crypto = callPackage ./fiat_crypto.nix {}; fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {}; flocq = callPackage ./flocq.nix {}; + formal-topology = callPackage ./formal-topology.nix {}; GeoCoq = callPackage ./GeoCoq.nix {}; HoTT = callPackage ./HoTT.nix {}; math_classes = callPackage ./math_classes.nix {}; mathcomp = {}; mtac2 = callPackage ./mtac2.nix {}; oddorder = callPackage ./oddorder.nix {}; + quickchick = callPackage ./quickchick.nix {}; VST = callPackage ./VST.nix {}; }; in @@ -60,10 +76,16 @@ else let prj = projects."${project}"; in +let inherit (stdenv.lib) optional optionals; in + stdenv.mkDerivation { name = "shell-for-${project}-in-${branch}"; - buildInputs = [ coq ] ++ (prj.buildInputs or []); + buildInputs = + optional withCoq coq + ++ (prj.buildInputs or []) + ++ optionals withCoq (prj.coqBuildInputs or []) + ; configure = prj.configure or "true"; make = prj.make or "make"; diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix index 7b37e6e8e4..0f0ee91387 100644 --- a/dev/ci/nix/fiat_crypto.nix +++ b/dev/ci/nix/fiat_crypto.nix @@ -1,6 +1,6 @@ { coqprime }: { - buildInputs = [ coqprime ]; + coqBuildInputs = [ coqprime ]; configure = "git submodule update --init --recursive && ulimit -s 32768"; make = "make new-pipeline c-files"; } diff --git a/dev/ci/nix/formal-topology.nix b/dev/ci/nix/formal-topology.nix new file mode 100644 index 0000000000..53b9b1182b --- /dev/null +++ b/dev/ci/nix/formal-topology.nix @@ -0,0 +1,4 @@ +{ corn }: +{ + coqBuildInputs = [ corn ]; +} diff --git a/dev/ci/nix/math_classes.nix b/dev/ci/nix/math_classes.nix index b0fa2fe795..8edc3c8358 100644 --- a/dev/ci/nix/math_classes.nix +++ b/dev/ci/nix/math_classes.nix @@ -1,6 +1,6 @@ { bignums }: { - buildInputs = [ bignums ]; + coqBuildInputs = [ bignums ]; configure = "./configure.sh"; } diff --git a/dev/ci/nix/mtac2.nix b/dev/ci/nix/mtac2.nix index 9a2353c5cf..4acc326c02 100644 --- a/dev/ci/nix/mtac2.nix +++ b/dev/ci/nix/mtac2.nix @@ -1,5 +1,6 @@ { coq, unicoq }: { - buildInputs = [ unicoq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]); + buildInputs = with coq.ocamlPackages; [ ocaml findlib camlp5 ]; + coqBuildInputs = [ unicoq ]; configure = "./configure.sh"; } diff --git a/dev/ci/nix/oddorder.nix b/dev/ci/nix/oddorder.nix index 3b8fdbab51..2341bb3173 100644 --- a/dev/ci/nix/oddorder.nix +++ b/dev/ci/nix/oddorder.nix @@ -1,4 +1,4 @@ { mathcomp }: { - buildInputs = [ mathcomp ]; + coqBuildInputs = [ mathcomp ]; } diff --git a/dev/ci/nix/quickchick.nix b/dev/ci/nix/quickchick.nix new file mode 100644 index 0000000000..46bf02ae3c --- /dev/null +++ b/dev/ci/nix/quickchick.nix @@ -0,0 +1,5 @@ +{ ocamlPackages, ssreflect, coq-ext-lib, simple-io }: +{ + buildInputs = with ocamlPackages; [ ocaml findlib ocamlbuild num ]; + coqBuildInputs = [ ssreflect coq-ext-lib simple-io ]; +} diff --git a/dev/ci/nix/shell b/dev/ci/nix/shell index 2e4462ed40..a5f8ee8f54 100755 --- a/dev/ci/nix/shell +++ b/dev/ci/nix/shell @@ -17,4 +17,10 @@ else BN="" fi -nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN +if [ "$NOCOQ" ]; then + NOCOQ="--arg withCoq false" +else + NOCOQ="" +fi + +nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN $NOCOQ diff --git a/dev/ci/nix/unicoq/META b/dev/ci/nix/unicoq/META new file mode 100644 index 0000000000..30dd8b5559 --- /dev/null +++ b/dev/ci/nix/unicoq/META @@ -0,0 +1,2 @@ +archive(native) = "unicoq.cmxa" +plugin(native) = "unicoq.cmxs" diff --git a/dev/ci/nix/unicoq.nix b/dev/ci/nix/unicoq/default.nix index 093c262cde..36f40dbe33 100644 --- a/dev/ci/nix/unicoq.nix +++ b/dev/ci/nix/unicoq/default.nix @@ -4,8 +4,16 @@ stdenv.mkDerivation { name = "coq${coq.coq-version}-unicoq-0.0-git"; src = fetchTarball https://github.com/unicoq/unicoq/archive/master.tar.gz; + patches = [ ./unicoq-num.patch ]; + buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]); configurePhase = "coq_makefile -f Make -o Makefile"; installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + postInstall = '' + install -d $OCAMLFIND_DESTDIR + ln -s $out/lib/coq/${coq.coq-version}/user-contrib/Unicoq $OCAMLFIND_DESTDIR/ + install -m 0644 ${./META} src/unicoq.a $OCAMLFIND_DESTDIR/Unicoq + ''; } diff --git a/dev/ci/nix/unicoq/unicoq-num.patch b/dev/ci/nix/unicoq/unicoq-num.patch new file mode 100644 index 0000000000..6d96d94dfc --- /dev/null +++ b/dev/ci/nix/unicoq/unicoq-num.patch @@ -0,0 +1,44 @@ +commit f29bc64ee3d8b36758d17e1f5d50812e0c93063b +Author: Vincent Laporte <Vincent.Laporte@fondation-inria.fr> +Date: Thu Nov 29 08:59:22 2018 +0000 + + Make explicit dependency to num + +diff --git a/Make b/Make +index 550dc6a..8aa1309 100644 +--- a/Make ++++ b/Make +@@ -9,7 +9,7 @@ src/logger.ml + src/munify.mli + src/munify.ml + src/unitactics.mlg +-src/unicoq.mllib ++src/unicoq.mlpack + theories/Unicoq.v + test-suite/munifytest.v + test-suite/microtests.v +diff --git a/Makefile.local b/Makefile.local +new file mode 100644 +index 0000000..88be365 +--- /dev/null ++++ b/Makefile.local +@@ -0,0 +1 @@ ++CAMLPKGS += -package num +diff --git a/src/unicoq.mllib b/src/unicoq.mllib +deleted file mode 100644 +index 2b84e2d..0000000 +--- a/src/unicoq.mllib ++++ /dev/null +@@ -1,3 +0,0 @@ +-Logger +-Munify +-Unitactics +diff --git a/src/unicoq.mlpack b/src/unicoq.mlpack +new file mode 100644 +index 0000000..2b84e2d +--- /dev/null ++++ b/src/unicoq.mlpack +@@ -0,0 +1,3 @@ ++Logger ++Munify ++Unitactics diff --git a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh new file mode 100644 index 0000000000..ebd1b524da --- /dev/null +++ b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "9263" ] || [ "$CI_BRANCH" = "parsing-state" ]; then + + mtac2_CI_REF=proof-mode + mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2 + + ltac2_CI_REF=proof-mode + ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 + + equations_CI_REF=proof-mode + equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations + +fi diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 56fdab0c26..5705857d76 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -93,7 +93,7 @@ put the approriate label. Otherwise, they are expected to merge the PR using the When CI has a few failures which look spurious, restarting the corresponding jobs is a good way of ensuring this was indeed the case. -To restart a job on Travis or on AppVeyor, you should connect using your GitHub +To restart a job on AppVeyor, you should connect using your GitHub account; being part of the Coq organization on GitHub should give you the permission to do so. To restart a job on GitLab CI, you should sign into GitLab (this can be done diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt index 29e87df6b8..8455d13377 100644 --- a/dev/doc/profiling.txt +++ b/dev/doc/profiling.txt @@ -10,7 +10,7 @@ In Coq source folder: opam switch 4.05.0+trunk+fp ./configure -local -debug make -perf record -g bin/coqtop -compile file.v +perf record -g bin/coqc file.v perf report -g fractal,callee --no-children To profile only part of a file, first load it using @@ -96,7 +96,7 @@ https://github.com/mshinwell/opam-repo-dev ### For memory dump: -CAMLRUNPARAM=T,mj bin/coqtop -compile file.v +CAMLRUNPARAM=T,mj bin/coqc file.v In another terminal: @@ -112,7 +112,7 @@ number of objects and third is the place where the objects where allocated. ### For complete memory graph: -CAMLRUNPARAM=T,gr bin/coqtop -compile file.v +CAMLRUNPARAM=T,gr bin/coqc file.v In another terminal: diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index b1c111685b..d05b6c8eef 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -4,37 +4,20 @@ - [ ] Create a new issue to track the release process where you can copy-paste the present checklist. -- [ ] Change the version name to the next major version and the magic numbers - (see [#7008](https://github.com/coq/coq/pull/7008/files)). -- [ ] Update the compatibility infrastructure, which consists of doing - the following steps. Note that all but the final step can be - performed automatically by - [`dev/tools/update-compat.py`](/dev/tools/update-compat.py) so - long as you have already updated `coq_version` in - [`configure.ml`](/configure.ml). - + [ ] Add a file `theories/Compat/CoqXX.v` which contains just the header - from [`dev/header.ml`](/dev/header.ml) - + [ ] Add the line `Require Export Coq.Compat.CoqXX.` at the top of - `theories/Compat/CoqYY.v`, where Y.Y is the version prior to X.X. - + [ ] Delete the file `theories/Compat/CoqWW.v`, where W.W is three versions - prior to X.X. - + [ ] Update - [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template) - with the deleted/added files. - + [ ] Remove any notations in the standard library which have `compat "W.W"`. - + [ ] Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by - bumping all the version numbers by one, and update the interpretations - of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and - [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg). - + [ ] Update the files - [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v), - [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v), - and - [`test-suite/success/CompatOldFlag.v`](/test-suite/success/CompatOldFlag.v) - by bumping all version numbers by 1. - + [ ] Decide what to do about all test-suite files which mention `-compat - W.W` or `Coq.Comapt.CoqWW` (which is no longer valid, since we only - keep compatibility against the two previous versions) +- [ ] Change the version name to the next major version and the magic + numbers (see [#7008](https://github.com/coq/coq/pull/7008/files)). + + Additionally, in the same commit, update the compatibility + infrastructure, which consists of invoking + [`dev/tools/update-compat.py`](../tools/update-compat.py) with the + `--master` flag. + + Note that the `update-compat.py` script must be run twice: once + *immediately after* branching with the `--master` flag (which sets + up Coq to support four `-compat` flag arguments), *in the same + commit* as the one that updates `coq_version` in + [`configure.ml`](../../configure.ml), and once again later on before + the next branch point with the `--release` flag (see next section). - [ ] Put the corresponding alpha tag using `git tag -s`. The `VX.X+alpha` tag marks the first commit to be in `master` and not in the branch of the previous version. @@ -43,6 +26,19 @@ release date) and put this information in the milestone (using the description and due date fields). +## Anytime after the previous version is branched off master ## + +- [ ] Update the compatibility infrastructure to the next release, + which consists of invoking + [`dev/tools/update-compat.py`](../tools/update-compat.py) with the + `--release` flag; this sets up Coq to support three `-compat` flag + arguments. To ensure that CI passes, you will have to decide what + to do about all test-suite files which mention `-compat U.U` or + `Coq.Comapt.CoqUU` (which is no longer valid, since we only keep + compatibility against the two previous versions on releases), and + you may have to prepare overlays for projects using the + compatibility flags. + ## About one month before the beta ## - [ ] Create the `X.X.0` milestone and set its due date. diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex index 8f9c3171da..1c4913d201 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/versions-history.tex @@ -271,7 +271,7 @@ Coq ``V7'' archive & August 1999 & new cvs archive based on J.-C. Filliâtre's \ & & \feature{kernel-centric} architecture \\ & & more care for outside readers\\ & & (indentation, ocaml warning protection)\\ -Coq V7.0beta& released 27 December 2000 & \feature{${\cal L}_{\mathit{tac}}$} \\ +Coq V7.0beta& released 27 December 2000 & \feature{${\mathcal{L}}_{\mathit{tac}}$} \\ Coq V7.0beta2& released 2 February 2001\\ Coq V7.0& released 25 April 2001 & \feature{extraction} (version 2) [6-2-2001] \\ diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 5fd8a3b7d9..72e2930386 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -143,7 +143,7 @@ fi # Sanity check: PR has an outdated version of CI BASE_COMMIT=$(echo "$PRDATA" | jq -r '.base.sha') -CI_FILES=(".travis.yml" ".gitlab-ci.yml" "appveyor.yml") +CI_FILES=(".gitlab-ci.yml" "appveyor.yml") if ! git diff --quiet "$BASE_COMMIT" "$LOCAL_BRANCH_COMMIT" -- "${CI_FILES[@]}" then @@ -198,8 +198,26 @@ if [ -z "$(git config user.signingkey)" ]; then warning "gpg will guess a key out of your git config user.* data" fi +# Generate commit message + +info "Fetching review data" +reviews=$(curl -s "$API/pulls/$PR/reviews") +msg="Merge PR #$PR: $TITLE" + +has_state() { + [ "$(jq -rc 'map(select(.user.login == "'"$1"'") | .state) | any(. == "'"$2"'")' <<< "$reviews")" = true ] +} + +for reviewer in $(jq -rc 'map(.user.login) | unique | join(" ")' <<< "$reviews" ); do + if has_state "$reviewer" APPROVED; then + msg=$(printf '%s\n' "$msg" | git interpret-trailers --trailer Reviewed-by="$reviewer") + elif has_state "$reviewer" COMMENTED; then + msg=$(printf '%s\n' "$msg" | git interpret-trailers --trailer Ack-by="$reviewer") + fi +done + info "merging" -git merge -v -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $TITLE" -e +git merge -v -S --no-ff FETCH_HEAD -m "$msg" -e # TODO: improve this check if ! git diff --quiet --diff-filter=A "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci/user-overlays; then diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py index 14094553a2..ff9b32fe78 100755 --- a/dev/tools/update-compat.py +++ b/dev/tools/update-compat.py @@ -1,6 +1,60 @@ #!/usr/bin/env python from __future__ import with_statement -import os, re, sys +import os, re, sys, subprocess + +# When passed `--release`, this script sets up Coq to support three +# `-compat` flag arguments. If executed manually, this would consist +# of doing the following steps: +# +# - Delete the file `theories/Compat/CoqUU.v`, where U.U is four +# versions prior to the new version X.X. After this, there +# should be exactly three `theories/Compat/CoqNN.v` files. +# - Update +# [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template) +# with the deleted file. +# - Remove any notations in the standard library which have `compat "U.U"`. +# - Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by +# bumping all the version numbers by one, and update the interpretations +# of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and +# [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg). +# +# - Remove the file +# [`test-suite/success/CompatOldOldFlag.v`](/test-suite/success/CompatOldOldFlag.v). +# - Update +# [`test-suite/tools/update-compat/run.sh`](/test-suite/tools/update-compat/run.sh) +# to ensure that it passes `--release` to the `update-compat.py` +# script. + +# When passed the `--master` flag, this script sets up Coq to support +# four `-compat` flag arguments. If executed manually, this would +# consist of doing the following steps: +# +# - Add a file `theories/Compat/CoqXX.v` which contains just the header +# from [`dev/header.ml`](/dev/header.ml) +# - Add the line `Require Export Coq.Compat.CoqXX.` at the top of +# `theories/Compat/CoqYY.v`, where Y.Y is the version prior to X.X. +# - Update +# [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template) +# with the added file. +# - Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by +# bumping all the version numbers by one, and update the interpretations +# of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and +# [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg). +# - Update the files +# [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v), +# [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v), +# and +# [`test-suite/success/CompatOldFlag.v`](/test-suite/success/CompatOldFlag.v) +# by bumping all version numbers by 1. Re-create the file +# [`test-suite/success/CompatOldOldFlag.v`](/test-suite/success/CompatOldOldFlag.v) +# with its version numbers also bumped by 1 (file should have +# been removed before branching; see above). +# - Update +# [`test-suite/tools/update-compat/run.sh`](/test-suite/tools/update-compat/run.sh) +# to ensure that it passes `--master` to the `update-compat.py` +# script. + + # Obtain the absolute path of the script being run. By assuming that # the script lives in dev/tools/, and basing all calls on the path of @@ -11,6 +65,8 @@ ROOT_PATH = os.path.realpath(os.path.join(SCRIPT_PATH, '..', '..')) CONFIGURE_PATH = os.path.join(ROOT_PATH, 'configure.ml') HEADER_PATH = os.path.join(ROOT_PATH, 'dev', 'header.ml') DEFAULT_NUMBER_OF_OLD_VERSIONS = 2 +RELEASE_NUMBER_OF_OLD_VERSIONS = 2 +MASTER_NUMBER_OF_OLD_VERSIONS = 3 EXTRA_HEADER = '\n(** Compatibility file for making Coq act similar to Coq v%s *)\n' FLAGS_MLI_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.mli') FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml') @@ -18,18 +74,46 @@ COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml') G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg') DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template') BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_4798.v') +BUG_9166_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_9166.v') +TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh') TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i) for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v')) TEST_SUITE_DESCRIPTIONS = ('current-minus-three', 'current-minus-two', 'current-minus-one', 'current') # sanity check that we are where we think we are assert(os.path.normpath(os.path.realpath(SCRIPT_PATH)) == os.path.normpath(os.path.realpath(os.path.join(ROOT_PATH, 'dev', 'tools')))) assert(os.path.exists(CONFIGURE_PATH)) +BUG_HEADER = r"""(* DO NOT MODIFY THIS FILE DIRECTLY *) +(* It is autogenerated by %s. *) +""" % os.path.relpath(os.path.realpath(__file__), ROOT_PATH) def get_header(): with open(HEADER_PATH, 'r') as f: return f.read() HEADER = get_header() +def break_or_continue(): + msg = 'Press ENTER to continue, or Ctrl+C to break...' + try: + raw_input(msg) + except NameError: # we must be running python3 + input(msg) + +def maybe_git_add(local_path, suggest_add=True, **args): + if args['git_add']: + print("Running 'git add %s'..." % local_path) + retc = subprocess.call(['git', 'add', local_path], cwd=ROOT_PATH) + if retc is not None and retc != 0: + print('!!! Process returned code %d' % retc) + elif suggest_add: + print(r"!!! Don't forget to 'git add %s'!" % local_path) + +def maybe_git_rm(local_path, **args): + if args['git_add']: + print("Running 'git rm %s'..." % local_path) + retc = subprocess.call(['git', 'rm', local_path], cwd=ROOT_PATH) + if retc is not None and retc != 0: + print('!!! Process returned code %d' % retc) + def get_version(cur_version=None): if cur_version is not None: return cur_version with open(CONFIGURE_PATH, 'r') as f: @@ -72,11 +156,56 @@ def get_known_versions(): def get_new_versions(known_versions, **args): if args['cur_version'] in known_versions: assert(known_versions[-1] == args['cur_version']) - assert(len(known_versions) == args['number_of_compat_versions']) - return known_versions + known_versions = known_versions[:-1] assert(len(known_versions) >= args['number_of_old_versions']) return tuple(list(known_versions[-args['number_of_old_versions']:]) + [args['cur_version']]) +def print_diff(olds, news, numch=30): + for ch in range(min(len(olds), len(news))): + if olds[ch] != news[ch]: + print('Character %d differs:\nOld: %s\nNew: %s' % (ch, repr(olds[ch:][:numch]), repr(news[ch:][numch]))) + return + ch = min(len(olds), len(news)) + assert(len(olds) != len(news)) + print('Strings are different lengths:\nOld tail: %s\nNew tail: %s' % (repr(olds[ch:]), repr(news[ch:]))) + +def update_shebang_to_match(contents, new_contents, path): + contents_lines = contents.split('\n') + new_contents_lines = new_contents.split('\n') + if not (contents_lines[0].startswith('#!/') and contents_lines[0].endswith('bash')): + raise Exception('Unrecognized #! line in existing %s: %s' % (os.path.relpath(path, ROOT_PATH), repr(contents_lines[0]))) + if not (new_contents_lines[0].startswith('#!/') and new_contents_lines[0].endswith('bash')): + raise Exception('Unrecognized #! line in new %s: %s' % (os.path.relpath(path, ROOT_PATH), repr(new_contents_lines[0]))) + new_contents_lines[0] = contents_lines[0] + return '\n'.join(new_contents_lines) + +def update_if_changed(contents, new_contents, path, exn_string='%s changed!', suggest_add=False, pass_through_shebang=False, assert_unchanged=False, **args): + if contents is not None and pass_through_shebang: + new_contents = update_shebang_to_match(contents, new_contents, path) + if contents is None or contents != new_contents: + if not assert_unchanged: + print('Updating %s...' % os.path.relpath(path, ROOT_PATH)) + with open(path, 'w') as f: + f.write(new_contents) + maybe_git_add(os.path.relpath(path, ROOT_PATH), suggest_add=suggest_add, **args) + else: + if contents is not None: + print('Unexpected change:\nOld contents:\n%s\n\nNew contents:\n%s\n' % (contents, new_contents)) + print_diff(contents, new_contents) + raise Exception(exn_string % os.path.relpath(path, ROOT_PATH)) + +def remove_if_exists(path, exn_string='%s exists when it should not!', assert_unchanged=False, **args): + if os.path.exists(path): + if not assert_unchanged: + print('Removing %s...' % os.path.relpath(path, ROOT_PATH)) + os.remove(path) + maybe_git_rm(os.path.relpath(path, ROOT_PATH), **args) + else: + raise Exception(exn_string % os.path.relpath(path, ROOT_PATH)) + +def update_file(new_contents, path, **args): + update_if_changed(None, new_contents, path, **args) + def update_compat_files(old_versions, new_versions, assert_unchanged=False, **args): for v in old_versions: if v not in new_versions: @@ -85,6 +214,7 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar print('Removing %s...' % compat_file) compat_path = os.path.join(ROOT_PATH, compat_file) os.rename(compat_path, compat_path + '.bak') + maybe_git_rm(compat_file, **args) else: raise Exception('%s exists!' % compat_file) for v, next_v in zip(new_versions, list(new_versions[1:]) + [None]): @@ -95,12 +225,7 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar contents = HEADER + (EXTRA_HEADER % v) if next_v is not None: contents += '\nRequire Export Coq.Compat.%s.\n' % version_name_to_compat_name(next_v, ext='') - if not assert_unchanged: - with open(compat_path, 'w') as f: - f.write(contents) - print(r"Don't forget to 'git add %s'!" % compat_file) - else: - raise Exception('%s does not exist!' % compat_file) + update_file(contents, compat_path, exn_string='%s does not exist!', assert_unchanged=assert_unchanged, **args) else: # print('Checking %s...' % compat_file) with open(compat_path, 'r') as f: @@ -116,12 +241,7 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar if not contents.startswith(header + '\n'): contents = contents.replace(header, header + '\n') contents = contents.replace(header, '%s\n%s' % (header, line)) - if not assert_unchanged: - print('Updating %s...' % compat_file) - with open(compat_path, 'w') as f: - f.write(contents) - else: - raise Exception('Compat file %s is missing line %s' % (compat_file, line)) + update_file(contents, compat_path, exn_string=('Compat file %%s is missing line %s' % line), assert_unchanged=assert_unchanged, **args) def update_compat_versions_type_line(new_versions, contents, relpath): compat_version_string = ' | '.join(['V%s_%s' % tuple(v.split('.')) for v in new_versions[:-1]] + ['Current']) @@ -173,11 +293,18 @@ def update_add_compat_require(new_versions, contents, relpath): return new_contents def update_parse_compat_version(new_versions, contents, relpath, **args): - line_count = args['number_of_compat_versions']+2 # 1 for the first line, 1 for the invalid flags + line_count = 3 # 1 for the first line, 1 for the invalid flags, and 1 for Current first_line = 'let parse_compat_version = let open Flags in function' - old_function_lines = contents[contents.index(first_line):].split('\n')[:line_count] - if re.match(r'^ \| \([0-9 "\.\|]*\) as s ->$', old_function_lines[-1]) is None: - raise Exception('Could not recognize line %d of parse_compat_version in %s as a list of invalid versions' % (line_count, relpath)) + split_contents = contents[contents.index(first_line):].split('\n') + while True: + cur_line = split_contents[:line_count][-1] + if re.match(r'^ \| \([0-9 "\.\|]*\) as s ->$', cur_line) is not None: + break + elif re.match(r'^ \| "[0-9\.]*" -> V[0-9_]*$', cur_line) is not None: + line_count += 1 + else: + raise Exception('Could not recognize line %d of parse_compat_version in %s as a list of invalid versions (line was %s)' % (line_count, relpath, repr(cur_line))) + old_function_lines = split_contents[:line_count] all_versions = re.findall(r'"([0-9\.]+)"', ''.join(old_function_lines)) invalid_versions = tuple(i for i in all_versions if i not in new_versions) new_function_lines = [first_line] @@ -197,15 +324,6 @@ def check_no_old_versions(old_versions, new_versions, contents, relpath): if V in contents: raise Exception('Unreplaced usage of %s remaining in %s' % (V, relpath)) -def update_if_changed(contents, new_contents, path, assert_unchanged=False, **args): - if contents != new_contents: - if not assert_unchanged: - print('Updating %s...' % os.path.relpath(path, ROOT_PATH)) - with open(path, 'w') as f: - f.write(new_contents) - else: - raise Exception('%s changed!' % os.path.relpath(path, ROOT_PATH)) - def update_flags_mli(old_versions, new_versions, **args): with open(FLAGS_MLI_PATH, 'r') as f: contents = f.read() new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH)) @@ -238,21 +356,26 @@ def update_flags(old_versions, new_versions, **args): update_coqargs_ml(old_versions, new_versions, **args) update_g_vernac(old_versions, new_versions, **args) -def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TEST_SUITE_PATHS, test_suite_descriptions=TEST_SUITE_DESCRIPTIONS, **args): +def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TEST_SUITE_PATHS, test_suite_descriptions=TEST_SUITE_DESCRIPTIONS, test_suite_outdated_paths=tuple(), **args): assert(len(new_versions) == len(test_suite_paths)) assert(len(new_versions) == len(test_suite_descriptions)) for i, (v, path, descr) in enumerate(zip(new_versions, test_suite_paths, test_suite_descriptions)): - if not os.path.exists(path): - raise Exception('Could not find existing file %s' % os.path.relpath(path, ROOT_PATH)) + contents = None + suggest_add = False + if os.path.exists(path): + with open(path, 'r') as f: contents = f.read() + else: + suggest_add = True if '%s' in descr: descr = descr % v - with open(path, 'r') as f: contents = f.read() lines = ['(* -*- coq-prog-args: ("-compat" "%s") -*- *)' % v, '(** Check that the %s compatibility flag actually requires the relevant modules. *)' % descr] for imp_v in reversed(new_versions[i:]): lines.append('Import Coq.Compat.%s.' % version_name_to_compat_name(imp_v, ext='')) lines.append('') new_contents = '\n'.join(lines) - update_if_changed(contents, new_contents, path, **args) + update_if_changed(contents, new_contents, path, suggest_add=suggest_add, **args) + for path in test_suite_outdated_paths: + remove_if_exists(path, assert_unchanged=assert_unchanged, **args) def update_doc_index(new_versions, **args): with open(DOC_INDEX_PATH, 'r') as f: contents = f.read() @@ -264,17 +387,48 @@ def update_doc_index(new_versions, **args): new_contents = new_contents.replace(firstline, '\n'.join([firstline] + extra_lines)) update_if_changed(contents, new_contents, DOC_INDEX_PATH, **args) +def update_test_suite_run(**args): + with open(TEST_SUITE_RUN_PATH, 'r') as f: contents = f.read() + new_contents = r'''#!/usr/bin/env bash + +# allow running this script from any directory by basing things on where the script lives +SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )" + +# we assume that the script lives in test-suite/tools/update-compat/, +# and that update-compat.py lives in dev/tools/ +cd "${SCRIPT_DIR}/../../.." +dev/tools/update-compat.py --assert-unchanged %s || exit $? +''' % ' '.join([('--master' if args['master'] else ''), ('--release' if args['release'] else '')]).strip() + update_if_changed(contents, new_contents, TEST_SUITE_RUN_PATH, pass_through_shebang=True, **args) + def update_bug_4789(new_versions, **args): # we always update this compat notation to oldest # currently-supported compat version, which should never be the # current version with open(BUG_4798_PATH, 'r') as f: contents = f.read() - new_contents = r"""Check match 2 with 0 => 0 | S n => n end. + new_contents = BUG_HEADER + r"""Check match 2 with 0 => 0 | S n => n end. Notation "|" := 1 (compat "%s"). Check match 2 with 0 => 0 | S n => n end. (* fails *) """ % new_versions[0] update_if_changed(contents, new_contents, BUG_4798_PATH, **args) +def update_bug_9166(new_versions, **args): + # we always update this compat notation to oldest + # currently-supported compat version, which should never be the + # current version + with open(BUG_9166_PATH, 'r') as f: contents = f.read() + new_contents = BUG_HEADER + r"""Set Warnings "+deprecated". + +Notation bar := option (compat "%s"). + +Definition foo (x: nat) : nat := + match x with + | 0 => 0 + | S bar => bar + end. +""" % new_versions[0] + update_if_changed(contents, new_contents, BUG_9166_PATH, **args) + def update_compat_notations_in(old_versions, new_versions, contents): for v in old_versions: if v not in new_versions: @@ -305,11 +459,26 @@ def parse_args(argv): args = { 'assert_unchanged': False, 'cur_version': None, - 'number_of_old_versions': DEFAULT_NUMBER_OF_OLD_VERSIONS + 'number_of_old_versions': None, + 'master': False, + 'release': False, + 'git_add': False, } + if '--master' not in argv and '--release' not in argv: + print(r'''WARNING: You should pass either --release (sometime before branching) + or --master (right after branching and updating the version number in version.ml)''') + if '--assert-unchanged' not in args: break_or_continue() for arg in argv[1:]: if arg == '--assert-unchanged': args['assert_unchanged'] = True + elif arg == '--git-add': + args['git_add'] = True + elif arg == '--master': + args['master'] = True + if args['number_of_old_versions'] is None: args['number_of_old_versions'] = MASTER_NUMBER_OF_OLD_VERSIONS + elif arg == '--release': + args['release'] = True + if args['number_of_old_versions'] is None: args['number_of_old_versions'] = RELEASE_NUMBER_OF_OLD_VERSIONS elif arg.startswith('--cur-version='): args['cur_version'] = arg[len('--cur-version='):] assert(len(args['cur_version'].split('.')) == 2) @@ -317,10 +486,11 @@ def parse_args(argv): elif arg.startswith('--number-of-old-versions='): args['number_of_old_versions'] = int(arg[len('--number-of-old-versions='):]) else: - print('USAGE: %s [--assert-unchanged] [--cur-version=NN.NN] [--number-of-old-versions=NN]' % argv[0]) + print('USAGE: %s [--assert-unchanged] [--cur-version=NN.NN] [--number-of-old-versions=NN] [--git-add]' % argv[0]) print('') print('ERROR: Unrecognized argument: %s' % arg) sys.exit(1) + if args['number_of_old_versions'] is None: args['number_of_old_versions'] = DEFAULT_NUMBER_OF_OLD_VERSIONS return args if __name__ == '__main__': @@ -331,11 +501,14 @@ if __name__ == '__main__': new_versions = get_new_versions(known_versions, **args) assert(len(TEST_SUITE_PATHS) >= args['number_of_compat_versions']) args['test_suite_paths'] = tuple(TEST_SUITE_PATHS[-args['number_of_compat_versions']:]) + args['test_suite_outdated_paths'] = tuple(TEST_SUITE_PATHS[:-args['number_of_compat_versions']]) args['test_suite_descriptions'] = tuple(TEST_SUITE_DESCRIPTIONS[-args['number_of_compat_versions']:]) update_compat_files(known_versions, new_versions, **args) update_flags(known_versions, new_versions, **args) update_test_suite(new_versions, **args) + update_test_suite_run(**args) update_doc_index(new_versions, **args) update_bug_4789(new_versions, **args) + update_bug_9166(new_versions, **args) update_compat_notations(known_versions, new_versions, **args) display_git_grep(known_versions, new_versions) |