diff options
70 files changed, 304 insertions, 766 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 2a641263e3..275d6c1ff5 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -30,10 +30,9 @@ # Trick to avoid getting review requests # each time someone adds an overlay -/appveyor.yml @maximedenes -/dev/ci/appveyor.* @maximedenes -/dev/ci/*.bat @maximedenes -# Secondary maintainer @SkySkimmer +/appveyor.yml @coq/ci-maintainers +/dev/ci/appveyor.* @coq/ci-maintainers +/dev/ci/*.bat @coq/ci-maintainers *.nix @coq/nix-maintainers @@ -71,7 +70,7 @@ azure-pipelines.yml @coq/ci-maintainers /man/ @silene # Secondary maintainer @maximedenes -/doc/plugin_tutorial/ @ybertot +/doc/plugin_tutorial/ @coq/plugin-tutorial-maintainers ########## Coqchk ########## diff --git a/.gitignore b/.gitignore index dfecfec837..2e5529ccfb 100644 --- a/.gitignore +++ b/.gitignore @@ -134,7 +134,6 @@ coqpp/coqpp_parse.mli g_*.ml -lib/coqProject_file.ml plugins/ltac/coretactics.ml plugins/ltac/extratactics.ml plugins/ltac/extraargs.ml diff --git a/CHANGES.md b/CHANGES.md index ae67eb5d1b..bcdb951a94 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -96,6 +96,11 @@ Vernacular commands - Computation of implicit arguments now properly handles local definitions in the binders for an `Instance`. +- `Declare Instance` now requires an instance name. + +- Option `Refine Instance Mode` has been turned off by default, meaning that + `Instance` no longer opens a proof when a body is provided. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: diff --git a/azure-pipelines.yml b/azure-pipelines.yml index e217601ae2..a8b42cc722 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -1,31 +1,78 @@ -pool: - vmImage: 'vs2017-win2016' - -steps: -- checkout: self - fetchDepth: 10 - -# cygwin package list not checked for minimality -- script: | - powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/setup-x86_64.exe', 'setup-x86_64.exe')" - SET CYGROOT=C:\cygwin64 - SET CYGCACHE=%CYGROOT%\var\cache\setup - setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib -P python - - SET TARGET_ARCH=x86_64-w64-mingw32 - SET CD_MFMT=%cd:\=/% - SET RESULT_INSTALLDIR_CFMT=%CD_MFMT:C:/=/cygdrive/c/% - C:\cygwin64\bin\bash -l %cd%\dev\build\windows\configure_profile.sh - displayName: 'Install cygwin' - env: - CYGMIRROR: "http://mirror.easyname.at/cygwin" - -- script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-opam.sh - displayName: 'Install opam' - -- script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-build.sh - displayName: 'Build Coq' - -- script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-test.sh - displayName: 'Test Coq' +# NB: image names can be found at +# https://docs.microsoft.com/en-us/azure/devops/pipelines/agents/hosted + +variables: + NJOBS: "2" + +jobs: +- job: Windows + pool: + vmImage: 'vs2017-win2016' + + steps: + - checkout: self + fetchDepth: 10 + + # cygwin package list not checked for minimality + - script: | + powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/setup-x86_64.exe', 'setup-x86_64.exe')" + SET CYGROOT=C:\cygwin64 + SET CYGCACHE=%CYGROOT%\var\cache\setup + setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib -P python + + SET TARGET_ARCH=x86_64-w64-mingw32 + SET CD_MFMT=%cd:\=/% + SET RESULT_INSTALLDIR_CFMT=%CD_MFMT:C:/=/cygdrive/c/% + C:\cygwin64\bin\bash -l %cd%\dev\build\windows\configure_profile.sh + displayName: 'Install cygwin' + env: + CYGMIRROR: "http://mirror.easyname.at/cygwin" + + - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-opam.sh + displayName: 'Install opam' + + - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-build.sh + displayName: 'Build Coq' + + - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-test.sh + displayName: 'Test Coq' + +- job: macOS + pool: + vmImage: 'macOS-10.13' + + steps: + - checkout: self + fetchDepth: 10 + + - script: | + set -e + brew update + brew unlink python + brew install gnu-time opam + + opam init -a -j "$NJOBS" --compiler=$COMPILER + opam switch set $COMPILER + eval $(opam env) + opam update + opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit + opam list + displayName: 'Install dependencies' + env: + COMPILER: "4.07.1" + FINDLIB_VER: ".1.8.0" + OPAMYES: "true" + + - script: | + set -e + + eval $(opam env) + ./configure -local -warn-error yes -native-compiler no + make -j "$NJOBS" + displayName: 'Build Coq' + + - script: | + eval $(opam env) + make -j "$NJOBS" test-suite + displayName: 'Run Coq Test Suite' diff --git a/clib/cThread.ml b/clib/cThread.ml index 0b7955aa28..9e0319e8f8 100644 --- a/clib/cThread.ml +++ b/clib/cThread.ml @@ -97,3 +97,13 @@ let thread_friendly_input_value ic = end with Unix.Unix_error _ | Sys_error _ -> raise End_of_file +(* On the ocaml runtime used in some opam-for-windows version the + * [Thread.sigmask] API raises Invalid_argument "not implemented", + * hence we protect the call and turn the exception into a no-op *) +let protect_sigalrm f x = + begin try ignore(Thread.sigmask Unix.SIG_BLOCK [Sys.sigalrm]) + with Invalid_argument _ -> () end; + f x + +let create f x = + Thread.create (protect_sigalrm f) x diff --git a/clib/cThread.mli b/clib/cThread.mli index acc5a60c09..b090479c4c 100644 --- a/clib/cThread.mli +++ b/clib/cThread.mli @@ -26,3 +26,6 @@ val thread_friendly_really_read : thread_ic -> Bytes.t -> off:int -> len:int -> unit val thread_friendly_really_read_line : thread_ic -> string +(* Wrapper around Thread.create that blocks signals such as Sys.sigalrm (used + * for Timeout *) +val create : ('a -> 'b) -> 'a -> Thread.t diff --git a/configure.ml b/configure.ml index 33f76078cf..6f5ade3b9a 100644 --- a/configure.ml +++ b/configure.ml @@ -1001,6 +1001,7 @@ let print_summary () = pr " Architecture : %s\n" arch; if operating_system <> "" then pr " Operating system : %s\n" operating_system; + pr " Sys.os_type : %s\n" Sys.os_type; pr " Coq VM bytecode link flags : %s\n" (String.concat " " vmbyteflags); pr " Other bytecode link flags : %s\n" custom_flag; pr " OCaml version : %s\n" caml_version; diff --git a/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat b/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat deleted file mode 100644 index 9dbce1920f..0000000000 --- a/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat +++ /dev/null @@ -1,28 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.4pl6 ^
- -destcyg="%ROOTPATH%\cygwin_coq64_84pl6_abs" ^
- -destcoq="%ROOTPATH%\coq64_84pl6_abs"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_84pl6_abs_ocaml.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat b/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat deleted file mode 100644 index 7faf3e9ce1..0000000000 --- a/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat +++ /dev/null @@ -1,28 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.5pl2 ^
- -destcyg="%ROOTPATH%\cygwin_coq64_85pl2_abs" ^
- -destcoq="%ROOTPATH%\coq64_85pl2_abs"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_85pl2_abs_ocaml.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat b/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat deleted file mode 100644 index b719b14c53..0000000000 --- a/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat +++ /dev/null @@ -1,28 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.5pl3 ^
- -destcyg="%ROOTPATH%\cygwin_coq64_85pl3_abs" ^
- -destcoq="%ROOTPATH%\coq64_85pl3_abs"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_85pl3_abs_ocaml.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_85pl3_installer.bat b/dev/build/windows/MakeCoq_85pl3_installer.bat deleted file mode 100644 index a9f4e2da2e..0000000000 --- a/dev/build/windows/MakeCoq_85pl3_installer.bat +++ /dev/null @@ -1,26 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=8.5pl3 ^
- -destcyg="%ROOTPATH%\cygwin_coq64_85pl3_inst" ^
- -destcoq="%ROOTPATH%\coq64_85pl3_inst"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_85pl3_installer.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_85pl3_installer_32.bat b/dev/build/windows/MakeCoq_85pl3_installer_32.bat deleted file mode 100644 index ef593cc63a..0000000000 --- a/dev/build/windows/MakeCoq_85pl3_installer_32.bat +++ /dev/null @@ -1,26 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=32 ^
- -installer=Y ^
- -coqver=8.5pl3 ^
- -destcyg="%ROOTPATH%\cygwin_coq32_85pl3_inst" ^
- -destcoq="%ROOTPATH%\coq32_85pl3_inst"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_85pl3_installer_32.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_86_abs_ocaml.bat b/dev/build/windows/MakeCoq_86_abs_ocaml.bat deleted file mode 100644 index 50483c4d4a..0000000000 --- a/dev/build/windows/MakeCoq_86_abs_ocaml.bat +++ /dev/null @@ -1,10 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.6 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86_abs ^
- -destcoq=%ROOTPATH%\coq64_86_abs
diff --git a/dev/build/windows/MakeCoq_86_installer.bat b/dev/build/windows/MakeCoq_86_installer.bat deleted file mode 100644 index 263520ff14..0000000000 --- a/dev/build/windows/MakeCoq_86_installer.bat +++ /dev/null @@ -1,8 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=8.6 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86_inst ^
- -destcoq=%ROOTPATH%\coq64_86_inst
diff --git a/dev/build/windows/MakeCoq_86_installer_32.bat b/dev/build/windows/MakeCoq_86_installer_32.bat deleted file mode 100644 index 14921dd7c3..0000000000 --- a/dev/build/windows/MakeCoq_86_installer_32.bat +++ /dev/null @@ -1,8 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=32 ^
- -installer=Y ^
- -coqver=8.6 ^
- -destcyg=%ROOTPATH%\cygwin_coq32_86_inst ^
- -destcoq=%ROOTPATH%\coq32_86_inst
diff --git a/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat b/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat deleted file mode 100644 index 914c332f46..0000000000 --- a/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat +++ /dev/null @@ -1,10 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.6beta1 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86beta1_abs ^
- -destcoq=%ROOTPATH%\coq64_86beta1_abs
diff --git a/dev/build/windows/MakeCoq_86beta1_installer.bat b/dev/build/windows/MakeCoq_86beta1_installer.bat deleted file mode 100644 index 76a5bb35ac..0000000000 --- a/dev/build/windows/MakeCoq_86beta1_installer.bat +++ /dev/null @@ -1,8 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=8.6beta1 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86beta1_inst ^
- -destcoq=%ROOTPATH%\coq64_86beta1_inst
diff --git a/dev/build/windows/MakeCoq_86beta1_installer_32.bat b/dev/build/windows/MakeCoq_86beta1_installer_32.bat deleted file mode 100644 index f53232b651..0000000000 --- a/dev/build/windows/MakeCoq_86beta1_installer_32.bat +++ /dev/null @@ -1,8 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=32 ^
- -installer=Y ^
- -coqver=8.6beta1 ^
- -destcyg=%ROOTPATH%\cygwin_coq32_86beta1_inst ^
- -destcoq=%ROOTPATH%\coq32_86beta1_inst
diff --git a/dev/build/windows/MakeCoq_86git_abs_ocaml.bat b/dev/build/windows/MakeCoq_86git_abs_ocaml.bat deleted file mode 100644 index 99a1f156b0..0000000000 --- a/dev/build/windows/MakeCoq_86git_abs_ocaml.bat +++ /dev/null @@ -1,28 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=git-v8.6 ^
- -destcyg="%ROOTPATH%\cygwin_coq64_86git_abs" ^
- -destcoq="%ROOTPATH%\coq64_86git_abs"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_86git_abs_ocaml.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat b/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat deleted file mode 100644 index 896d1cd633..0000000000 --- a/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat +++ /dev/null @@ -1,29 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -gtksrc=Y ^
- -coqver=git-v8.6 ^
- -destcyg="%ROOTPATH%\cygwin_coq64_86git_abs_gtksrc" ^
- -destcoq="%ROOTPATH%\coq64_86git_abs_gtksrc"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_86git_abs_ocaml_gtksrc.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_86git_installer.bat b/dev/build/windows/MakeCoq_86git_installer.bat deleted file mode 100644 index c4823103f1..0000000000 --- a/dev/build/windows/MakeCoq_86git_installer.bat +++ /dev/null @@ -1,26 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=git-v8.6 ^
- -destcyg="%ROOTPATH%\cygwin_coq64_86git_inst" ^
- -destcoq="%ROOTPATH%\coq64_86git_inst"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_86git_installer.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_86git_installer2.bat b/dev/build/windows/MakeCoq_86git_installer2.bat deleted file mode 100644 index d184f0e30e..0000000000 --- a/dev/build/windows/MakeCoq_86git_installer2.bat +++ /dev/null @@ -1,8 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=git-v8.6 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86git_inst2 ^
- -destcoq=%ROOTPATH%\coq64_86git_inst2
diff --git a/dev/build/windows/MakeCoq_86git_installer_32.bat b/dev/build/windows/MakeCoq_86git_installer_32.bat deleted file mode 100644 index 19146c96c9..0000000000 --- a/dev/build/windows/MakeCoq_86git_installer_32.bat +++ /dev/null @@ -1,26 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=32 ^
- -installer=Y ^
- -coqver=git-v8.6 ^
- -destcyg="%ROOTPATH%\cygwin_coq32_86git_inst" ^
- -destcoq="%ROOTPATH%\coq32_86git_inst"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_86git_installer_32.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_86git_installer_cyglocal.bat b/dev/build/windows/MakeCoq_86git_installer_cyglocal.bat deleted file mode 100755 index cf6cafaa02..0000000000 --- a/dev/build/windows/MakeCoq_86git_installer_cyglocal.bat +++ /dev/null @@ -1,27 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=git-v8.6 ^
- -cyglocal=Y ^
- -destcyg="%ROOTPATH%\cygwin_coq64_86git_inst_cyglocal" ^
- -destcoq="%ROOTPATH%\coq64_86git_inst_cyglocal"
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_86git_installer_cyglocal.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat b/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat deleted file mode 100644 index c0669f01d2..0000000000 --- a/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat +++ /dev/null @@ -1,10 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.6rc1 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86rc1_abs ^
- -destcoq=%ROOTPATH%\coq64_86rc1_abs
diff --git a/dev/build/windows/MakeCoq_86rc1_installer.bat b/dev/build/windows/MakeCoq_86rc1_installer.bat deleted file mode 100644 index 66234ebbde..0000000000 --- a/dev/build/windows/MakeCoq_86rc1_installer.bat +++ /dev/null @@ -1,8 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=8.6rc1 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86rc1_inst ^
- -destcoq=%ROOTPATH%\coq64_86rc1_inst
diff --git a/dev/build/windows/MakeCoq_86rc1_installer_32.bat b/dev/build/windows/MakeCoq_86rc1_installer_32.bat deleted file mode 100644 index 96f43e16a5..0000000000 --- a/dev/build/windows/MakeCoq_86rc1_installer_32.bat +++ /dev/null @@ -1,8 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=32 ^
- -installer=Y ^
- -coqver=8.6rc1 ^
- -destcyg=%ROOTPATH%\cygwin_coq32_86rc1_inst ^
- -destcoq=%ROOTPATH%\coq32_86rc1_inst
diff --git a/dev/build/windows/MakeCoq_88git_installer.bat b/dev/build/windows/MakeCoq_88git_installer.bat deleted file mode 100755 index b016fb3891..0000000000 --- a/dev/build/windows/MakeCoq_88git_installer.bat +++ /dev/null @@ -1,27 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=git-v8.8 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_88_inst ^
- -destcoq=%ROOTPATH%\coq64_88_inst ^
- -addon=bignums
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_88git_installer.bat failed with error code %ERRORLEVEL%
- EXIT /b %ERRORLEVEL%
-)
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt index 93851aeb8d..a392115ea4 100644 --- a/dev/build/windows/ReadMe.txt +++ b/dev/build/windows/ReadMe.txt @@ -369,8 +369,6 @@ Text files patched by the installer: Text files containing the install folder path after install: -./bin/mkcamlp5:LIB=D:/bin/coq64_buildtest_reloc_ocaml20/libocaml/camlp5 -./bin/mkcamlp5.opt:LIB=D:/bin/coq64_buildtest_reloc_ocaml20/libocaml/camlp5 ./libocaml/Makefile.config:PREFIX=D:/bin/coq64_buildtest_reloc_ocaml20 ./libocaml/Makefile.config:LIBDIR=D:/bin/coq64_buildtest_reloc_ocaml20/libocaml ./libocaml/site-lib/findlib/Makefile.config:OCAML_CORE_BIN=/cygdrive/d/bin/coq64_buildtest_reloc_ocaml20/bin @@ -382,8 +380,6 @@ Text files containing the install folder path after install: ./libocaml/topfind: Topdirs.dir_load Format.err_formatter "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib_top.cma"; ./libocaml/topfind:(* #load "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib.cma";; *) ./libocaml/topfind:(* #load "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib_top.cma";; *) -./man/man1/camlp5.1:These files are installed in the directory D:/bin/coq64_buildtest_reloc_ocaml20/libocaml/camlp5. -./man/man1/camlp5.1:D:/bin/coq64_buildtest_reloc_ocaml20/libocaml/camlp5 Binary files containing the build folder path after install: @@ -398,26 +394,6 @@ Binary file ./libocaml/ocamldoc/odoc_info.cma matches Binary files containing the install folder path after install: $ find . -type f -exec grep "coq64_buildtest_reloc_ocaml20" {} /dev/null \; -Binary file ./bin/camlp4.exe matches -Binary file ./bin/camlp4boot.exe matches -Binary file ./bin/camlp4o.exe matches -Binary file ./bin/camlp4o.opt.exe matches -Binary file ./bin/camlp4of.exe matches -Binary file ./bin/camlp4of.opt.exe matches -Binary file ./bin/camlp4oof.exe matches -Binary file ./bin/camlp4oof.opt.exe matches -Binary file ./bin/camlp4orf.exe matches -Binary file ./bin/camlp4orf.opt.exe matches -Binary file ./bin/camlp4r.exe matches -Binary file ./bin/camlp4r.opt.exe matches -Binary file ./bin/camlp4rf.exe matches -Binary file ./bin/camlp4rf.opt.exe matches -Binary file ./bin/camlp5.exe matches -Binary file ./bin/camlp5o.exe matches -Binary file ./bin/camlp5o.opt matches -Binary file ./bin/camlp5r.exe matches -Binary file ./bin/camlp5r.opt matches -Binary file ./bin/camlp5sch.exe matches Binary file ./bin/coqc.exe matches Binary file ./bin/coqchk.exe matches Binary file ./bin/coqdep.exe matches @@ -428,11 +404,7 @@ Binary file ./bin/coqtop.exe matches Binary file ./bin/coqworkmgr.exe matches Binary file ./bin/coq_makefile.exe matches Binary file ./bin/menhir matches -Binary file ./bin/mkcamlp4.exe matches Binary file ./bin/ocaml.exe matches -Binary file ./bin/ocamlbuild.byte.exe matches -Binary file ./bin/ocamlbuild.exe matches -Binary file ./bin/ocamlbuild.native.exe matches Binary file ./bin/ocamlc.exe matches Binary file ./bin/ocamlc.opt.exe matches Binary file ./bin/ocamldebug.exe matches @@ -455,17 +427,6 @@ Binary file ./lib/ide/ide_win32_stubs.o matches Binary file ./lib/lib/clib.a matches Binary file ./lib/lib/clib.cma matches Binary file ./lib/libcoqrun.a matches -Binary file ./libocaml/camlp4/camlp4fulllib.a matches -Binary file ./libocaml/camlp4/camlp4fulllib.cma matches -Binary file ./libocaml/camlp4/camlp4lib.a matches -Binary file ./libocaml/camlp4/camlp4lib.cma matches -Binary file ./libocaml/camlp4/camlp4o.cma matches -Binary file ./libocaml/camlp4/camlp4of.cma matches -Binary file ./libocaml/camlp4/camlp4oof.cma matches -Binary file ./libocaml/camlp4/camlp4orf.cma matches -Binary file ./libocaml/camlp4/camlp4r.cma matches -Binary file ./libocaml/camlp4/camlp4rf.cma matches -Binary file ./libocaml/camlp5/odyl.cma matches Binary file ./libocaml/compiler-libs/ocamlcommon.a matches Binary file ./libocaml/compiler-libs/ocamlcommon.cma matches Binary file ./libocaml/dynlink.cma matches diff --git a/dev/build/windows/patches_coq/camlp4-4.02+6.patch b/dev/build/windows/patches_coq/camlp4-4.02+6.patch deleted file mode 100644 index 0cdb4a929b..0000000000 --- a/dev/build/windows/patches_coq/camlp4-4.02+6.patch +++ /dev/null @@ -1,11 +0,0 @@ ---- camlp4-4.02-6.orig/myocamlbuild.ml 2015-06-17 13:37:36.000000000 +0200 -+++ camlp4-4.02+6/myocamlbuild.ml 2016-10-13 13:57:35.512213600 +0200 -@@ -86,7 +86,7 @@ - let dep = "camlp4"/"boot"/exe in - let cmd = - let ( / ) = Filename.concat in -- "camlp4"/"boot"/exe -+ String.escaped (String.escaped ("camlp4"/"boot"/exe)) - in - (Some dep, cmd) - in diff --git a/dev/build/windows/patches_coq/coq-8.4pl2.patch b/dev/build/windows/patches_coq/coq-8.4pl2.patch deleted file mode 100644 index 45a66d0bfa..0000000000 --- a/dev/build/windows/patches_coq/coq-8.4pl2.patch +++ /dev/null @@ -1,11 +0,0 @@ ---- configure 2014-04-14 22:28:39.174177924 +0200 -+++ configure 2014-04-14 22:29:23.253025166 +0200 -@@ -335,7 +335,7 @@ - MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3` - MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1` - MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2` -- if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then -+ if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ] || [ "$MAKEVERSIONMAJOR" -ge 4 ] ; then - echo "You have GNU Make $MAKEVERSION. Good!" - else - OK="no"
\ No newline at end of file diff --git a/dev/build/windows/patches_coq/coq-8.4pl6.patch b/dev/build/windows/patches_coq/coq-8.4pl6.patch deleted file mode 100644 index c3b7f8574e..0000000000 --- a/dev/build/windows/patches_coq/coq-8.4pl6.patch +++ /dev/null @@ -1,13 +0,0 @@ -coq-8.4pl6.orig ---- coq-8.4pl6.orig/configure 2015-04-09 15:59:35.000000000 +0200 -+++ coq-8.4pl6//configure 2016-11-09 13:29:42.235319800 +0100 -@@ -309,9 +309,6 @@ - # executable extension - - case "$ARCH,$CYGWIN" in -- win32,yes) -- EXE=".exe" -- DLLEXT=".so";; - win32,*) - EXE=".exe" - DLLEXT=".dll";; diff --git a/dev/build/windows/patches_coq/flexdll-0.34.patch b/dev/build/windows/patches_coq/flexdll-0.34.patch deleted file mode 100644 index 16389baca3..0000000000 --- a/dev/build/windows/patches_coq/flexdll-0.34.patch +++ /dev/null @@ -1,14 +0,0 @@ -reloc.ml ---- orig.flexdll-0.34/reloc.ml 2015-01-22 17:30:07.000000000 +0100 -+++ flexdll-0.34/reloc.ml 2016-10-12 11:59:16.885829700 +0200 -@@ -117,8 +117,8 @@ - - let new_cmdline () = - let rf = match !toolchain with -- | `MSVC | `MSVC64 | `LIGHTLD -> true -- | `MINGW | `MINGW64 | `GNAT | `CYGWIN | `CYGWIN64 -> false -+ | `MSVC | `MSVC64 | `LIGHTLD | `MINGW | `MINGW64 -> true -+ | `GNAT | `CYGWIN | `CYGWIN64 -> false - in - { - may_use_response_file = rf; diff --git a/dev/build/windows/patches_coq/glib-2.46.0.patch b/dev/build/windows/patches_coq/glib-2.46.0.patch deleted file mode 100644 index 9082460bf0..0000000000 --- a/dev/build/windows/patches_coq/glib-2.46.0.patch +++ /dev/null @@ -1,30 +0,0 @@ -diff -u -r glib-2.46.0/gio/glocalfile.c glib-2.46.0.patched/gio/glocalfile.c ---- glib-2.46.0/gio/glocalfile.c 2015-08-27 05:32:26.000000000 +0200 -+++ glib-2.46.0.patched/gio/glocalfile.c 2016-01-27 13:08:30.059736400 +0100 -@@ -2682,7 +2682,10 @@ - (!g_path_is_absolute (filename) || len > g_path_skip_root (filename) - filename)) - wfilename[len] = '\0'; - -- retval = _wstat32i64 (wfilename, &buf); -+ // MSoegtrop: _wstat32i64 is the wrong function for GLocalFileStat = struct _stati64 -+ // The correct function is _wstati64, see https://msdn.microsoft.com/en-us/library/14h5k7ff.aspx -+ // Also _wstat32i64 is a VC function, not a windows SDK function, see https://msdn.microsoft.com/en-us/library/aa273365(v=vs.60).aspx -+ retval = _wstati64 (wfilename, &buf); - save_errno = errno; - - g_free (wfilename); -diff -u -r glib-2.46.0/glib/gstdio.c glib-2.46.0.patched/glib/gstdio.c ---- glib-2.46.0/glib/gstdio.c 2015-02-26 13:57:09.000000000 +0100 -+++ glib-2.46.0.patched/glib/gstdio.c 2016-01-27 13:31:12.708987700 +0100 -@@ -493,7 +493,10 @@ - (!g_path_is_absolute (filename) || len > g_path_skip_root (filename) - filename)) - wfilename[len] = '\0'; - -- retval = _wstat (wfilename, buf); -+ // MSoegtrop: _wstat32i64 is the wrong function for GLocalFileStat = struct _stati64 -+ // The correct function is _wstati64, see https://msdn.microsoft.com/en-us/library/14h5k7ff.aspx -+ // Also _wstat32i64 is a VC function, not a windows SDK function, see https://msdn.microsoft.com/en-us/library/aa273365(v=vs.60).aspx -+ retval = _wstati64 (wfilename, buf); - save_errno = errno; - - g_free (wfilename); diff --git a/dev/build/windows/patches_coq/lablgtk-2.18.3.patch b/dev/build/windows/patches_coq/lablgtk-2.18.3.patch deleted file mode 100644 index 23c303135d..0000000000 --- a/dev/build/windows/patches_coq/lablgtk-2.18.3.patch +++ /dev/null @@ -1,101 +0,0 @@ -diff/patch file created on Wed, Apr 25, 2018 11:08:05 AM with: -difftar-folder.sh ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz lablgtk-2.18.3 1 -TARFILE= ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz -FOLDER= lablgtk-2.18.3 -TARSTRIP= 1 -TARPREFIX= lablgtk-2.18.3/ -ORIGFOLDER= lablgtk-2.18.3.orig ---- lablgtk-2.18.3.orig/configure 2014-10-29 08:51:05.000000000 +0100 -+++ lablgtk-2.18.3/configure 2018-04-25 10:58:54.454501600 +0200 -@@ -2667,7 +2667,7 @@ - fi - - --if test "`$OCAMLFIND printconf stdlib`" != "`$CAMLC -where`"; then -+if test "`$OCAMLFIND printconf stdlib | tr '\\' '/'`" != "`$CAMLC -where | tr '\\' '/'`"; then - { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Ignoring ocamlfind" >&5 - $as_echo "$as_me: WARNING: Ignoring ocamlfind" >&2;} - OCAMLFIND=no ---- lablgtk-2.18.3.orig/src/glib.mli 2014-10-29 08:51:06.000000000 +0100 -+++ lablgtk-2.18.3/src/glib.mli 2018-04-25 10:58:54.493555500 +0200 -@@ -75,6 +75,7 @@ - type condition = [ `ERR | `HUP | `IN | `NVAL | `OUT | `PRI] - type id - val channel_of_descr : Unix.file_descr -> channel -+ val channel_of_descr_socket : Unix.file_descr -> channel - val add_watch : - cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id - val remove : id -> unit ---- lablgtk-2.18.3.orig/src/glib.ml 2014-10-29 08:51:06.000000000 +0100 -+++ lablgtk-2.18.3/src/glib.ml 2018-04-25 10:58:54.479543500 +0200 -@@ -72,6 +72,8 @@ - type id - external channel_of_descr : Unix.file_descr -> channel - = "ml_g_io_channel_unix_new" -+ external channel_of_descr_socket : Unix.file_descr -> channel -+ = "ml_g_io_channel_unix_new_socket" - external remove : id -> unit = "ml_g_source_remove" - external add_watch : - cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id ---- lablgtk-2.18.3.orig/src/Makefile 2014-10-29 08:51:06.000000000 +0100 -+++ lablgtk-2.18.3/src/Makefile 2018-04-25 10:58:54.506522500 +0200 -@@ -461,9 +461,9 @@ - do rm -f "$(BINDIR)"/$$f; done - - lablgtk.cma liblablgtk2$(XA): $(COBJS) $(MLOBJS) -- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) -+ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) - lablgtk.cmxa: $(COBJS) $(MLOBJS:.cmo=.cmx) -- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) -+ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) - lablgtk.cmxs: DYNLINKLIBS=$(GTK_LIBS) - - lablgtkgl.cma liblablgtkgl2$(XA): $(GLCOBJS) $(GLMLOBJS) ---- lablgtk-2.18.3.orig/src/ml_glib.c 2014-10-29 08:51:06.000000000 +0100 -+++ lablgtk-2.18.3/src/ml_glib.c 2018-04-25 10:58:54.539535600 +0200 -@@ -25,6 +25,8 @@ - #include <string.h> - #include <locale.h> - #ifdef _WIN32 -+/* to kill a #warning: include winsock2.h before windows.h */ -+#include <winsock2.h> - #include "win32.h" - #include <wtypes.h> - #include <io.h> -@@ -38,6 +40,11 @@ - #include <caml/callback.h> - #include <caml/threads.h> - -+#ifdef _WIN32 -+/* for Socket_val */ -+#include <caml/unixsupport.h> -+#endif -+ - #include "wrappers.h" - #include "ml_glib.h" - #include "glib_tags.h" -@@ -325,14 +332,23 @@ - - #ifndef _WIN32 - ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref) -+CAMLprim value ml_g_io_channel_unix_new_socket (value arg1) { -+ return Val_GIOChannel_noref (g_io_channel_unix_new (Int_val (arg1))); -+} - - #else - CAMLprim value ml_g_io_channel_unix_new(value wh) - { - return Val_GIOChannel_noref -- (g_io_channel_unix_new -+ (g_io_channel_win32_new_fd - (_open_osfhandle((long)*(HANDLE*)Data_custom_val(wh), O_BINARY))); - } -+ -+CAMLprim value ml_g_io_channel_unix_new_socket(value wh) -+{ -+ return Val_GIOChannel_noref -+ (g_io_channel_win32_new_socket(Socket_val(wh))); -+} - #endif - - static gboolean ml_g_io_channel_watch(GIOChannel *s, GIOCondition c, diff --git a/dev/build/windows/patches_coq/sed-4.2.2-3.src.patch b/dev/build/windows/patches_coq/sed-4.2.2-3.src.patch index d210a04153..d210a04153 100755..100644 --- a/dev/build/windows/patches_coq/sed-4.2.2-3.src.patch +++ b/dev/build/windows/patches_coq/sed-4.2.2-3.src.patch diff --git a/dev/build/windows/patches_coq/sed-4.2.2.patch b/dev/build/windows/patches_coq/sed-4.2.2.patch index c7ccd53c7f..c7ccd53c7f 100755..100644 --- a/dev/build/windows/patches_coq/sed-4.2.2.patch +++ b/dev/build/windows/patches_coq/sed-4.2.2.patch 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/gitlab.bat b/dev/ci/gitlab.bat index 2a42a6b58e..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
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 59602581c7..554bfefa0a 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4343,7 +4343,7 @@ Automating distributivity, constant propagation) and comparing syntactically the results. -.. tacn:: ring_simplify {+ @term} +.. tacn:: ring_simplify {* @term} :name: ring_simplify This tactic applies the normalization procedure described above to @@ -4357,7 +4357,7 @@ the tactic and how to declare new ring structures. All declared field structures can be printed with the ``Print Rings`` command. .. tacn:: field - field_simplify {+ @term} + field_simplify {* @term} field_simplify_eq :name: field; field_simplify; field_simplify_eq diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 6532e08e9d..49cbc4d7e5 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -77,6 +77,9 @@ val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t For getting the evar-normal form of a term with evars see {!Evarutil.nf_evar}. *) +val to_constr_opt : Evd.evar_map -> t -> Constr.t option +(** Same as [to_constr], but returns [None] if some unresolved evars remain *) + val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type (** {5 Constructors} *) diff --git a/engine/evd.ml b/engine/evd.ml index 31c326df6a..eee2cb700c 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1376,6 +1376,13 @@ module MiniEConstr = struct in UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c + let to_constr_opt sigma c = + let evar_value ev = Some (existential_value sigma ev) in + try + Some (UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c) + with NotInstantiatedEvar -> + None + let of_named_decl d = d let unsafe_to_named_decl d = d let of_rel_decl d = d diff --git a/engine/evd.mli b/engine/evd.mli index 7560d68805..de73144895 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -689,6 +689,7 @@ module MiniEConstr : sig val of_constr_array : Constr.t array -> t array val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t + val to_constr_opt : evar_map -> t -> Constr.t option val unsafe_to_constr : t -> Constr.t val unsafe_to_constr_array : t array -> Constr.t array diff --git a/lib/control.ml b/lib/control.ml index e09068740d..ffb3584f1e 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -57,7 +57,7 @@ let windows_timeout n f x e = done in let init = Unix.gettimeofday () in - let _id = Thread.create thread init in + let _id = CThread.create thread init in try let res = f x in let () = killed := true in @@ -284,15 +284,12 @@ let pr_vertical_list pr = function [pr 0 a0 ++ sep() ++ ... ++ sep() ++ pr n an] *) let prvecti_with_sep sep elem v = - let rec pr i = - if Int.equal i 0 then - elem 0 v.(0) - else - let r = pr (i-1) and s = sep () and e = elem i v.(i) in - r ++ s ++ e + let v = CArray.mapi (fun i x -> + let pp = if i = 0 then mt() else sep() in + pp ++ elem i x) + v in - let n = Array.length v in - if Int.equal n 0 then mt () else pr (n - 1) + seq (Array.to_list v) (* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 4bb52f599a..2055b25ff4 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -2014,7 +2014,7 @@ let add_morphism atts binders m s n = in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance - (Some (true, CAst.make @@ CRecord [])) + None ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) (** Bind to "rewrite" too *) diff --git a/proofs/proof.ml b/proofs/proof.ml index 1aeb24606b..4ce932b93d 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -351,19 +351,13 @@ let dependent_start ~name ~poly goals = type open_error_reason = | UnfinishedProof - | HasShelvedGoals | HasGivenUpGoals - | HasUnresolvedEvar let print_open_error_reason er = let open Pp in match er with | UnfinishedProof -> str "Attempt to save an incomplete proof" - | HasShelvedGoals -> - str "Attempt to save a proof with shelved goals" | HasGivenUpGoals -> strbrk "Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed." - | HasUnresolvedEvar -> - strbrk "Attempt to save a proof with existential variables still non-instantiated" exception OpenProof of Names.Id.t option * open_error_reason @@ -375,19 +369,25 @@ let _ = CErrors.register_handler begin function | _ -> raise CErrors.Unhandled end +let warn_remaining_shelved_goals = + CWarnings.create ~name:"remaining-shelved-goals" ~category:"tactics" + (fun () -> Pp.str"The proof has remaining shelved goals") + +let warn_remaining_unresolved_evars = + CWarnings.create ~name:"remaining-unresolved-evars" ~category:"tactics" + (fun () -> Pp.str"The proof has unresolved variables") + let return ?pid (p : t) = if not (is_done p) then raise (OpenProof(pid, UnfinishedProof)) - else if has_shelved_goals p then - raise (OpenProof(pid, HasShelvedGoals)) else if has_given_up_goals p then raise (OpenProof(pid, HasGivenUpGoals)) - else if has_unresolved_evar p then - (* spiwack: for compatibility with <= 8.3 proof engine *) - raise (OpenProof(pid, HasUnresolvedEvar)) - else + else begin + if has_shelved_goals p then warn_remaining_shelved_goals () + else if has_unresolved_evar p then warn_remaining_unresolved_evars (); let p = unfocus end_of_stack_kind p () in Proofview.return p.proofview + end let compact p = let entry, proofview = Proofview.compact p.entry p.proofview in diff --git a/proofs/proof.mli b/proofs/proof.mli index fd5e905a3b..40e8ff7eef 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -130,13 +130,10 @@ val compact : t -> t (* Returns the proofs (with their type) of the initial goals. Raises [UnfinishedProof] is some goals remain to be considered. Raises [HasShelvedGoals] if some goals are left on the shelf. - Raises [HasGivenUpGoals] if some goals have been given up. - Raises [HasUnresolvedEvar] if some evars have been left undefined. *) + Raises [HasGivenUpGoals] if some goals have been given up. *) type open_error_reason = | UnfinishedProof - | HasShelvedGoals | HasGivenUpGoals - | HasUnresolvedEvar exception OpenProof of Names.Id.t option * open_error_reason diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f8adc58921..4cc73f419e 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -443,8 +443,13 @@ let return_proof ?(allow_partial=false) () = (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) + let proof_opt c = + match EConstr.to_constr_opt evd c with + | Some p -> p + | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain") + in let proofs = - List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in + List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in proofs, Evd.evar_universe_context evd let close_future_proof ~opaque ~feedback_id proof = diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 51166cf238..2f8129bbfd 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -190,7 +190,7 @@ module Make(T : Task) () = struct let () = TQueue.broadcast queue in Worker.kill proc in - let _ = Thread.create kill_if () in + let _ = CThread.create kill_if () in try while true do report_status ~id "Idle"; @@ -250,7 +250,7 @@ module Make(T : Task) () = struct { active = Pool.create queue ~size; queue; - cleaner = if size > 0 then Some (Thread.create cleaner queue) else None; + cleaner = if size > 0 then Some (CThread.create cleaner queue) else None; } let destroy { active; queue } = diff --git a/stm/spawned.ml b/stm/spawned.ml index a5d6ea96f9..bd772d825d 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -38,7 +38,7 @@ let controller h pr pw = prerr_endline ("control channel broken: " ^ Printexc.to_string e); exit 1 in loop () in - ignore(Thread.create main ()) + ignore(CThread.create main ()) let main_channel = ref None let control_channel = ref None diff --git a/stm/stm.ml b/stm/stm.ml index 169d608d2d..8ed7f2c866 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -739,7 +739,7 @@ end = struct (* {{{ *) else begin set_last_job job; if Option.is_empty !worker then - worker := Some (Thread.create run_command ()) + worker := Some (CThread.create run_command ()) end end @@ -3006,7 +3006,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) let bname = VCS.mk_branch_name x in let opacity_of_produced_term = function (* This AST is ambiguous, hence we check it dynamically *) - | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity + | VernacInstance (_,_ , None, _) -> GuaranteesOpacity | _ -> Doesn'tGuaranteeOpacity in VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[])); let proof_mode = default_proof_mode () in diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 454a4b66e7..09f531ce13 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -160,11 +160,12 @@ let classify_vernac e = | VernacMemOption _ | VernacPrintOption _ | VernacGlobalCheck _ | VernacDeclareReduction _ - | VernacDeclareClass _ | VernacDeclareInstances _ + | VernacExistingClass _ | VernacExistingInstance _ | VernacRegister _ | VernacNameSectionHypSet _ | VernacDeclareCustomEntry _ - | VernacComments _ -> VtSideff [], VtLater + | VernacComments _ + | VernacDeclareInstance _ -> VtSideff [], VtLater (* Who knows *) | VernacLoad _ -> VtSideff [], VtNow (* (Local) Notations have to disappear *) diff --git a/stm/workerPool.ml b/stm/workerPool.ml index 0ff66686e4..2432e72c8a 100644 --- a/stm/workerPool.ml +++ b/stm/workerPool.ml @@ -86,7 +86,7 @@ let rec create_worker extra pool id = let exit () = cancel := true; cleanup pool; Thread.exit () in let cancelled () = !cancel in let cpanel = { exit; cancelled; extra } in - let manager = Thread.create (Model.manager cpanel) worker in + let manager = CThread.create (Model.manager cpanel) worker in { name; cancel; manager; process } and cleanup x = locking x begin fun { workers; count; extra_arg } -> diff --git a/test-suite/bugs/closed/bug_2830.v b/test-suite/bugs/closed/bug_2830.v index 801c61b132..a321bb324e 100644 --- a/test-suite/bugs/closed/bug_2830.v +++ b/test-suite/bugs/closed/bug_2830.v @@ -194,14 +194,17 @@ Instance skel_equiv A : Equivalence (@skel A). Admitted. Import FunctionalExtensionality. -Instance set_cat : Category Type (fun A B => A -> B) := { + +Instance set_cat : Category Type (fun A B => A -> B). +refine {| id := fun A => fun x => x ; comp c b a f g := fun x => f (g x) ; eqv := fun A B => @skel (A -> B) -}. +|}. intros. compute. symmetry. apply eta_expansion. intros. compute. symmetry. apply eta_expansion. -intros. compute. reflexivity. Defined. +intros. compute. reflexivity. +Defined. (* The [list] type constructor is a Functor. *) diff --git a/test-suite/bugs/closed/bug_3495.v b/test-suite/bugs/closed/bug_3495.v index 7b0883f910..47db64a096 100644 --- a/test-suite/bugs/closed/bug_3495.v +++ b/test-suite/bugs/closed/bug_3495.v @@ -1,7 +1,7 @@ Require Import RelationClasses. Axiom R : Prop -> Prop -> Prop. -Declare Instance : Reflexive R. +Declare Instance R_refl : Reflexive R. Class bar := { x : False }. Record foo := { a : Prop ; b : bar }. diff --git a/test-suite/bugs/closed/bug_4498.v b/test-suite/bugs/closed/bug_4498.v index 379e46b3e3..9b3210860c 100644 --- a/test-suite/bugs/closed/bug_4498.v +++ b/test-suite/bugs/closed/bug_4498.v @@ -19,6 +19,6 @@ Class Category := { Require Export Coq.Setoids.Setoid. -Add Parametric Morphism `{C : Category} {A B C} : (@compose _ A B C) with +Add Parametric Morphism `{Category} {A B C} : (@compose _ A B C) with signature equiv ==> equiv ==> equiv as compose_mor. Proof. apply comp_respects. Qed. diff --git a/test-suite/bugs/closed/bug_9329.v b/test-suite/bugs/closed/bug_9329.v new file mode 100644 index 0000000000..c0322dec40 --- /dev/null +++ b/test-suite/bugs/closed/bug_9329.v @@ -0,0 +1,12 @@ +(* Declare empty levels in the same order they are computed *) + +Notation "< a ; b ; c >1" := + (sum a (sum b c)) (at level 18, a at level 19, b at level 20, c at level 21). +Notation "< a ; b ; c >2" := + (sum a (sum b c)) (at level 28, a at level 29, c at level 32, b at level 31). +Notation "< a ; b ; c >3" := + (sum a (sum b c)) (at level 38, c at level 42, a at level 39, b at level 41). +Notation "< a ; b ; c >4" := + (sum a (sum b c)) (at level 48, c at level 52, b at level 51, a at level 49). +Notation "< a ; b >" := + (sum a b) (at level 61, a at level 63, b at level 62). diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v index 78b2aa69b9..9d83743b2a 100644 --- a/test-suite/bugs/opened/bug_3890.v +++ b/test-suite/bugs/opened/bug_3890.v @@ -3,7 +3,9 @@ Set Nested Proofs Allowed. Class Foo. Class Bar := b : Type. +Set Refine Instance Mode. Instance foo : Foo := _. +Unset Refine Instance Mode. (* 1 subgoals, subgoal 1 (ID 4) ============================ diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 400479ae85..9086621344 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -198,7 +198,9 @@ Module UniqueInstances. for it. *) Set Typeclasses Unique Instances. Class Eq (A : Type) : Set. + Set Refine Instance Mode. Instance eqa : Eq nat := _. constructor. Qed. + Unset Refine Instance Mode. Instance eqb : Eq nat := {}. Class Foo (A : Type) (e : Eq A) : Set. Instance fooa : Foo _ eqa := {}. diff --git a/test-suite/unit-tests/lib/pp_big_vect.ml b/test-suite/unit-tests/lib/pp_big_vect.ml new file mode 100644 index 0000000000..e1cdd290e2 --- /dev/null +++ b/test-suite/unit-tests/lib/pp_big_vect.ml @@ -0,0 +1,14 @@ +open OUnit +open Pp + +let pr_big_vect = + let n = "pr_big_vect" in + n >:: (fun () -> + let v = Array.make (1 lsl 20) () in + let pp = prvecti_with_sep spc (fun _ _ -> str"x") v in + let str = string_of_ppcmds pp in + ignore(str)) + +let tests = [pr_big_vect] + +let () = Utest.run_tests __FILE__ (Utest.open_log_out_ch __FILE__) tests diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v index 81a087b525..decb5c7519 100644 --- a/theories/Compat/Coq89.v +++ b/theories/Compat/Coq89.v @@ -12,3 +12,4 @@ Local Set Warnings "-deprecated". Unset Private Polymorphic Universes. +Set Refine Instance Mode. diff --git a/vernac/classes.ml b/vernac/classes.ml index a342f5bf98..748a2628c5 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -28,7 +28,7 @@ module RelDecl = Context.Rel.Declaration open Decl_kinds open Entries -let refine_instance = ref true +let refine_instance = ref false let () = Goptions.(declare_bool_option { optdepr = false; @@ -105,8 +105,6 @@ let id_of_class cl = mip.(0).Declarations.mind_typename | _ -> assert false -open Pp - let instance_hook k info global imps ?hook cst = Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps; let info = intern_info info in @@ -128,7 +126,7 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma); instance_hook k info global imps ?hook (ConstRef kn) -let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id = +let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst id = let subst = List.fold_left2 (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') [] subst (snd k.cl_context) @@ -144,7 +142,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); - instance_hook k pri global imps ?hook (ConstRef cst); id + instance_hook k pri global imps (ConstRef cst) let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype = let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in @@ -191,7 +189,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id else ignore (Pfedit.by (Tactics.auto_intros_tac ids)); (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) () -let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = +let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = let props = match props with | Some (true, { CAst.v = CRecord fs }) -> @@ -278,69 +276,74 @@ let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~pro else CErrors.user_err Pp.(str "Unsolved obligations remaining."); id -let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~program_mode - poly ctx (instid, bk, cl) props - ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = - let env = Global.env() in - let ({CAst.loc;v=instid}, pl) = instid in +let interp_instance_context env ctx ?(generalize=false) pl bk cl = let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in let tclass, ids = match bk with | Decl_kinds.Implicit -> - Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false - (fun avoid (clname, _) -> - match clname with - | Some cl -> - let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in - t, avoid - | None -> failwith ("new instance: under-applied typeclass")) - cl + Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false + (fun avoid (clname, _) -> + match clname with + | Some cl -> + let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in + t, avoid + | None -> failwith ("new instance: under-applied typeclass")) + cl | Explicit -> cl, Id.Set.empty in let tclass = if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) else tclass in - let sigma, k, u, cty, ctx', ctx, imps, subst = - let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in - let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in - let len = Context.Rel.nhyps ctx in - let imps = imps @ Impargs.lift_implicits len imps' in - let ctx', c = decompose_prod_assum sigma c' in - let ctx'' = ctx' @ ctx in - let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in - let u_s = EInstance.kind sigma u in - let cl = Typeclasses.typeclass_univ_instance (k, u_s) in - let args = List.map of_constr args in - let cl_context = List.map (Termops.map_rel_decl of_constr) (snd cl.cl_context) in - let _, args = - List.fold_right (fun decl (args, args') -> - match decl with - | LocalAssum _ -> (List.tl args, List.hd args :: args') + let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in + let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in + let len = Context.Rel.nhyps ctx in + let imps = imps @ Impargs.lift_implicits len imps' in + let ctx', c = decompose_prod_assum sigma c' in + let ctx'' = ctx' @ ctx in + let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in + let u_s = EInstance.kind sigma u in + let cl = Typeclasses.typeclass_univ_instance (k, u_s) in + let args = List.map of_constr args in + let cl_context = List.map (Termops.map_rel_decl of_constr) (snd cl.cl_context) in + let _, args = + List.fold_right (fun decl (args, args') -> + match decl with + | LocalAssum _ -> (List.tl args, List.hd args :: args') | LocalDef (_,b,_) -> (args, Vars.substl args' b :: args')) - cl_context (args, []) - in - sigma, cl, u, c', ctx', ctx, imps, args + cl_context (args, []) + in + let sigma = Evarutil.nf_evar_map sigma in + let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in + sigma, cl, u, c', ctx', ctx, imps, args, decl + + +let new_instance ?(global=false) ?(refine= !refine_instance) ~program_mode + poly ctx (instid, bk, cl) props + ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = + let env = Global.env() in + let ({CAst.loc;v=instid}, pl) = instid in + let sigma, k, u, cty, ctx', ctx, imps, subst, decl = + interp_instance_context env ~generalize ctx pl bk cl in let id = match instid with - Name id -> - let sp = Lib.make_path id in - if Nametab.exists_cci sp then - user_err ~hdr:"new_instance" (Id.print id ++ Pp.str " already exists."); - id - | Anonymous -> - let i = Nameops.add_suffix (id_of_class k) "_instance_0" in - Namegen.next_global_ident_away i (Termops.vars_of_env env) + | Name id -> id + | Anonymous -> + let i = Nameops.add_suffix (id_of_class k) "_instance_0" in + Namegen.next_global_ident_away i (Termops.vars_of_env env) in let env' = push_rel_context ctx env in - let sigma = Evarutil.nf_evar_map sigma in - let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in - if abstract then - do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id - else - do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode - cty k u ctx ctx' pri decl imps subst id props + do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode + cty k u ctx ctx' pri decl imps subst id props + +let declare_new_instance ?(global=false) poly ctx (instid, bk, cl) pri = + let env = Global.env() in + let ({CAst.loc;v=instid}, pl) = instid in + let sigma, k, u, cty, ctx', ctx, imps, subst, decl = + interp_instance_context env ctx pl bk cl + in + do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid let named_of_rel_context l = let open Vars in diff --git a/vernac/classes.mli b/vernac/classes.mli index eb6c0c92e1..6f61da66cf 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -40,7 +40,6 @@ val declare_instance_constant : unit val new_instance : - ?abstract:bool (** Not abstract by default. *) -> ?global:bool (** Not global by default. *) -> ?refine:bool (** Allow refinement *) -> program_mode:bool -> @@ -54,6 +53,14 @@ val new_instance : Hints.hint_info_expr -> Id.t +val declare_new_instance : + ?global:bool (** Not global by default. *) -> + Decl_kinds.polymorphic -> + local_binder_expr list -> + ident_decl * Decl_kinds.binding_kind * constr_expr -> + Hints.hint_info_expr -> + unit + (** Setting opacity *) val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 43abc0a200..1a07d74a0e 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -146,7 +146,8 @@ let register_empty_levels accu forpat levels = (where, ans) :: rem, save_levels accu where nlev else rem, accu in - filter accu levels + let (l,accu) = filter accu levels in + List.rev l, accu let find_position accu custom forpat assoc level = let accu, (clev, plev) = find_levels accu custom in diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 22528a607f..3bc4aecdb1 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -683,19 +683,19 @@ GRAMMAR EXTEND Gram info = hint_info ; props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } | ":="; c = lconstr -> { Some (false,c) } | -> { None } ] -> - { VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info) } + { VernacInstance (snd namesup,(fst namesup,expl,t),props,info) } | IDENT "Existing"; IDENT "Instance"; id = global; info = hint_info -> - { VernacDeclareInstances [id, info] } + { VernacExistingInstance [id, info] } | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global; pri = OPT [ "|"; i = natural -> { i } ] -> { let info = { Typeclasses.hint_priority = pri; hint_pattern = None } in let insts = List.map (fun i -> (i, info)) ids in - VernacDeclareInstances insts } + VernacExistingInstance insts } - | IDENT "Existing"; IDENT "Class"; is = global -> { VernacDeclareClass is } + | IDENT "Existing"; IDENT "Class"; is = global -> { VernacExistingClass is } (* Arguments *) | IDENT "Arguments"; qid = smart_global; @@ -809,9 +809,8 @@ GRAMMAR EXTEND Gram | IDENT "transparent" -> { Conv_oracle.transparent } ] ] ; instance_name: - [ [ name = ident_decl; sup = OPT binders -> - { (CAst.map (fun id -> Name id) (fst name), snd name), - (Option.default [] sup) } + [ [ name = ident_decl; bl = binders -> + { (CAst.map (fun id -> Name id) (fst name), snd name), bl } | -> { ((CAst.make ~loc Anonymous), None), [] } ] ] ; hint_info: @@ -845,10 +844,10 @@ GRAMMAR EXTEND Gram [ [ IDENT "Comments"; l = LIST0 comment -> { VernacComments l } (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *) - | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; + | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":"; expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200"; info = hint_info -> - { VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) } + { VernacDeclareInstance (bl, (id, expl, t), info) } (* Should be in syntax, but camlp5 would not factorize *) | IDENT "Declare"; IDENT "Scope"; sc = IDENT -> diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 8d6268753e..78e26c65d4 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -215,7 +215,7 @@ let add_vo_path ~recursive lp = let () = match lp.has_ml with | AddNoML -> () | AddTopML -> add_ml_dir unix_path - | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs in + | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs; add_ml_dir unix_path in let add (path, dir) = Loadpath.add_load_path path ~implicit dir in let () = List.iter add dirs in diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index e0dd3380f9..5eeeaada2d 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -887,10 +887,9 @@ open Pputils spc() ++ pr_class_rawexpr c2) ) - | VernacInstance (abst, sup, (instid, bk, cl), props, info) -> + | VernacInstance (sup, (instid, bk, cl), props, info) -> return ( hov 1 ( - (if abst then keyword "Declare" ++ spc () else mt ()) ++ keyword "Instance" ++ (match instid with | {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc () @@ -906,13 +905,23 @@ open Pputils | None -> mt())) ) + | VernacDeclareInstance (sup, (instid, bk, cl), info) -> + return ( + hov 1 ( + keyword "Declare Instance" ++ spc () ++ pr_ident_decl instid ++ spc () ++ + pr_and_type_binders_arg sup ++ + str":" ++ spc () ++ + (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ + pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info) + ) + | VernacContext l -> return ( hov 1 ( keyword "Context" ++ pr_and_type_binders_arg l) ) - | VernacDeclareInstances insts -> + | VernacExistingInstance insts -> let pr_inst (id, info) = pr_qualid id ++ pr_hint_info pr_constr_pattern_expr info in @@ -922,7 +931,7 @@ open Pputils spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts) ) - | VernacDeclareClass id -> + | VernacExistingClass id -> return ( hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_qualid id) ) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index dbccea1117..26859cd2cf 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1005,22 +1005,29 @@ let vernac_identity_coercion ~atts id qids qidt = (* Type classes *) -let vernac_instance ~atts abst sup inst props pri = +let vernac_instance ~atts sup inst props pri = let open DefAttributes in let atts = parse atts in let global = not (make_section_locality atts.locality) in Dumpglob.dump_constraint (fst (pi1 inst)) false "inst"; let program_mode = Flags.is_program_mode () in - ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri) + ignore(Classes.new_instance ~program_mode ~global atts.polymorphic sup inst props pri) + +let vernac_declare_instance ~atts sup inst pri = + let open DefAttributes in + let atts = parse atts in + let global = not (make_section_locality atts.locality) in + Dumpglob.dump_definition (fst (pi1 inst)) false "inst"; + Classes.declare_new_instance ~global atts.polymorphic sup inst pri let vernac_context ~poly l = if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom -let vernac_declare_instances ~section_local insts = +let vernac_existing_instance ~section_local insts = let glob = not section_local in List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts -let vernac_declare_class id = +let vernac_existing_class id = Record.declare_existing_class (Nametab.global id) (***********) @@ -2227,11 +2234,13 @@ let interp ?proof ~atts ~st c = vernac_identity_coercion ~atts id s t (* Type classes *) - | VernacInstance (abst, sup, inst, props, info) -> - vernac_instance ~atts abst sup inst props info + | VernacInstance (sup, inst, props, info) -> + vernac_instance ~atts sup inst props info + | VernacDeclareInstance (sup, inst, info) -> + vernac_declare_instance ~atts sup inst info | VernacContext sup -> vernac_context ~poly:(only_polymorphism atts) sup - | VernacDeclareInstances insts -> with_section_locality ~atts vernac_declare_instances insts - | VernacDeclareClass id -> unsupported_attributes atts; vernac_declare_class id + | VernacExistingInstance insts -> with_section_locality ~atts vernac_existing_instance insts + | VernacExistingClass id -> unsupported_attributes atts; vernac_existing_class id (* Solving *) | VernacSolveExistential (n,c) -> unsupported_attributes atts; vernac_solve_existential n c diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 417c9ebfbd..68a17e316e 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -300,18 +300,22 @@ type nonrec vernac_expr = (* Type classes *) | VernacInstance of - bool * (* abstract instance *) local_binder_expr list * (* super *) typeclass_constraint * (* instance name, class name, params *) (bool * constr_expr) option * (* props *) Hints.hint_info_expr + | VernacDeclareInstance of + local_binder_expr list * (* super *) + (ident_decl * Decl_kinds.binding_kind * constr_expr) * (* instance name, class name, params *) + Hints.hint_info_expr + | VernacContext of local_binder_expr list - | VernacDeclareInstances of + | VernacExistingInstance of (qualid * Hints.hint_info_expr) list (* instances names, priorities and patterns *) - | VernacDeclareClass of qualid (* inductive or definition name *) + | VernacExistingClass of qualid (* inductive or definition name *) (* Modules and Module Types *) | VernacDeclareModule of bool option * lident * |